feat(ClassicalMechanics): inertia tensor about a point and the parallel-axis theorem

[giuseppesorge]

Adds the inertia tensor of a rigid body about an arbitrary point and proves the
parallel-axis theorem, discharging the parallel_axis_theorem informal lemma
(tag LL32-PA, Landau & Lifshitz, Mechanics, §32).

Everything lives in Physlib/ClassicalMechanics/RigidBody/Basic.lean, next to inertiaTensor
(+95 / −8 lines, one file, plus the API map).

What is added

Declaration	What it is
RigidBody.inertiaTensorAbout R p	the inertia tensor with the moments taken about p rather than about the origin of the reference frame
RigidBody.inertiaTensorAbout_apply	its (i, j) entry as a moment of the mass distribution (rfl)
RigidBody.inertiaTensorAbout_zero	inertiaTensorAbout 0 = inertiaTensor, identifying the new definition with the existing one
RigidBody.inertiaTensorAbout_symmetric	symmetry, about any point
RigidBody.inertiaTensorAbout_integrand_split	the algebraic split of the integrand about p into the integrand about the centre of mass, terms linear in the centred coordinates y − c, and a constant
RigidBody.inertiaTensorAbout_eq_centerOfMass_add_pointMass	the parallel-axis theorem, I(p) = I(c) + M (|c − p|² 1 − (c − p) ⊗ (c − p))
RigidBody.inertiaTensor_eq_centerOfMass_add_pointMass	its specialisation to the origin, I(0) = I(c) + M (|c|² 1 − c ⊗ c)

The parallel_axis_theorem informal lemma is removed (replaced by the formal statement) and the
API map gains the corresponding requirement.

Reading order

1. inertiaTensorAbout and inertiaTensorAbout_apply — the definition.
2. inertiaTensorAbout_integrand_split — pure algebra on test functions: y − p = (y − c) + (c − p)
   expands the integrand into the centred integrand, terms linear in y − c, and a constant.
3. inertiaTensorAbout_eq_centerOfMass_add_pointMass — apply ρ; the linear terms die by
   rho_coord_sub_centerOfMass (the first moment about the centre of mass vanishes, whence the
   R.mass ≠ 0 hypothesis) and the constant contributes M times itself.

Two points I would flag

• The informal statement was true only about the centre of mass. Its docstring read
  I_{O'} = I_O + M(|a|² 1 − a ⊗ a) for a displacement a between two arbitrary points; that
  holds when O is the centre of mass, otherwise first-moment terms survive. The formal theorem
  therefore takes the centre of mass as the base point, which is the L&L §32 statement.
• Why inertiaTensor is not redefined as inertiaTensorAbout 0. inertiaTensor is the
  origin-based notion already used by angularMomentum and rotationalKineticEnergy, so I left
  it as the primitive and added inertiaTensorAbout_zero (a simp lemma) as the bridge, keeping
  the diff to one file. Happy to invert the definitional order if you prefer it the other way.

If the inertia API grows further (principal axes, the spatial tensor R I Rᵀ), these declarations
would naturally move together into a dedicated RigidBody/Inertia.lean; that seemed premature for
this PR.

Verification

• lake build — full aggregate, 9264 jobs, green; Basic.lean recompiles from scratch with no
  warnings.
• lake exe runPhyslibLinters — Linting passed for Physlib.
• lake exe check_file_imports, lake exe check_dup_tags, lake exe sorry_lint — all pass.
• ./scripts/lint-style.sh — exit 0; python scripts/api_map_linter.py --repo . — [ok] for
  RigidBody/API-map.yaml.
• #print axioms on all seven new declarations — [propext, Classical.choice, Quot.sound] only.

AI disclosure: drafted with Claude Code (see the commit trailer); every statement and proof has
been read and checked by me.

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