5.4. L3 — The body opens up🔗

5.4.1. Synopsis🔗

5.4.1.1. Purpose🔗

Open body A of pair P into two rigid halves, with a body-fixed frame beside the lab frame. Mass assembles over the halves as a sum. The centre of mass is the mass-weighted mean of the halves' positions, which is meaningful only when the total mass is nonzero. Every half of a rigid body has the same angular velocity, so angular velocity is intensive and has no Assembles instance. Each frame-dependent quantity has its frame in its type (InFrame), so a body-frame rotational energy computed from a lab-frame angular velocity fails to type-check.

5.4.1.2. PKC vocabulary in scope🔗

New at this step:

WeightedCarving (parts, weight, mean, total_ne_zero) — a carving with per-part weights whose mean requires nonzero total weight.
totalWeight, weightedSum — the pieces of a weighted mean.
Decomposition.fold — a value per part, combined over a decomposition.
InFrame — components read in a stated frame.
union_mass, union_centerOfMass, union_inertiaTensor — how mass, centre of mass and inertia combine over a union.
labOmega, bodyOmega, bodyInertia, rotationalContraction — rigid-body quantities indexed by frame.

Carried from earlier steps: Composite, Decomposition, Assembles, assemble, IndividualQuantity, DifferenceKind.ofScale, SortOfSystem, Sorted, Designated, displacementK.

5.4.1.3. Verifiable properties🔗

Body A's centre of mass is the mass-weighted mean of its halves' positions: halves of mass 3 and 5 at positions 0 and 10 give 25/4, not the midpoint 5 (theorem) HCP.L3_TheBodyOpens#center_of_mass_mean.
PhysLib's centerOfMass of a body with zero mass is the origin, because 1/0 = 0 in Lean; body A's carving comes with a proof that its total mass is nonzero (theorem) HCP.L3_TheBodyOpens#massless_center_of_mass.
Angular velocity is equal on both halves and is not a sum over them, and assemble of angular velocity over the halves fails: there is no Assembles rigidBodyS angularVelocityK instance (refused) HCP.L3_TheBodyOpens#angular_velocity_intensive.
rotationalContraction of the body-frame inertia with the lab-frame ω fails with a type mismatch between InFrame lab and InFrame body (refused) HCP.L3_TheBodyOpens#framed_rotational_energy.
With the body-frame ω, the kinded rotational energy equals PhysLib's rotational kinetic energy (theorem) HCP.L3_TheBodyOpens#framed_rotational_energy.
A homogeneous solid sphere of mass m and radius R has moment of inertia (2/5) m R² (theorem) HCP.L3_TheBodyOpens#solid_sphere.

5.4.1.4. Errors prevented🔗

Sum or midpoint instead of weighted mean: body A's centre of mass computed as the sum or the midpoint of its halves' positions (HCP.L3_TheBodyOpens#center_of_mass_mean).
Degenerate whole: a centre of mass reported for a body with zero total mass, which PhysLib returns as the origin (HCP.L3_TheBodyOpens#massless_center_of_mass).
Wrong frame: PhysLib accepts the lab-frame ω in the body-frame energy; with InFrame, it fails to type-check (HCP.L3_TheBodyOpens#bare_frame_mismatch, HCP.L3_TheBodyOpens#framed_rotational_energy).

5.4.2. Persona🔗

You are a PhysLib contributor: a physicist who writes Lean in PhysLib. You know Lean and PhysLib and trust Dimension and WithDim; L0–L2 have established kinds, bearers, and sort-specific assembly licenses.

5.4.3. Pull🔗

Body A of pair P wobbles instead of sliding along the line. Its centre of mass is off the springs' line of action, so the spring force misses the centre of mass, produces a torque, and rotates the body. Body A therefore stops being a point mass: it opens into left and right halves, acquires a mass distribution and inertia tensor, and needs a body-fixed frame beside the lab frame. One name remains one system: records under that name are its states at different times, configurations, or rival estimates; comparing them is the point. Distinct names are distinct systems. HalfOf .P .A keeps body A's halves shared across descriptions of pair P, while a half of pair Q has a different bearer type.

5.4.4. Risks at this step🔗

Wrong carving. For body A of pair P, counting a half twice or leaving one out changes the whole mass; the pinned decomposition gives one slot to each half and proves the total at HCP.L3_TheBodyOpens#opened_body.
Weighted mean, not sum. The centre of mass uses each half's mass and position, while both halves share the same angular velocity; the pinned checks are HCP.L3_TheBodyOpens#center_of_mass_mean and HCP.L3_TheBodyOpens#angular_velocity_intensive.
Degenerate whole and frame. A massless body's centerOfMass evaluates to the origin because Lean defines 1/0 = 0, which is not a physical centre of mass; and lab-frame angular velocity is not the body-frame input to rotational energy; the checks are HCP.L3_TheBodyOpens#massless_center_of_mass, HCP.L3_TheBodyOpens#bare_frame_mismatch, and HCP.L3_TheBodyOpens#framed_rotational_energy.

Further reading

Exhibits/Composition, findings 2 and 5.

5.4.5. Small rigorous improvement🔗

Question	Context change	Attribute change	Risk shown	PhysLib stage
Body A wobbles instead of sliding along the line. Why, and what must the model now say about the body?	Body A of pair P becomes a rigid composite carved into left and right halves; a body-fixed frame appears beside the lab frame.	Per-half mass and position, centre of mass, inertia tensor, and body- versus lab-frame angular velocity.	Counting the wrong halves changes total mass; angular velocity is intensive; a massless body's centre of mass evaluates to the origin, which is not physical; lab-frame angular velocity does not match the body-frame energy input.	Stages 2–3 on rigid bodies; proved solid-sphere inertia theorem.

The L2 on-axis point-mass assumption has fallen. L4 revisits the remaining assumption of motion along one line seen by one observer.

5.4.6. Learning path🔗

#	Do	Checked by `HCP.L3_TheBodyOpens` anchor	Concept disclosed
1	Open body A into left and right halves, index them by pair and body identity, and assemble their masses.	`opened_body`	`HalfOf .P .A` names the bearers; mass assembles to the rigid-body whole, while P and Q remain distinct systems.
2	Weight the half positions by this state's half masses, then try to assemble positions by addition.	`center_of_mass_mean`	`centerOfMass_eq` uses the `OpenBody.mass` and `.position` fields; masses 3 and 5 at positions 0 and 10 give 25/4, not the unit-weight midpoint 5. `rigidBodyS` has no displacement assembly license.
3	Inspect the massless whole and the nonzero-total condition on a weighted carving.	`massless_center_of_mass`	PhysLib reports the origin for zero mass; the license is hypothesis `h`, which a massless state cannot satisfy to build the carving.
4	Check angular velocity over halves and try to assemble it.	`angular_velocity_intensive`	The halves share ω; adding their angular velocities would double it, so no license exists.
5	Pass lab-frame angular velocity to upstream rotational kinetic energy.	`bare_frame_mismatch`	The bare expression type-checks even though the inertia tensor is body-fixed, so the accepted term is physically wrong.
6	Apply PKC's frame-indexed contraction to lab and body angular velocities.	`framed_rotational_energy`	The lab-frame term is refused, the body-frame term is accepted, and the accepted contraction agrees with PhysLib energy.
7	Specialize the old homogeneity assumption to a solid sphere.	`solid_sphere`	The proved inertia tensor is `(2/5) m R² · 1`; upstream records the target as `informal_lemma` `CM-RB-sphereI`.

Worksheet: HCP/Worksheets/L3_TheBodyOpens.lean · Solution: HCP/L3_TheBodyOpens.lean

5.4.7. Lesson🔗

1. Open body A. HalfOf π b adds nominal pair-and-body identity to the upstream left/right Half. OpenBody π b records per-half mass and one position coordinate. The existing Assembles rigidBodyS massK license produces the whole-body total and its magnitude reads the two real fields. Upstream's union theorems state the corresponding mass and inertia-tensor laws. Same-name records share bearers, while P and Q do not:

/--
One pair name is one system. Records under that name describe states, configurations, or
rival estimates of it; distinct names denote distinct systems.
-/
inductive PairId | P | Q
deriving DecidableEq, Repr

inductive Body | A | B
deriving DecidableEq, Repr

def halfS : SortOfSystem := ⟨"half of a rigid body"⟩

structure HalfOf (π : PairId) (b : Body) where
  half : Half
deriving DecidableEq, Repr

instance {π : PairId} {b : Body} : Sorted (HalfOf π b) :=
  ⟨fun _ => halfS⟩

instance {π : PairId} {b : Body} : Designated (HalfOf π b) where
  designation
    | ⟨.left⟩ => ⟨"left half"⟩
    | ⟨.right⟩ => ⟨"right half"⟩
  designation_inj {x y} h := byπ:PairIdb:Bodyx:HalfOf π by:HalfOf π bh:(match x with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match y with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ x = y
    rcases x with ⟨x⟩π:PairIdb:Bodyy:HalfOf π bx:Halfh:(match { half := x } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match y with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := x } = y
    rcases y with ⟨y⟩π:PairIdb:Bodyx:Halfy:Halfh:(match { half := x } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := y } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := x } = { half := y }
    cases xleftπ:PairIdb:Bodyy:Halfh:(match { half := Half.left } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := y } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.left } = { half := y }rightπ:PairIdb:Bodyy:Halfh:(match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := y } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.right } = { half := y } <;>leftπ:PairIdb:Bodyy:Halfh:(match { half := Half.left } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := y } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.left } = { half := y }rightπ:PairIdb:Bodyy:Halfh:(match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := y } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.right } = { half := y } cases yright.leftπ:PairIdb:Bodyh:(match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := Half.left } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.right } = { half := Half.left }right.rightπ:PairIdb:Bodyh:(match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.right } = { half := Half.right } <;>left.leftπ:PairIdb:Bodyh:(match { half := Half.left } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := Half.left } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.left } = { half := Half.left }left.rightπ:PairIdb:Bodyh:(match { half := Half.left } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.left } = { half := Half.right }right.leftπ:PairIdb:Bodyh:(match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := Half.left } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.right } = { half := Half.left }right.rightπ:PairIdb:Bodyh:(match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ { half := Half.right } = { half := Half.right } first | rflAll goals completed! 🐙 | exact absurd (System.mk.inj h) (byπ:PairIdb:Bodyh:(match { half := Half.right } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }) =
  match { half := Half.left } with
  | { half := Half.left } => { id := "left half" }
  | { half := Half.right } => { id := "right half" }⊢ ¬"right half" = "left half" decideAll goals completed! 🐙)

structure OpenBody (π : PairId) (b : Body) where
  mass : Half → ℝ
  position : Half → ℝ

def halfPart (π : PairId) (b : Body) (h : Half) : HalfOf π b := ⟨h⟩

def bodyHalves : Decomposition Half := .union (.atom .left) (.atom .right)

def massOf {π : PairId} {b : Body} (state : OpenBody π b) (h : HalfOf π b) :
    IndividualQuantity
      (Composite.part (σ := rigidBodyS) h)
      massK ℝ :=
  ⟨state.mass h.half⟩

def bodyMass {π : PairId} {b : Body} (state : OpenBody π b) :
    IndividualQuantity
      (Composite.whole : Composite rigidBodyS (HalfOf π b))
      massK ℝ :=
  assemble (k := massK) rigidBodyS
    (Composite.whole : Composite rigidBodyS (HalfOf π b))
    (fun h : Half => Composite.part (σ := rigidBodyS) (halfPart π b h))
    bodyHalves
    (fun h => massOf state (halfPart π b h))

/-- Composition law: Proves that the assembled whole-mass magnitude of a body equals the sum of its left- and right-half masses. -/
theorem bodyMass_magnitude {π : PairId} {b : Body} (state : OpenBody π b) :
    (bodyMass state).magnitude = state.mass .left + state.mass .right := byπ:PairIdb:Bodystate:OpenBody π b⊢ (bodyMass state).magnitude = state.mass Half.left + state.mass Half.right
  rflAll goals completed! 🐙

-- Composition law: Proves that PhysLib's union-mass law is mass(A ∪ B) = mass(A) + mass(B), the additive law used for body A's halves.
example := ForPhysLib.Exhibits.Composition.union_mass

-- Composition law: Proves that PhysLib's union-inertia law is I(A ∪ B) = I(A) + I(B) about a common origin; the theorem's type does not record the axis.
example := ForPhysLib.Exhibits.Composition.union_inertiaTensor

-- Same-name records: Constructs a massK IndividualQuantity about body A's left half in pair P, allowing earlier and later states of that half to be compared.
#guard_msgs in
example (earlier later : OpenBody .P .A) :
    IndividualQuantity
      (Composite.part (σ := rigidBodyS) (halfPart .P .A .left))
      massK ℝ :=
  IndividualQuantity.add DifferenceKind.ofScale
    (massOf later (halfPart .P .A .left))
    (-(massOf earlier (halfPart .P .A .left)))

-- Bearer safety: Refused: type mismatch between body A's left-half mass bearers in pairs P and Q; this prevents treating distinct pairs as one state history.
/--
error: Application type mismatch: The argument
  massOf q (halfPart PairId.Q Body.A Half.left)
has type
  IndividualQuantity (Composite.part (halfPart PairId.Q Body.A Half.left)) massK ℝ
but is expected to have type
  IndividualQuantity (Composite.part (halfPart PairId.P Body.A Half.left)) massK ℝ
in the application
  IndividualQuantity.add ⋯ (massOf p (halfPart PairId.P Body.A Half.left))
    (massOf q (halfPart PairId.Q Body.A Half.left))
-/
#guard_msgs in
example (p : OpenBody .P .A) (q : OpenBody .Q .A) :=
  IndividualQuantity.add DifferenceKind.ofScale
    (massOf p (halfPart .P .A .left))
    (massOf q (halfPart .Q .A .left))

The HCP total is the narrow restatement: upstream union_mass and union_inertiaTensor are about PhysLib's RigidBody, not the nominal HalfOf .P .A bearer.

2. Centre of mass is a weighted mean. Upstream supplies both the rigid-body union law and the general weighted-mean machinery. HCP's centerOfMassCarving uses this state's OpenBody.mass for its weights, and centerOfMass_eq gives the resulting formula. For example, masses 3 and 5 at positions 0 and 10 give 25/4 (6.25), not the unit-weight midpoint 5. HCP's position quantities use the same nominal half bearers as mass, but an attempted sum has no Assembles license:

-- Centre of mass: Proves that with nonzero masses, (mA + mB)·COM(A ∪ B) = mA·COM(A) + mB·COM(B), PhysLib's weighted-mean law.
example := ForPhysLib.Exhibits.Composition.union_centerOfMass

noncomputable def centerOfMassCarving {π : PairId} {b : Body}
    (state : OpenBody π b)
    (h : state.mass .left + state.mass .right ≠ 0) :
    WeightedCarving ℝ Half where
  parts := bodyHalves
  weight := state.mass
  total_ne_zero := byπ:PairIdb:Bodystate:OpenBody π bh:state.mass Half.left + state.mass Half.right ≠ 0⊢ totalWeight state.mass bodyHalves ≠ Carrier.zero
    change state.mass .left + state.mass .right ≠ 0π:PairIdb:Bodystate:OpenBody π bh:state.mass Half.left + state.mass Half.right ≠ 0⊢ state.mass Half.left + state.mass Half.right ≠ 0
    exact hAll goals completed! 🐙

/-- Centre of mass: Proves that a body's two-half carving mean is (mL·xL + mR·xR)/(mL + mR) when total mass is nonzero. -/
theorem centerOfMass_eq {π : PairId} {b : Body} (state : OpenBody π b)
    (h : state.mass .left + state.mass .right ≠ 0) :
    (centerOfMassCarving state h).mean state.position =
      (state.mass .left * state.position .left + state.mass .right * state.position .right) /
        (state.mass .left + state.mass .right) := byπ:PairIdb:Bodystate:OpenBody π bh:state.mass Half.left + state.mass Half.right ≠ 0⊢ (centerOfMassCarving state h).mean state.position =
  (state.mass Half.left * state.position Half.left + state.mass Half.right * state.position Half.right) /
    (state.mass Half.left + state.mass Half.right)
  rflAll goals completed! 🐙

def unequalMassExample : OpenBody .P .A where
  mass
    | .left => 3
    | .right => 5
  position
    | .left => 0
    | .right => 10

/-- Centre of mass: Proves that body A in pair P, with half masses 3 and 5 at positions 0 and 10, has weighted-mean centre 25/4, not midpoint 5. -/
theorem unequalMassExample_centerOfMass :
    (centerOfMassCarving unequalMassExample (by⊢ unequalMassExample.mass Half.left + unequalMassExample.mass Half.right ≠ 0 norm_num [unequalMassExample]All goals completed! 🐙)).mean
      unequalMassExample.position = (25 : ℝ) / 4 := by⊢ (centerOfMassCarving unequalMassExample unequalMassExample_centerOfMass._proof_3).mean unequalMassExample.position =
  25 / 4
  norm_num [centerOfMassCarving, unequalMassExample, WeightedCarving.mean, weightedSum,
    totalWeight, bodyHalves, Decomposition.fold, Carrier.add]All goals completed! 🐙

def positionOf {π : PairId} {b : Body} (state : OpenBody π b) (h : HalfOf π b) :
    IndividualQuantity
      (Composite.part (σ := rigidBodyS) h)
      ForPhysLib.ClassicalMechanics.displacementK ℝ :=
  ⟨state.position h.half⟩

-- Centre of mass: Refused: no Assembles rigidBodyS displacementK instance; the halves' positions form a mass-weighted mean, not an additive total.
/--
error: failed to synthesize instance of type class
  Assembles rigidBodyS ForPhysLib.ClassicalMechanics.displacementK

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example {π : PairId} {b : Body} (state : OpenBody π b) :=
  assemble (k := ForPhysLib.ClassicalMechanics.displacementK) rigidBodyS
    (Composite.whole : Composite rigidBodyS (HalfOf π b))
    (fun h : Half => Composite.part (σ := rigidBodyS) (halfPart π b h))
    bodyHalves
    (fun h => positionOf state (halfPart π b h))

The physical content is (mA + mB) com = mA comA + mB comB, not com = comA + comB.

3. The degenerate whole. PhysLib defines the massless body's centre of mass to be the origin by convention. The license to build centerOfMassCarving is hypothesis h, that the state's total mass is nonzero; a massless state cannot satisfy it, so it cannot build the carving:

-- Centre of mass: proves that a massless body's `centerOfMass` is the origin, because PhysLib computes (1 / mass) • … and Lean's 1 / 0 = 0.
example := ForPhysLib.Exhibits.Composition.massless_centerOfMass

-- Centre of mass: Proves that the two mass-weighted halves have total weight 2 ≠ 0, supplying the license for their weighted mean.
example := ForPhysLib.Exhibits.Composition.halvesByMass_total_ne_zero

4. Angular velocity is intensive. The two rigid halves share one angular velocity; adding their measurements would double it. The upstream finding proves the intensive law and refutes extensivity, while the HCP attempted assembly is rejected:

-- Composition law: Proves that angular velocity is intensive: each rigid-body half reads 7 rad/s rather than receiving a share of a total.
example := ForPhysLib.Exhibits.Composition.omegaOfHalf_intensive

-- Composition law: Proves that angular velocity is not extensive across the rigid body's halves: both read 7 rad/s, not a summed 14 rad/s.
example := ForPhysLib.Exhibits.Composition.omegaOfHalf_not_extensive

-- Licensed composition: Refused: no Assembles rigidBodyS angularVelocityK instance; angular velocity is constant across parts, not an additive total.
/--
error: failed to synthesize instance of type class
  Assembles rigidBodyS angularVelocityK

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example :=
  fun {π : PairId} {b : Body}
      (ω : (h : Half) →
        IndividualQuantity
          (Composite.part (σ := rigidBodyS) (halfPart π b h))
          angularVelocityK ℝ) =>
    assemble (k := angularVelocityK) rigidBodyS
      (Composite.whole : Composite rigidBodyS (HalfOf π b))
      (fun h : Half => Composite.part (σ := rigidBodyS) (halfPart π b h))
      bodyHalves ω

5. Upstream frames. PhysLib's bare rotational-energy API accepts the lab-frame M.angularVelocity t against the body-fixed inertia tensor. The term below type-checks, but it is physically wrong:

-- Frame safety: The bare ℝ example accepts rotational energy from M's body inertia and lab-frame ω; it erases frame and motion bearer, hiding the invalid mix.
noncomputable example (M : RigidBodyMotion 3) (t : Time) : ℝ :=
  M.toRigidBody.rotationalKineticEnergy (M.angularVelocity t)

6. PKC frames. rotationalContraction retains the frame in the type. Lab-frame ω is therefore refused, body-frame ω is accepted, and the bridge theorem equates the accepted components with twice PhysLib's own rotational kinetic energy:

-- Frame safety: Refused: type mismatch between lab-frame ω and the body-frame ω required by contraction; this prevents pairing body inertia with lab angular velocity.
/--
error: Application type mismatch: The argument
  ForPhysLib.Exhibits.RigidBody.labOmega M t
has type
  InFrame ForPhysLib.Exhibits.RigidBody.lab Variance.vector ForPhysLib.Exhibits.RigidBody.angularVelocityK (Fin 3 → ℝ)
but is expected to have type
  InFrame ForPhysLib.Exhibits.RigidBody.body Variance.vector ForPhysLib.Exhibits.RigidBody.angularVelocityK (Fin 3 → ℝ)
in the application
  ForPhysLib.Exhibits.RigidBody.rotationalContraction ForPhysLib.Exhibits.RigidBody.inertia_mul_angularVelocity
    ForPhysLib.Exhibits.RigidBody.angularVelocity_mul_angularMomentum (ForPhysLib.Exhibits.RigidBody.bodyInertia M)
    (ForPhysLib.Exhibits.RigidBody.labOmega M t)
-/
#guard_msgs in
noncomputable example (M : RigidBodyMotion 3) (t : Time) :=
  ForPhysLib.Exhibits.RigidBody.rotationalContraction
    ForPhysLib.Exhibits.RigidBody.inertia_mul_angularVelocity
    ForPhysLib.Exhibits.RigidBody.angularVelocity_mul_angularMomentum
    (ForPhysLib.Exhibits.RigidBody.bodyInertia M)
    (ForPhysLib.Exhibits.RigidBody.labOmega M t)

-- Frame safety: Constructs a bearer-free body-frame kineticEnergyK scalar from M's body-frame inertia and angular velocity; the result retains frame and kind, not M.
noncomputable example (M : RigidBodyMotion 3) (t : Time) :
    InFrame ForPhysLib.Exhibits.RigidBody.body .scalar
      ForPhysLib.Exhibits.RigidBody.kineticEnergyK ℝ :=
  ForPhysLib.Exhibits.RigidBody.rotationalContraction
    ForPhysLib.Exhibits.RigidBody.inertia_mul_angularVelocity
    ForPhysLib.Exhibits.RigidBody.angularVelocity_mul_angularMomentum
    (ForPhysLib.Exhibits.RigidBody.bodyInertia M)
    (ForPhysLib.Exhibits.RigidBody.bodyOmega M t)

-- Frame safety: Proves that body-frame rotational contraction equals PhysLib's rotational kinetic energy for the motion's body-frame angular velocity.
example := ForPhysLib.Exhibits.RigidBody.rotationalContraction_eq_physlib

7. Homogeneity returns as a special case. For a nonzero-radius solid sphere, the proved inertia tensor is (2/5) m R² times the identity matrix:

-- Inertia tensor: Proves that the 3D solid sphere's inertia tensor is (2/5) m R² times the identity matrix.
example := ForPhysLib.ClassicalMechanics.SolidSphereInertia.solidSphere_inertiaTensor

PhysLib records this target as informal_lemma CM-RB-sphereI. The proof in ForPhysLib.ClassicalMechanics.SolidSphereInertia is therefore a ready first upstream contribution for the PhysLib contributor. L4 next revisits motion along one line seen by one observer.

5.4.8. AI assistance contract🔗

Define L3-local PairId and Body: the preceding lesson modules are independent rather than importing one another.
Reuse the ForPhysLib findings directly when their upstream bearers already express the claim; restate only the HCP-specific half bearers and the refused assembly probes.
Preserve nominal identity: same-name records share bearers, while P and Q do not.
Treat Assembles as an explicit physical license, not a generic arithmetic operation.
Make the weighted-mean license the state's nonzero total mass; do not substitute unit weights.
Keep the body- and lab-frame indices visible in rotational expressions.
Label the accepted upstream lab-ω expression physically wrong even though Lean accepts it.
Leave the one-dimensional, one-observer assumption for L4.

5.4.9. Questions to ask the model so far🔗

Question	Check	What the verdict means
What bears the mass of body A's left half?	`opened_body`	`Composite.part (HalfOf .P .A)` bears it; the body whole bears the assembled total.
Can another record of body A in pair P use the same bearer?	`opened_body`	Yes; it is another state, configuration, or estimate of the named system.
Can pair Q's left-half mass be mixed with pair P's?	`opened_body`	No; nominal pair identities produce distinct bearer types.
How does this state's centre of mass depend on its halves?	`center_of_mass_mean`	`centerOfMassCarving` uses the actual half masses; 3 at 0 and 5 at 10 yield 25/4 rather than 5. Position addition is unlicensed.
What happens when total mass is zero?	`massless_center_of_mass`	PhysLib returns the origin by convention, but hypothesis `h` fails, so the state cannot construct a weighted carving.
Does angular velocity add over a carving?	`angular_velocity_intensive`	No; it is intensive, and the attempted assembly is refused.
Can the body inertia tensor contract with lab-frame ω?	`bare_frame_mismatch`, `framed_rotational_energy`	The bare PhysLib API accepts it, but the PKC frame index refuses it.
Where does the homogeneous-body assumption survive?	`solid_sphere`	As the solid-sphere theorem `(2/5) m R² · 1`, ready to contribute upstream.

5.4.10. System-context card🔗

Scope	System or component	Sort / status	L3 assumptions and attributes
System	Coupled pair P	Nominal `PairId.P`	The L2 coupled pair remains the named system; records under P may describe different states, configurations, or estimates.
Part	Body A	Rigid body in pair P	No longer point-like or homogeneous; carved into left and right halves with per-half mass and position.
Part	Left half of A	`HalfOf .P .A`	Mass-bearing rigid-body part, designated “left half.”
Part	Right half of A	`HalfOf .P .A`	Mass-bearing rigid-body part, designated “right half.”
Attribute	Centre of mass	Weighted mean	Uses each state's half masses and positions; defined only under nonzero-total hypothesis `h`. Masses 3 and 5 at positions 0 and 10 give 25/4. An off-axis value makes the spring force produce torque.
Attribute	Inertia tensor	Body-fixed tensor	The union theorem adds part tensors about a common origin; the solid sphere is the homogeneous special case.
Attribute	Angular velocity	Lab or body frame	Intensive over rigid halves; rotational contraction requires the body-frame value.
Outside / deferred	Observer and full 3-D motion	L4	L3 introduces two frames but still defers the one-observer, one-line assumption to L4.

The HCP bearer is narrower than the upstream RigidBody theorems: HalfOf π b adds nominal pair-and-body identity. The mass total, state-dependent weighted mean, and refused assembly probes are therefore stated over HCP bearers. The physical union, massless, intensive-ω, frame-bridge, and solid-sphere results are reused directly from ForPhysLib.