feat(ClassicalMechanics): add the total kinetic energy and prove the König decomposition

[giuseppesorge]

Adds the total kinetic energy of a rigid body in motion and proves the König decomposition T = ½M V·V + ½∫|ω × r|² dm (Landau–Lifshitz, Mechanics, §32). Follow-up to #1377 in the rigid-body API (#893).

New declarations

Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean (new section for RigidBodyMotion):

• RigidBodyMotion.velocityClosedForm — the closed form Ṙ(t)(y − c) + V(t) of the velocity of the body point y. It is polynomial in y, hence smooth for any motion (contDiff_velocityClosedForm_dotProduct), whereas the honest point velocity ∂ₜ(displacement · y) is not bundleable unconditionally (for non-differentiable motions its junk values need not be smooth in y). For differentiable motions the two agree: velocityClosedForm_eq_velocity.
• RigidBodyMotion.kineticEnergy — the total kinetic energy T = ½ ∫ v ⬝ᵥ v dm at time t, with v = velocityClosedForm.
• kineticEnergy_eq_integral_velocity — for differentiable motions the integrand is the honest point velocity: T = ½ ∫ velocity ⬝ᵥ velocity dm. This is the definitional-honesty lemma.
• kineticEnergy_eq_translational_add_rotational — König's theorem in any dimension: T = ½ M (V ⬝ᵥ V) + ½ ∫ |Ṙ(y − c)|² dm for mass ≠ 0, with no differentiability hypotheses. The cross term ∫ V ⬝ᵥ Ṙ(y − c) dm vanishes because the first moment of the mass distribution about its centre of mass is zero (rho_coord_sub_centerOfMass).
• kineticEnergy_eq_translational_add_angularVelocity — König's theorem in three dimensions: T = ½ M (V ⬝ᵥ V) + ½ ∫ |ω × r|² dm, with ω the angular velocity vector and r = displacement − comTrajectory the position relative to the centre of mass, spelled exactly as in velocity_eq_angularVelocity (feat(ClassicalMechanics): prove the velocity decomposition v = V + ω × r #1376). Needs only DifferentiableAt at t.

Supporting lemmas extracted so they are stated once (previously inline or private):

• Basic.lean: RigidBody.rho_one (ρ 1 = mass, @[simp]) replaces three identical inline have ... := rfl; cmap, cmap_apply, rho_coord_sub_centerOfMass move here from Motion.lean — their subject is RigidBody, so dot notation now works and KineticEnergy.lean can use them.
• Motion.lean: orientation_mulVec_sub_centerOfMass — R(t)(y − c) = displacement t y − comTrajectory t.
• AngularVelocity.lean: deriv_orientation_mulVec_eq_angularVelocity_cross — Ṙ(t)(y − c) = ω(t) × r under DifferentiableAt; velocity_eq_angularVelocity now reuses it and its proof shrinks to two lines.

Other changes

• Basic.lean: removed the informal_definition kineticEnergy stub (tag MEYBM), now formalized. The informal_lemma kinetic_energy_decomposition (LL32-TK) is kept: its ½ ω · I_CM ω form needs the body-frame angular velocity / rotated inertia tensor, planned as a follow-up.
• API-map.yaml: kinetic-energy requirement marked done; Overview extended.

Reading order

Basic.lean (rho_one + relocations) → Motion.lean (orientation_mulVec_sub_centerOfMass) → AngularVelocity.lean (deriv_orientation_mulVec_eq_angularVelocity_cross) → KineticEnergy.lean from namespace RigidBodyMotion.

Verification

• lake build Physlib clean; fresh compile of the touched files with zero warnings.
• #print axioms on all new declarations: only [propext, Classical.choice, Quot.sound].
• lake exe runLinter — no issues in the touched files; ./scripts/lint-style.sh clean.

[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.