auto-task(RigidBody): add API-map.yaml tracking the Rigid body API

[ShlokVaibhav]

Summary

Adds Physlib/ClassicalMechanics/RigidBody/API-map.yaml, a new in-repo tracker for the
Rigid body API (Physlib/ClassicalMechanics/RigidBody/). The map is generated from the
directory's Lean files (Basic.lean, SolidSphere.lean), with GitHub issue
#893 "API: Rigid body" used only
as a reference for the intended scope. No Lean source is touched; lake build stays green
(a YAML-only change).

The directory has no API-map.yaml yet and no open PR is adding or editing an API-map.yaml
anywhere. The two open PRs that touch this directory are #1320 (adds a new Motion.lean) and
#962 (proves solidSphere_inertiaTensor, against the old PhysLean/ path); neither adds a map,
so there is no conflict.

Links below pin commit 843373266f73adaccb4db401c545fdef9810f78e so line numbers are stable.

A note on the issue checklist vs. the code

Per the task rules, every done flag was decided by reading the code, not by trusting the
issue's checkboxes.

• The four items the issue marks - [x] (RigidBody defined, mass, centre of mass, moment of
  inertia) are all genuinely present and are marked done: true.
• The four items the issue marks - [ ] (angular velocity, velocity of the centre of mass,
  kinetic energy, Euler angles) exist in the directory only as informal_definition /
  informal_lemma stubs (no formal declaration), so they are marked done: false. In
  particular the code's euler_equations is an informal statement of Euler's equations of
  motion, which is not the Euler angles the issue asks for.
• Two items the issue does not list are genuinely provided by the code and are added as
  done: true: the inertia-tensor symmetry lemma, and the solid sphere worked example
  (definition + mass + centre of mass).
• The solid sphere's inertia tensor is stated (solidSphere_inertiaTensor) but proved with
  sorry (@[sorryful]), so it is done: false.
• The one TODO in the directory (switch RigidBody to continuous linear maps) is carried as a
  done: false requirement.

---

Field-by-field justification (reviewer tick-box)

Title / Overview

Title: Rigid body

Overview: |
    The key data structure is `RigidBody d`, a rigid body in `d` dimensions specified by
    its mass distribution (a linear map from smooth functions on `Space d` to `ℝ`). The API
    provides the body's total mass, centre of mass and inertia tensor, and works out the
    solid sphere as a concrete example.

Grounded in the Basic.lean module docstring
(Basic.lean#L11-L25):

# Rigid bodies

A rigid body is one where the distance and relative orientation between particles does not change.
In other words, the body remains undeformed.

In this module we will define the basic properties of a rigid body, including
- mass
- center of mass
- inertia tensor

and the SolidSphere.lean module docstring
(SolidSphere.lean#L11-L18):

# The solid sphere as a rigid body

In this module we consider the solid sphere as a rigid body, and compute its mass,
center of mass and inertia tensor.

The "mass distribution as a linear map" phrasing is the structure field itself
(Basic.lean#L35-L38):

/-- A Rigid body defined by its mass distribution. -/
structure RigidBody (d : ℕ) where
  /-- The mass distribution of the rigid body. -/
  ρ : C^⊤⟮𝓘(ℝ, Space d), Space d; 𝓘(ℝ, ℝ), ℝ⟯ →ₗ[ℝ] ℝ

Issue #893: "The key data structure shall be the definition of a Rigid Body specified by its
mass distribution."

ParentAPIs

ParentAPIs:
  - Space (Physlib/SpaceAndTime/Space)

Determined from the imports/usages. Basic.lean imports and uses the Space API
(Basic.lean#L8;
Space d appears in the RigidBody field and in centerOfMass,
Basic.lean#L45-L47),
and SolidSphere.lean imports the Space integrals API
(SolidSphere.lean#L8-L9):

public import Physlib.ClassicalMechanics.RigidBody.Basic
public import Physlib.SpaceAndTime.Space.Integrals.Basic

Issue #893 lists "Parent APIs #854 #855" (Space and Time). Only Space (#854) is actually
imported/used by this directory — there is no Time import or usage — so, taking the code as the
source of truth, only Space is listed.

References

References:
  - Landau and Lifshitz, Mechanics, Section 32 (page 100)

Taken from the Basic.lean module docstring's ## References section
(Basic.lean#L23-L24):

## References
- Landau and Lifshitz, Mechanics, page 100, Section 32

Matches issue #893: "References — Landau and Lifshitz, Mechanics, Section 32." Not invented.

---

Requirements

✅ RigidBody is defined

- description: >
    The key data structure `RigidBody`, a rigid body specified by its mass distribution,
    is defined.
  done: true
  location: Physlib/ClassicalMechanics/RigidBody/Basic.lean (RigidBody)

Basic.lean#L35-L38

/-- A Rigid body defined by its mass distribution. -/
structure RigidBody (d : ℕ) where
  /-- The mass distribution of the rigid body. -/
  ρ : C^⊤⟮𝓘(ℝ, Space d), Space d; 𝓘(ℝ, ℝ), ℝ⟯ →ₗ[ℝ] ℝ

Issue #893: "Key data structure … - [x] is defined".

✅ Total mass

- description: The API allows the calculation of the total mass of the rigid body.
  done: true
  location: Physlib/ClassicalMechanics/RigidBody/Basic.lean (RigidBody.mass)

Basic.lean#L42-L43

/-- The total mass of the rigid body. -/
noncomputable def mass {d : ℕ} (R : RigidBody d) : ℝ := R.ρ ⟨fun _ => 1, contMDiff_const⟩

Issue #893: "- [x] The API shall allow the calculation of the total mass of the rigid body."

✅ Centre of mass

- description: The API allows the calculation of the centre of mass of the rigid body.
  done: true
  location: Physlib/ClassicalMechanics/RigidBody/Basic.lean (RigidBody.centerOfMass)

Basic.lean#L45-L47

/-- The center of mass of the rigid body. -/
noncomputable def centerOfMass {d : ℕ} (R : RigidBody d) : Space d := ⟨fun i =>
  (1 / R.mass) • R.ρ ⟨fun x => x i, ContDiff.contMDiff <| by fun_prop⟩⟩

Issue #893: "- [x] The API shall allow the calculation of the center of mass of the rigid body."

✅ Moment of inertia (inertia tensor)

- description: >
    The API allows the calculation of the moment of inertia (inertia tensor) of the
    rigid body.
  done: true
  location: Physlib/ClassicalMechanics/RigidBody/Basic.lean (RigidBody.inertiaTensor)

Basic.lean#L49-L53

/-- The inertia tensor of the rigid body. -/
noncomputable def inertiaTensor {d : ℕ} (R : RigidBody d) :
    Matrix (Fin d) (Fin d) ℝ := fun i j =>
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k : Fin d, (x k)^2 - x i * x j,
    ContDiff.contMDiff <| by fun_prop⟩

Issue #893: "- [x] The API shall allow the calculation of the moment of inertia of the rigid body."

✅ Inertia tensor is symmetric (not in issue; provided by code)

- description: The inertia tensor of the rigid body is symmetric.
  done: true
  location: Physlib/ClassicalMechanics/RigidBody/Basic.lean (RigidBody.inertiaTensor_symmetric)

Basic.lean#L55-L63

lemma inertiaTensor_symmetric {d : ℕ} (R : RigidBody d) (i j : Fin d) :
    R.inertiaTensor i j = R.inertiaTensor j i := by
  simp only [inertiaTensor]
  ...

Not in the issue checklist, but a fully-proved lemma in the directory, so done: true.

✅ Solid sphere worked example (definition + mass + centre of mass)

- description: >
    The API provides the solid sphere as a worked example, with its total mass and centre
    of mass computed.
  done: true
  location: >
    Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean
    (RigidBody.solidSphere, RigidBody.solidSphere_mass, RigidBody.solidSphere_centerOfMass)

Definition
SolidSphere.lean#L28-L44:

/-- The solid sphere as a rigid body. -/
noncomputable def solidSphere (d : ℕ) (m R : ℝ≥0) : RigidBody d where
  ρ := ⟨⟨fun f => m / volume.real (Metric.closedBall (0 : Space d) R) *
      ∫ x in Metric.closedBall (0 : Space d) R, f x ∂volume, ...

Mass = m
SolidSphere.lean#L46-L58:

lemma solidSphere_mass {d : ℕ} (m R : ℝ≥0) (hr : R ≠ 0) : (solidSphere d m R).mass = m := by

Centre of mass = 0
SolidSphere.lean#L60-L73:

/-- The center of mass of a solid sphere located at the origin is `0`. -/
lemma solidSphere_centerOfMass {d : ℕ} (m R : ℝ≥0) : (solidSphere d m R).centerOfMass = 0 := by

Both lemmas are fully proved (no sorry). Motivated by issue #893: "This API is needed to study
many examples in classical mechanics, for example rigid spheres."

❌ Solid sphere inertia tensor (stated but sorry)

- description: >
    The inertia tensor of the solid sphere equals `2/5 m R^2` times the identity. Stated as
    `solidSphere_inertiaTensor` but currently proved with `sorry`.
  done: false
  location: N/A

SolidSphere.lean#L75-L80

/-- The moment of inertia tensor of a solid sphere through its center of mass is
  `2/5 m R^2 * I`. -/
@[sorryful]
lemma solidSphere_inertiaTensor (m R : ℝ≥0) (hr : R ≠ 0) :
    (solidSphere 3 m R).inertiaTensor = (2/5 * m.1 * R.1^2) • (1 : Matrix _ _ _) := by
  sorry

The statement exists but the proof is sorry (@[sorryful]), so the result is not established →
done: false. (Open PR #962 aims to complete this proof.)

❌ Angular velocity of rotation

- description: The API contains the definition of the angular velocity of rotation of the rigid body.
  done: false
  location: N/A

Issue #893: "- [ ] The API shall contain the definition of the angular velocity of rotation of
the rigid body." Only an informal_lemma stub exists, no formal declaration
(Basic.lean#L90-L94):

/-- The angular velocity of rotation of a rigid body from a system of coordinates fixed in the
    body is independent of the system chosen. -/
informal_lemma angular_velocity_is_well_defined where
  tag := "LL32-AM"
  deps := [``RigidBody]

grep -rn "angularVelocity\|def angular" in the directory returns nothing → done: false.

❌ Velocity of the centre of mass

- description: The API contains the definition of the velocity of the centre of mass of the rigid body.
  done: false
  location: N/A

Issue #893: "- [ ] The API shall contain the definition of the velocity of the center of mass of
the rigid body." No such formal declaration exists in the directory (only centerOfMass, the
position, at Basic.lean#L45-L47)
→ done: false.

❌ Kinetic energy

- description: The API contains the definition of the kinetic energy of the rigid body.
  done: false
  location: N/A

Issue #893: "- [ ] The API shall contain the definition of the kinetic energy of the rigid
body." Only an informal_definition stub exists, no formal declaration
(Basic.lean#L65-L68):

/-- The kinetic energy of a rigid body. -/
informal_definition kineticEnergy where
  tag := "MEYBM"
  deps := [``RigidBody]

grep for a formal def kineticEnergy returns nothing → done: false.

❌ Euler angles

- description: The API contains the definition of Euler angles for a rigid body.
  done: false
  location: N/A

Issue #893: "- [ ] The API shall contain the definition of Euler angles for a rigid body." No
Euler-angle declaration exists. The only "Euler" content is an informal statement of Euler's
equations of motion (not Euler angles)
(Basic.lean#L206-L212):

informal_lemma euler_equations where
  tag := "LL32-EQ"
  deps := [``RigidBody]

→ done: false.

❌ Redefine RigidBody with continuous linear maps (directory TODO)

- description: >
    Redefine `RigidBody` using continuous linear maps instead of plain linear maps from
    the space of smooth functions to `ℝ` (existing TODO).
  done: false
  location: N/A

From the TODO in the directory
(Basic.lean#L31-L33):

TODO "The definition of a rigid body is currently defined via linear maps
  from the space of smooth functions to ℝ. When possible, it should be change
  to *continuous* linear maps. "

Not yet done (the structure field is still →ₗ[ℝ], not →L[ℝ], at
Basic.lean#L38)
→ done: false.

---

Verification

• ruby -e 'require "yaml"; ...' → valid YAML; top-level keys are exactly
  version, Title, Overview, ParentAPIs, References, Requirements (no others); 12 requirements,
  6 done: true, 6 done: false. Every done: true has a real location; every done: false
  has location: N/A.
• Every done: true declaration was confirmed in the source at the pinned SHA (line numbers
  above); the working tree matches the SHA for these files (git diff is empty).
• done: false items confirmed absent as formal declarations via grep in the directory
  (kineticEnergy, angularVelocity, euler/Euler angles), and solidSphere_inertiaTensor
  confirmed to be @[sorryful] + sorry.
• lake build is unaffected — this is a YAML-only addition that cannot enter the Lean build
  graph.
• No .lean file, other map, docstring, or the GitHub issue was modified.

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

Approved - many thanks. Will merge now.