feat(ClassicalMechanics): add Caldirola-Kanai lagrangian for the damped harmonic oscillator

[giuseppesorge]

Summary

Adds the Caldirola–Kanai lagrangian for the damped harmonic oscillator and the simplification of its variational gradient to the Euler-Lagrange equations, completing two open requirements of #905. Since the damped oscillator is non-conservative, the plain T − V lagrangian does not reproduce the damped equation of motion; the Caldirola–Kanai lagrangian exp (γ/m * t) * (T − V) does: its Euler-Lagrange equation is exactly m ẍ + γ ẋ + k x = 0, the EquationOfMotion already in the file.

The new section F mirrors the structure of HarmonicOscillator/Basic.lean (sections D.1–D.3).

Changes

Declaration	File	Change
lagrangian	DampedHarmonicOscillator/Basic.lean	new def: exp (γ/m * t) * undamped lagrangian
lagrangian_eq, lagrangian_eq_exp_mul_kineticEnergy_sub_potentialEnergy, lagrangian_of_isUndamped	〃	equalities; reduction to the undamped lagrangian at γ = 0
contDiff_lagrangian (@[fun_prop])	〃	smoothness in all arguments
gradient_const_mul (private)	〃	helper: gradient (c * f) = c • gradient f
gradient_lagrangian_position_eq, gradient_lagrangian_velocity_eq	〃	gradients, reusing the HarmonicOscillator gradient lemmas
gradLagrangian	〃	new def: variational gradient δ ∫ L of the action
gradLagrangian_eq_eulerLagrangeOp	〃	via euler_lagrange_varGradient
deriv_exp_smul (private)	〃	∂ₜ (exp (a t) • y t) product rule
gradLagrangian_eq_force	〃	simplification to exp (γ/m * t) • (F − m a)
equationOfMotion_iff_gradLagrangian_zero	〃	EoM ⟺ variational gradient vanishes
Time.val_contDiff (@[fun_prop])	SpaceAndTime/Time/Derivatives.lean	completes the val_measurable/val_differentiable API; needed for contDiff_lagrangian (section D retitled "Smoothness properties" to cover it)
requirements	DampedHarmonicOscillator/API-map.yaml	lagrangian + variational-gradient marked done; kinetic/potential energy marked done as inherited from HarmonicOscillator (per the discussion on #905); Overview and References synced

Reviewer reading order: Time.val_contDiff → lagrangian → F.1.1–F.1.3 → gradLagrangian → gradLagrangian_eq_force → equationOfMotion_iff_gradLagrangian_zero.

Scope — what is NOT changed

• No existing statement, definition, or proof is changed; besides the new declarations, only the Time/Derivatives.lean section-D title and the API-map prose are touched.
• The variational-gradient formula in HarmonicOscillator/Basic.lean section D.2 transposes the position and velocity arguments of L(t, x, v) (doc-only typo). The new section F.2 here states it correctly; I can fix the HarmonicOscillator docstring in a small follow-up rather than widen this diff.
• Solution.lean has a private exp_decay_smul_velocity similar in spirit to the private deriv_exp_smul added here (decay vs growth sign, function-level vs pointwise). Unifying them would mean touching Solution.lean; happy to do that as a follow-up if preferred.
• The uniqueness-of-solution requirement of API: Damped harmonic oscillator #905 is untouched (tracked by the existing TODO in Solution.lean).

On size: the diff is 236 gross lines, but roughly half is module-doc/section-header text required by the numbered template; the net Lean code is ~110 lines forming one coherent concept (the CK lagrangian and its Euler-Lagrange derivation), which loses its point if split.

Verification

• lake build (full library): success; touched modules re-built clean after the final docs pass.
• lake exe lint_all: passes (the "transitive imports" shake messages are the known pre-existing false positives, incl. on Time/Derivatives.lean before this change).
• ./scripts/lint-style.sh (on the committed state): clean.
• #print axioms on all 12 new public declarations: only [propext, Classical.choice, Quot.sound].

Toward #905.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[jstoobysmith]

Great! This is really nice! Just a couple of convention comments.

[jstoobysmith]

I would keep this as:

Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean (kineticEnergy)

just because I think we will likely use a script at some point to make sure these definitions go to a place which actually exists. (likewise with below).

[giuseppesorge]

Done - both inherited-energy location fields now use the plain file (name) format; the inheritance rationale stays in the Overview.

[giuseppesorge]

-awaiting-author

[jstoobysmith]

Approved - will merge shortly. Many thanks.