feat(ClassicalMechanics): the small-angle regime of the simple pendulum as a harmonic oscillator - #1572
Conversation
|
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.
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. |
…ian and Hamilton's equations New module Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Hamiltonian (imported from Physlib.lean), with the Hamiltonian formulation of the simple pendulum: - toCanonicalMomentum: the canonical momentum p = dL/dtheta-dot = I theta-dot, as a linear equivalence between velocities and momenta, with its value toCanonicalMomentum_eq. - hamiltonian: the Legendre transform of the Lagrangian, with hamiltonian_eq computing it as the momentum-space kinetic energy plus the potential energy, hamiltonian_contDiff for its joint smoothness, and the partial gradients gradient_hamiltonian_position_eq and gradient_hamiltonian_momentum_eq. - hamiltonian_eq_energy: along any lift of the angle the Hamiltonian, evaluated on the canonical momentum of the lift, is the energy. - hamiltonEqOp: the Hamilton-equations operator of the Hamiltonian on momentum-angle phase space. - equationOfMotion_iff_hamiltonEqOp_eq_zero: for a smooth lift of the angle the equation of motion is equivalent to Hamilton's equations. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Add section B to SimplePendulum/Hamiltonian.lean: equationOfMotion_tfae proves that, for a smooth lift of the angle, the pointwise equation of motion, the vanishing of the variational derivative of the action, Hamilton's equations, the Lagrangian variational principle and the Hamiltonian variational principle are all equivalent. Update the module doc (Key results bullet and TOC entry for section B) and the API map (Hamiltonian-formulation requirement row, Overview kept consistent). Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
e9c3307 to
7e1e043
Compare
…miltonian module - Rename `toCanonicalMomentum` to `canonicalMomentum` (the `to` prefix is for maps into a different type); `toCanonicalMomentum_eq` becomes `canonicalMomentum_eq`. - Inline the four one-line proofs of the linear equivalence. - Drop the sub-subsection heading that introduced a single lemma. Requested by review on leanprover-community#1570. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
… linearized equation of motion - toHarmonicOscillator (m := inertia, k := m g l) with simp projections and toHarmonicOscillator_omega - LinearizedEquationOfMotion with its Newton form (smoothness-free) and the equivalence with the oscillator's equation of motion for smooth lifts - imports HarmonicOscillator.Basic only (no Solution API used in this commit; the next commit extends the import) Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
…m the harmonic oscillator - Import HarmonicOscillator.Solution (re-exporting Basic) to inherit the oscillator's solution theory. - smallAngleTrajectory: the small-angle motion of given initial conditions as the trajectory of the associated harmonic oscillator, with smoothness (smallAngleTrajectory_contDiff) and its initial data at time 0 (smallAngleTrajectory_at_zero, smallAngleTrajectory_velocity_at_zero). - Existence and uniqueness: smallAngleTrajectory_linearizedEquationOfMotion and linearized_unique, both transferred through linearizedEquationOfMotion_iff; uniqueness routes the separate initial-data hypotheses into the conjunction taken by HarmonicOscillator.InitialConditions.trajectories_unique. - releasedFromRest: the motion released from rest at angle θ₀ in the fun_prop-friendly cosine-smul shape, identified with the trajectory of ⟨single 0 θ₀, 0⟩ (releasedFromRest_eq), with its initial angle, vanishing initial angular velocity, and the linearized equation of motion. - Module doc: key results and table of contents extended for section C. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
…y and the cubic linearization bound - Section D: smallAnglePeriod as the period of the associated harmonic oscillator, with the closed forms 2π/ω and 2π √(ℓ/g), positivity, the periodicity of every small-angle trajectory and of releasedFromRest, and the constant energy ½ (I ‖v₀‖² + m g ℓ ‖θ₀‖²) of a small-angle trajectory, transferred in its exact closed form from HarmonicOscillator.InitialConditions.trajectory_energy. - Section E: the cubic linearization bound |τ(θ) + m g ℓ θ| ≤ m g ℓ |θ|³/6 via Real.abs_sub_sin_le, the exact vector difference torque_sub_toHarmonicOscillator_force, and gradLagrangian_sub_toHarmonicOscillator identifying the difference of the variational gradients of the two actions with the difference of torque and linearized force, the inertial terms cancelling. - Task-2 review fold-ins: @[fun_prop] on smallAngleTrajectory_contDiff, @[simp] on the four at-zero lemmas, and the two small-angle docstring qualifiers; module doc ii/iii extended with the new sections. - API map: two new rows (the small-angle limit; the relation between the full and the linearized dynamics) and the overview clause brought up to date. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
…ngle module - extend the Overview through the inherited solution theory, the mass- and amplitude-free period 2π√(ℓ/g), and the cubic measure of what the linearization discards - prose fixes: the pendulum "is approximated by" its associated oscillator; the released-from-rest periodicity docstring describes the linearized motion; the energy docstring names the initial angle as ‖IC.x₀‖ - Huygens: drop the historically inverted pendulum-clocks clause, keep the isochrony attribution, and add Horologium Oscillatorium (1673) to the references - state the rotational Newton form of the linearized equation with S.inertia - new lemmas: smallAngleTrajectory_eq (the closed form), norm_torque_sub_toHarmonicOscillator_force_le (the normed cubic bound), and norm_equationOfMotion_residual_le (new subsection E.3: a small-angle motion nearly solves the pendulum's own equation of motion) - reorder E.1 exact-difference-first and derive the coordinate bound from the exact difference instead of recomputing the torque - dot-notation for the associated oscillator's force and gradLagrangian sites - API map: the classical amplitude-dependent period formula follows in later modules; its identification with the nonlinear return time remains open Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
7e1e043 to
b7bb450
Compare
2 participants
Toward #883. The small-angle regime.
Stacked. Base is the Hamiltonian PR #1570 (branch
pendulum/pr3-hamiltonian,bda52edb);this PR is independent of #1571 by design — no common Lean file (the two do both edit the
Overviewparagraph ofSimplePendulum/API-map.yaml; whichever merges second needs aone-paragraph hand-merge). The commits belonging to this PR are the last four
(
deb72686..b7bb4508).One new module,
Physlib/ClassicalMechanics/Pendulum/SimplePendulum/SmallAngle.lean(584 addedlines, of which 146 are Lean code — 31 declarations), plus
Physlib.leanand two API-map rows.The single concept: the linearized simple pendulum is the harmonic oscillator of mass
I = m ℓ²and spring constantm g ℓ— so its solution theory is inherited rather thanreproved — together with the cubic bound that says how far the linearization is from the truth.
toHarmonicOscillator; its frequency isSimplePendulum.ω = √(g/ℓ)— the mass cancelsLinearizedEquationOfMotion(θ̈ + ω² θ = 0); its smoothness-free Newton form; the smooth-lift equivalence with the oscillator's equation of motion (with the totalized-variational caveat spelled out)@[simp]initial-data lemmas, uniqueness (linearized_unique), the closed form, andreleasedFromRest— the cosine motion, genuinely at rest att = 0smallAnglePeriod = 2π √(ℓ/g)(as derived by Huygens, 1673) — mass- and amplitude-free; periodicity; the conserved energy in closed formm g ℓ (θ − sin θ); the cubic bounds≤ m g ℓ ‖θ‖³/6(normed and coordinate forms, viaReal.abs_sub_sin_le); and the capstonenorm_equationOfMotion_residual_le— a small-angle motion solves the pendulum's own equation of motion up to a cubically small residualEvery statement and docstring keeps the linearized/true boundary explicit — nothing claims
small-angle results for the true pendulum beyond the quantified E-section bounds. The API map now
records: "the classical amplitude-dependent period formula follows in later modules; its
identification with the nonlinear return time remains open."
Reviewer reading order: the module doc (i–iv); §A–B (the smoothness split); skim §C–D (one-to-
three-line transfers, following
DampedHarmonicOscillator.toUndamped); read §E closely — it iswhere the PR says what the linearization costs.
Verification: full
lake build+ complete linter battery pass; axiom audit clean; theLandau–Lifshitz citations were verified by the author against the printed sources.
Developed with assistance from AI; all mathematics and proofs were reviewed and verified to compile.