feat(ClassicalMechanics): the simple pendulum's dynamics, Lagrangian and equation of motion

[aadarwal]

Toward #883. Second of the series (after #1560, merged, and #1561).

Stacked on #1561. This branch contains #1561's commits underneath it (the dynamics import the
configuration-space API map). The commits belonging to this PR are the last six
(5114c9df..b0965d2a); the diff cleans itself once #1561 merges and this branch is rebased.

Adds Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Basic.lean: the input data of the simple gravity pendulum, its energies, its Lagrangian, the torque of gravity, and the equation of motion I θ̈ = τ(θ) with its scalar form θ̈ + (g/ℓ) sin θ = 0. The dynamics are written on the Euclidean lift Time → EuclideanSpace ℝ (Fin 1), exactly as HarmonicOscillator/Basic.lean does; the geometric configuration space added in #1561 is connected to it in a later PR.

Size. 754 added lines in Basic.lean, of which 434 are documentation (335 module-doc and section prose, 99 docstrings) and ~236 are non-blank Lean. For comparison, HarmonicOscillator/Basic.lean is 756 lines with the same section structure. The two feature commits are separable — 5114c9df is sections A–C (data, frequency, inertia, energies) and ccce411d is D–F (Lagrangian, torque, equation of motion) — and I am happy to split this into two PRs at that boundary if you would prefer to review it that way.

One design choice worth flagging. The equation of motion is defined as the pointwise relation ∀ t, I • θ̈ t = τ(θ t), following DampedHarmonicOscillator/Basic.lean, rather than as the vanishing of the variational derivative as in HarmonicOscillator/Basic.lean. varGradient is defined to be 0 when no variational gradient exists, so its vanishing holds for every lift too rough to admit one; the pointwise form is totalized too, but its totalization hands a rough lift θ̈ = 0 and leaves a genuine, generally false constraint rather than a vacuous truth. The two agree for smooth lifts; that equivalence, and energy conservation, come in the follow-up PR. IsSolution θ := ContDiff ℝ ∞ θ ∧ EquationOfMotion θ is the public notion of a solution, and excludes the piecewise-equilibrium functions that the bare pointwise equation admits.

Reviewer reading order

1. The module doc (sections i–iv) — the physics, the choice of lift, and the table of contents.
2. Section E, and in particular the prose preceding E.1 — the rationale for the pointwise equation of motion. This is the only place where the pendulum departs from the harmonic oscillator's design, and it is the part most worth disagreeing with.
3. Sections A–C — the data, ω, inertia, and the energies. ω_sq_mul_inertia is the identity that cancels the mass; gradient_potentialEnergy is the only real calculus in the section.
4. Section D — the Lagrangian and its two partial gradients, both of which feed section F.
5. Sections E.4 and F — the scalar equation, mass independence, and the variational derivative.
6. SimplePendulum/API-map.yaml and the one-line addition to Physlib.lean.

Declarations added

All in Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Basic.lean, namespace ClassicalMechanics.SimplePendulum.

Section	Declaration	What it is
A.1	SimplePendulum	the input data: mass m, rod length ℓ, gravity g, all positive
A.2	m_ne_zero, ℓ_ne_zero, g_ne_zero	@[simp] non-vanishing, the form the field-clearing tactics consume
B.1	ω	the angular frequency √(g/ℓ) of the small oscillations
B.1	ω_pos, ω_ne_zero, ω_sq, inverse_ω_sq	positivity, ω² = g/ℓ, (ω²)⁻¹ = ℓ/g
B.2	inertia	the moment of inertia m ℓ² about the pivot
B.2	inertia_pos, inertia_ne_zero	positivity and non-vanishing
B.2	ω_sq_mul_inertia	ω² I = m g ℓ — the identity by which the mass cancels
C.1	kineticEnergy, potentialEnergy, energy	½ I θ̇², m g ℓ (1 − cos θ), and their sum
C.2	kineticEnergy_eq, potentialEnergy_eq, energy_eq	definitional unfoldings
C.2	potentialEnergy_nonneg, potentialEnergy_le, potentialEnergy_eq_zero_iff	0 ≤ V ≤ 2 m g ℓ, and V = 0 ↔ cos θ = 1
C.3	potentialEnergy_contDiff, differentiable_potentialEnergy	smoothness of V as a function of the angle
C.3	gradient_potentialEnergy	∇V = m g ℓ sin θ · e₀
C.3	kineticEnergy_differentiable, potentialEnergy_differentiable, energy_differentiable	differentiability in time along a smooth lift
C.4	kineticEnergy_deriv, potentialEnergy_deriv, energy_deriv	each derivative as ⟪θ̇, ·⟫; energy_deriv pairs θ̇ with I θ̈ + ∇V
D.1	lagrangian, lagrangian_eq, lagrangian_eq_kineticEnergy_sub_potentialEnergy	L(t,θ,θ̇) = ½ I ‖θ̇‖² − V(θ), expanded, and as T − V along a lift
D.2	contDiff_lagrangian	joint smoothness of ↿L, the Euler–Lagrange hypothesis
D.3	gradient_lagrangian_position_eq, gradient_lagrangian_velocity_eq	∂L/∂θ = −∇V and ∂L/∂θ̇ = I θ̇, the angular momentum
E.1	torque, torque_eq, torque_apply	τ = −∇V; the generalized force conjugate to the angle, = −m g ℓ sin θ
E.2	EquationOfMotion	∀ t, I • θ̈ t = τ(θ t)
E.2	equationOfMotion_iff_newtons_2nd_law	the equation with all terms on one side (I θ̈ + ∇V = 0), the damped oscillator's shape — the combination energy_deriv pairs with the velocity
E.3	IsSolution, IsSolution.contDiff, IsSolution.equationOfMotion	a smooth lift satisfying the equation, and its two projections
E.4	equationOfMotion_iff_scalar	θ̈ + ω² sin θ = 0 — the mass has cancelled
E.4	equationOfMotion_iff_of_eq_ω	two pendulums with the same ω have the same motions
F.1	gradLagrangian	the variational derivative of the action
F.2	gradLagrangian_eq_eulerLagrangeOp	it is the Euler–Lagrange operator, for smooth lifts
F.3	gradLagrangian_eq_torque	it equals τ(θ) − I θ̈

Also: one public import line in Physlib.lean, and two row updates in SimplePendulum/API-map.yaml (the Lagrangian/equation-of-motion requirement is now met; a new row records the variational equivalence and energy conservation as outstanding).

Why Pendulum/API-map.yaml is in the diff: this PR made the parent map's Overview stale, so it
is amended. I read the parent's "shall subsequently contain the definition of the lagrangian" row
as the Lagrangian built on the configuration-space trajectory — still open, coming with the
geometric bridge — so I left it done: false and recorded the Euclidean-lift Lagrangian in the
SimplePendulum map instead. Happy to flip it if you read that row differently.

Verification

• lake build Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Basic —
• lake build —
• lake exe runPhyslibLinters Physlib —
• lake exe check_file_imports —
• ./scripts/lint-style.sh (run on committed state) —
• python scripts/api_map_linter.py --repo . —
• codespell with the repo's .codespellignore —
• Each public import confirmed necessary by removing it and rebuilding —
• Landau & Lifshitz and Arnold references checked against the printed editions —

Developed with assistance from AI; all mathematics and proofs were reviewed and verified to compile.

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[nateabr]

Would you be able to rebase this branch with your earlier merged PR so that it is a bit easier to see the changes