15.4. Aggregating about a shared parameter🔗

Some quantities add only relative to something the parts must share — a moment of inertia about a common axis, an energy about a common datum. A Measurement reads a carving and nothing else, so the parameter is made an explicit argument; what that buys is not a weaker law but a statable one, about the case a library that forgets the axis actually hits.

The parameter is kind-specific — an axis for a moment of inertia, a frame for a momentum, a reference point for an angular momentum — and the transports relating two parameter values form a tower: each correction is priced in a summary that is itself extensive one rung down, grounding out in mass. The worked witness is a rover (RoverExtensivity, examples): whether its four wheels' spins, each read about its own axle, may be summed against the chassis is decided by the priced correction — each assembly's momentum — which vanishes parked and does not while driving.

Definition15.4.1

Group: Mass is extensive: the mass of a whole is the sum of the masses of its parts. Volume on mixing is not: ethanol and water mix sub-additively. Tracking which kinds are extensive is a precondition for soundly aggregating measurements. (30)

Group member previews

Preview

Definition 15.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 15.4.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

A kind is extensive about a parameter when fixing the parameter — an axis, an origin, a datum — makes the ordinary additivity law hold. This is extensivity at every parameter at once, not a weakening of it, which is what makes the mixed-parameter statement a claim about the predicate rather than about one lucky choice.

Lean code for Definition15.4.1●1 definition

structure(2 fields)defined in PropertyKindCalculus/Extensivity.lean

complete

structure PropertyKindCalculus.ExtensiveAbout.{u} {A : Type} {O : Type u}
  (k : PropertyKindCalculus.KindOfProperty)
  (m : PropertyKindCalculus.ParamMeasurement A O) : Prop

structure PropertyKindCalculus.ExtensiveAbout.{u}
  {A : Type} {O : Type u}
  (k :
    PropertyKindCalculus.KindOfProperty)
  (m :
    PropertyKindCalculus.ParamMeasurement
      A O) :
  Prop

**§13.5.1 relative to a parameter.** `k` is extensive *about* each value of `A`: fix the
axis and the ordinary additivity law holds. Every parameter at once — which is what makes the
mixed-parameter statement below a statement about this predicate rather than about one
lucky choice.

Fields

ofKind : ∀ (a : A) (d : PropertyKindCalculus.Decomposition O), (m a d).kind = k

Every measured part is a value of the kind `k`, about every parameter.

additive : ∀ (a : A) (d₁ d₂ : PropertyKindCalculus.Decomposition O),
  (m a (d₁.union d₂)).numeral = (m a d₁).numeral + (m a d₂).numeral

The single-split additivity law, at a fixed parameter.

Proof for Definition 15.4.1

uses 0

Realized as ExtensiveAbout k m over a ParamMeasurement, with ExtensiveAbout.at recovering Extensive k (m a) at each parameter so both §13.5 capstones apply unchanged. Its companion Transports carries the correction as an argument rather than defining it as the difference: a transport law is useful only when the correction is computable from data the part already carries.

Theorem15.4.2

Group member previews

Preview

Definition 15.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

EffortmediumTagscapstoneproved

The parallel-axis theorem, over any carving. The moment of inertia about a is the moment about b plus a correction built from the carving's own first moment and total mass, I_a = I_b + 2(b-a)\sum_i w_i x_i + (a^2 - b^2)\sum_i w_i. Both summaries are themselves extensive over the same carving, which is why this is a metrological statement and not only an algebraic identity: transporting an aggregate costs only quantities the parts already carry. Taking b at the centre of mass kills the first moment and leaves the textbook M d^2. Builds on extensivity about a parameter.

Lean code for Theorem15.4.2●1 theorem

theoremdefined in PropertyKindCalculus/AggregationLaws.lean

complete

theorem PropertyKindCalculus.parallelAxis.{u} {O : Type u} (w x : O → ℤ)
  (a b : ℤ) (d : PropertyKindCalculus.Decomposition O) :
  PropertyKindCalculus.inertiaAbout w x a d =
    PropertyKindCalculus.inertiaAbout w x b d +
      (2 * (b - a) * PropertyKindCalculus.firstMoment w x d +
        (a * a - b * b) * PropertyKindCalculus.partTotal w d)

theorem PropertyKindCalculus.parallelAxis.{u}
  {O : Type u} (w x : O → ℤ) (a b : ℤ)
  (d :
    PropertyKindCalculus.Decomposition
      O) :
  PropertyKindCalculus.inertiaAbout w x a
      d =
    PropertyKindCalculus.inertiaAbout w x
        b d +
      (2 * (b - a) *
          PropertyKindCalculus.firstMoment
            w x d +
        (a * a - b * b) *
          PropertyKindCalculus.partTotal w
            d)

**The parallel-axis theorem, over any carving of any part type.** The moment of inertia
about `a` is the moment about `b` plus a correction built from the carving's *first moment*
and its *total mass* — two extensive summaries of the same parts. Taking `b` at the centre of
mass makes the first moment vanish and leaves the textbook `M d²`.

Proved by induction on the carving: at a leaf it is `ring` on
`w·(x−a)² = w·(x−b)² + 2(b−a)·w·x + (a²−b²)·w`, and at a join the three folds distribute.

Proof for Theorem 15.4.2

uses 0

By induction on the carving: at a leaf it is ring normalization of w(x-a)^2 = w(x-b)^2 + 2(b-a)wx + (a^2-b^2)w, and at a join the three folds distribute. The Int ring arithmetic is why it lives in the Mathlib-backed AggregationLaws rather than the core. What the core exhibits is the failure it corrects: two point masses read about axes through themselves contribute nothing each, where the rod about its centre reads 2.

Theorem15.4.3

Group member previews

Preview

Definition 15.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

EffortsmallTagsproved

A momentum transports between frames, priced in mass. The momentum read in the frame at u_1 is the momentum read at u_2 plus the carving's mass times the frame difference, p_{u_1} = p_{u_2} + \Bigl(\sum_i w_i\Bigr)(u_2 - u_1). The parameter of extensivity about a parameter is a frame here rather than an axis, and the failure it prices is reading each part in its own rest frame: every reading is zero, so the untransported sum reports a system with no momentum at all.

Lean code for Theorem15.4.3●1 theorem

theoremdefined in PropertyKindCalculus/AggregationLaws.lean

complete

theorem PropertyKindCalculus.momentumBoost.{u} {O : Type u} (w v : O → ℤ)
  (u₁ u₂ : ℤ) (d : PropertyKindCalculus.Decomposition O) :
  PropertyKindCalculus.momentumIn w v u₁ d =
    PropertyKindCalculus.momentumIn w v u₂ d +
      PropertyKindCalculus.partTotal w d * (u₂ - u₁)

theorem PropertyKindCalculus.momentumBoost.{u}
  {O : Type u} (w v : O → ℤ) (u₁ u₂ : ℤ)
  (d :
    PropertyKindCalculus.Decomposition
      O) :
  PropertyKindCalculus.momentumIn w v u₁
      d =
    PropertyKindCalculus.momentumIn w v u₂
        d +
      PropertyKindCalculus.partTotal w d *
        (u₂ - u₁)

**The Galilean boost, as a transport law**: the momentum read in the frame at `u₁` is the
momentum read at `u₂` plus the carving's mass times the frame difference — the correction is
the one unconditionally extensive summary there is, which is the tower's ground floor.

Proof for Theorem 15.4.3

uses 0

By induction on the carving: ring at a leaf on w(v-u_1) = w(v-u_2) + w(u_2-u_1), folds distributing at a join. The core exhibits the failure (drift_rest_frames_wrong: two drifting masses read 0 in their own rest frames where the laboratory reads the pair at 3) and drift_rest_frames_corrected closes the gap from the general law, with the two corrections being the parts' own laboratory momenta.

Theorem15.4.4

Group member previews

Preview

Definition 15.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 15.4.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsproved

An angular momentum transports between reference points, priced in momentum. Componentwise over any carving, L_a = L_b + (b - a) \times p, with the momentum components entering as the first moments of the velocities. This is the middle rung of the transport tower: inertia's correction is priced in mass and first moment, this one in momentum, and momentum's in mass — each price itself extensive one rung down, so mixed-parameter aggregation is checkable all the way to the ground.

Lean code for Theorem15.4.4●1 theorem

theoremdefined in PropertyKindCalculus/AggregationLaws.lean

complete

theorem PropertyKindCalculus.angularMomentumTransport.{u} {O : Type u}
  (w x y vx vy : O → ℤ) (a b : ℤ × ℤ)
  (d : PropertyKindCalculus.Decomposition O) :
  PropertyKindCalculus.angularMomentumAbout w x y vx vy a d =
    PropertyKindCalculus.angularMomentumAbout w x y vx vy b d +
      ((b.1 - a.1) * PropertyKindCalculus.firstMoment w vy d -
        (b.2 - a.2) * PropertyKindCalculus.firstMoment w vx d)

theorem PropertyKindCalculus.angularMomentumTransport.{u}
  {O : Type u} (w x y vx vy : O → ℤ)
  (a b : ℤ × ℤ)
  (d :
    PropertyKindCalculus.Decomposition
      O) :
  PropertyKindCalculus.angularMomentumAbout
      w x y vx vy a d =
    PropertyKindCalculus.angularMomentumAbout
        w x y vx vy b d +
      ((b.1 - a.1) *
          PropertyKindCalculus.firstMoment
            w vy d -
        (b.2 - a.2) *
          PropertyKindCalculus.firstMoment
            w vx d)

**An angular momentum transports between reference points, priced in momentum**:
`L_a = L_b + (b − a) × p`, componentwise over any carving, with the momentum components as
the first moments of the velocities. Taking `b` at a part's own mass centre and `a` at the
system's shows the split of an angular momentum into spin and orbital terms is this law and
not a new principle — and a part whose momentum vanishes reads the same about every point,
which is why a parked flywheel's spin may be summed untransported and a translating one's
may not.

Proof for Theorem 15.4.4

uses 0

By induction on the carving, ring at a leaf. Taking b at a part's own mass centre and a at the system's shows the spin/orbital split of an angular momentum is this law and not a new principle, and a part whose momentum vanishes reads the same about every point. The rover instantiates both readings: each wheel's spin reads 2 about its own axle, parked or driving; parked, every assembly's momentum vanishes and the four spins sum against the chassis unchanged, while driving each transport costs −15 and the untransported sum misses the whole by exactly the four prices.