A Property Kind Calculus for Measurement Metrology

16.5. Assembly over a composite🔗

Gating on the object refuses a sum across two objects, which is what it is for — and it refuses, with equal correctness, the total mass of an assembly, because the total characterizes an object the part type does not contain. Aggregation therefore needs an eliminator, and the eliminator is where the §13.5 license enters.

Three decisions shape the eliminator, each an application of the unite/unify distinction the foundations chapter states: the whole is added rather than derived, because no carving yields it; the same parts under two sorts (the foundations chapter) are two object types with two sets of licenses, because the statue and the lump are two wholes; and the license is indexed by the sort rather than by the kind alone, because how parts make a whole is settled by what the whole is — the one claim the parts cannot make on their own behalf.

Definition16.5.1
Group: The object of an individual quantity (the foundations chapter's mode) ranges over an arbitrary type. The gate needs nothing from it; the designation needs Designated , whose injectivity field is what distinguishes a designation from a formality. (7)
Group member previews
Preview
Definition 16.3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

The composite object type over a part type, as a sort of whole: the whole, or one of its parts. The whole and the parts must inhabit one type or their quantities cannot be related at all; the whole is a distinct term from every part, so a whole-assembly quantity and a part quantity do not combine. The sort index is what lets two wholes stand over one part type — the statue and the lump over the same clay — and their quantities do not combine either, because the types differ. Extensionality about objects is not assumed.

Lean code for Definition16.5.1●1 definition
  • inductive(2 constructors, 2 parameters)defined in PropertyKindCalculus/Composite.lean
    complete
    inductive PropertyKindCalculus.Composite.{u}
  (σ : PropertyKindCalculus.SortOfSystem) (P : Type u) : Type u
    inductive PropertyKindCalculus.Composite.{u}
  (σ : PropertyKindCalculus.SortOfSystem)
  (P : Type u) : Type u
    **The object type of a composite** — the whole, or one of its parts.

The construct `MR22` asks for and the one a structural object type (physlib's particles, a
mesh's cells) does not supply on its own: a particle type contains particles and no
assembly, so a total mass has nowhere to live. `Composite P` adds exactly one inhabitant,
and it is *distinct as a term* from every part, which is the whole mechanism — a
whole-system quantity and a part quantity do not add, definitionally, with nothing to
prove and nothing to enforce.

    Constructors

    PropertyKindCalculus.Composite.whole.{u}
  {σ : PropertyKindCalculus.SortOfSystem} {P : Type u} :
  PropertyKindCalculus.Composite σ P
    The assembly itself — the bearer of whole-composite quantities. 
    PropertyKindCalculus.Composite.part.{u}
  {σ : PropertyKindCalculus.SortOfSystem} {P : Type u}
  (p : P) : PropertyKindCalculus.Composite σ P
    One part of the assembly, *read as composing this sort of whole*. The bare `p` (at the
object type `P` itself) remains the part simpliciter; `Composite.part p` is the part in its
compositional role, which is why the sort reaches it.
Proof for Definition 16.5.1
uses 0

A two-constructor inductive with DecidableEq and Repr, indexed by the sort and the part type. Naming a composite is a definition rather than an instance, taking the whole's name and the proof that no part already answers to it — a terminological commitment instance search has no business guessing.

Definition16.5.2
Group: The object of an individual quantity (the foundations chapter's mode) ranges over an arbitrary type. The gate needs nothing from it; the designation needs Designated , whose injectivity field is what distinguishes a designation from a formality. (7)
Group member previews
Preview
Definition 16.3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

The assembly license, keyed by the sort of the whole and the kind: which kinds' part quantities may be summed into a quantity of that sort of whole. Registration is opt-in, and the entry carries the same scale gate addition demands, so a nominal or ordinal kind cannot be licensed at all.

Lean code for Definition16.5.2●1 definition
  • class(1 method)defined in PropertyKindCalculus/Composite.lean
    complete
    class PropertyKindCalculus.Assembles (σ : PropertyKindCalculus.SortOfSystem)
  (k : PropertyKindCalculus.KindOfProperty) : Prop
    class PropertyKindCalculus.Assembles
  (σ : PropertyKindCalculus.SortOfSystem)
  (k :
    PropertyKindCalculus.KindOfProperty) :
  Prop
    **The aggregation license (§13.5, curated) — keyed by the sort of the whole.** A kind
whose quantities may be summed over the parts of a composite *of the given sort* to give the
quantity of the whole. Mass carries it for every sort a mechanical model declares; angular
velocity deliberately carries it for none, and the sum of the parts' angular velocities is
then not a term anyone can write.

The sort index is not decoration, and the library's own counterexample is why: **volume**.
Over the parts of a rigid assembly, volume aggregates; over the parts of a mixture it
contracts (`mixing_subadditive` — 50 mL of ethanol and 50 mL of water make 96 mL), and both
facts are facts about *volume*. A registry keyed by the kind alone must either license the
mixture or refuse the assembly, and either answer is wrong. Keyed by the sort, both answers
are right at once — which is the neo-Aristotelian point that how parts unify into a whole is
dictated by the *sort* of the whole, not by the attribute being summed and not by the parts.

Registration is opt-in — an unregistered pair has no instance and `assemble` does not
elaborate — and the entry is not a formality: its `diff` field is the same scale gate
`Quantity.add` demands, so a nominal or ordinal kind cannot be licensed at all. What the
class does *not* prove is that the sum is the physics; that is a fact about a measurement,
and `assemble_eq_measured` is where an author discharges it, per sort.

    Methods

    diff : PropertyKindCalculus.DifferenceKind k
    `k`'s scale licenses the sum the assembly is built from — interval or ratio.
Proof for Definition 16.5.2
uses 0

A Prop-valued class with one field, a DifferenceKind witness. The sort index is forced by the library's own counterexample: volume aggregates over the parts of a rigid assembly and contracts over the parts of a mixture (mixing_subadditive), and both facts are facts about volume — a registry keyed by the kind alone must either license the mixture or refuse the assembly, and either answer is wrong. The validation suite carries both verdicts side by side, each backed by its witness: an Extensive measurement for the rigid sort, the ethanol/water contraction for the mixture.

Definition16.5.3
Group: The object of an individual quantity (the foundations chapter's mode) ranges over an arbitrary type. The gate needs nothing from it; the designation needs Designated , whose injectivity field is what distinguishes a designation from a formality. (7)
Group member previews
Preview
Definition 16.3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Assembly: the quantity of the whole, folded from the quantities of the parts over a carving. The whole and the part injection are arguments rather than fixed, so the eliminator serves a composite and equally a host library's own object type with its own naming of parts. Its part function is dependent — the quantity supplied for a part must characterize that part — which is the gate.

Lean code for Definition16.5.3●1 definition
  • defdefined in PropertyKindCalculus/Composite.lean
    complete
    def PropertyKindCalculus.assemble.{u, v} {O : Type u} {P : Type v}
  {k : PropertyKindCalculus.KindOfProperty} {R : Type}
  [PropertyKindCalculus.Carrier R]
  (σ : PropertyKindCalculus.SortOfSystem)
  [PropertyKindCalculus.Assembles σ k] (whole : O) (part : P → O)
  (d : PropertyKindCalculus.Decomposition P)
  (f : (p : P) → PropertyKindCalculus.IndividualQuantity (part p) k R) :
  PropertyKindCalculus.IndividualQuantity whole k R
    def PropertyKindCalculus.assemble.{u, v}
  {O : Type u} {P : Type v}
  {k :
    PropertyKindCalculus.KindOfProperty}
  {R : Type}
  [PropertyKindCalculus.Carrier R]
  (σ : PropertyKindCalculus.SortOfSystem)
  [PropertyKindCalculus.Assembles σ k]
  (whole : O) (part : P → O)
  (d :
    PropertyKindCalculus.Decomposition P)
  (f :
    (p : P) →
      PropertyKindCalculus.IndividualQuantity
        (part p) k R) :
  PropertyKindCalculus.IndividualQuantity
    whole k R
    **Assembly — the quantity of the whole from the quantities of its parts, as a sort of
whole.**

The sort `σ` says *what kind of whole* is being composed, and it is the index the license is
looked up at — assembling the same parts as a different sort of whole is a different act, with
its own licenses (rigid assembly versus mixture is the canonical split). The whole `whole` and
the part-injection `part` are arguments, so this serves a bespoke `Composite P`
(`assemble σ .whole .part`) and equally a host library's own object type with its own
naming of parts (`assemble σ rover (partOf rover)`). `f` is *dependent*: the quantity
supplied for `p` must characterize `part p`, which is the gate — a part's quantity cannot
be smuggled in under another part's name.

The traversal is `Decomposition.fold`, the same one `leafSum` uses, so the arithmetic here
and the §13.5 law are one recursion read at two carriers rather than two that agree.
Proof for Definition 16.5.3
uses 0

Decomposition.fold of the parts' magnitudes under Carrier.add: the same traversal leafSum uses, so the quantity-level arithmetic and the §13.5 law are one recursion read at two carriers. The counterpart over a finite index (assembleOver, assembleAll) sums a Finset instead, which is the shape a host library's own aggregate is written in — a Finset.sum, recovered by rfl rather than by a rewriting lemma.

Theorem16.5.4
Group: The object of an individual quantity (the foundations chapter's mode) ranges over an arbitrary type. The gate needs nothing from it; the designation needs Designated , whose injectivity field is what distinguishes a designation from a formality. (7)
Group member previews
Preview
Definition 16.3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
EffortsmallTagsproved

The license refused. For a whole-proper kind — one whose value the parts do not determine, in either of the two ways they could — there is a carving on which the assembled magnitude is not the value the whole has. Not merely unjustified: wrong, on an exhibited pair of parts. Uses assembly.

Lean code for Theorem16.5.4●1 theorem
  • theoremdefined in PropertyKindCalculus/Composite.lean
    complete
    theorem PropertyKindCalculus.assemble_ne_measured.{u, v} {O : Type u}
  {P : Type v} {k : PropertyKindCalculus.KindOfProperty}
  (σ : PropertyKindCalculus.SortOfSystem)
  [PropertyKindCalculus.Assembles σ k] (whole : O) (part : P → O)
  {m : PropertyKindCalculus.Measurement P}
  (h : PropertyKindCalculus.WholeProper k m) :
  ∃ d,
    (PropertyKindCalculus.assemble σ whole part d fun p =>
          {
            magnitude :=
              (m
                  (PropertyKindCalculus.Decomposition.atom
                    p)).numeral }).magnitude ≠
      (m d).numeral
    theorem PropertyKindCalculus.assemble_ne_measured.{u,
    v}
  {O : Type u} {P : Type v}
  {k :
    PropertyKindCalculus.KindOfProperty}
  (σ : PropertyKindCalculus.SortOfSystem)
  [PropertyKindCalculus.Assembles σ k]
  (whole : O) (part : P → O)
  {m : PropertyKindCalculus.Measurement P}
  (h :
    PropertyKindCalculus.WholeProper k
      m) :
  ∃ d,
    (PropertyKindCalculus.assemble σ whole
          part d fun p =>
          {
            magnitude :=
              (m
                  (PropertyKindCalculus.Decomposition.atom
                    p)).numeral }).magnitude ≠
      (m d).numeral
    **The license refused.** For a *whole-proper* kind — one whose
value the parts do not determine, in either of the two ways they could — there is a carving
on which the assembled magnitude is **not** the value the whole has. Not merely unjustified:
wrong, on an exhibited pair of parts.

The `[Assembles σ k]` instance is still required, and that is the finding. The class licenses
the sum to be *written*; nothing about writing it makes it true, so an author who registers a
whole-proper kind gets a term that elaborates and a number that is not the physics. This is
the negative counterpart of `assemble_eq_measured` — same eliminator, same measurement, the
`Extensive` hypothesis replaced by its refutation — and it is why the registry is opt-in and
its entries are curated per sort.
Proof for Theorem 16.5.4
uses 0

The Assembles instance is still required, and that is the finding: the class licenses the sum to be written, and nothing about writing it makes it true, so an author who registers a whole-proper kind gets a term that elaborates and a number that is not the physics. The witness's own non-additive pair supplies the carving; the negative twin of assemble_eq_measured, same eliminator and same measurement, with the extensivity hypothesis replaced by its refutation. This is why the registry is opt-in and curated per sort rather than derived.

16.5.1. Two sums, and only the object tells them apart🔗

A sum of quantities appears in applied models in two shapes that are identical on the page.

A resultant combines several quantities of one object and one kind into one of the same object and kind: the forces acting on a particle, the currents into a node. Nothing about the object changes, so nothing beyond the scale gate addition already demands is needed.

An assembly combines the quantities of the parts into a quantity of the whole. The object changes, and whether that is meaningful at all is a fact about the kind — which is what the license records.

Summing the particles' velocities is refused because it is an assembly of an unlicensed kind. Summing the forces on one particle must not be refused, because it is not an assembly. A layer that indexes quantities only by kind writes both with the same ∑ at the same type and can refuse neither; this is the clearest single thing the object index buys, and the PointParticle case study scores four designs on exactly it.

Theorem16.5.1.1
Group: The object of an individual quantity (the foundations chapter's mode) ranges over an arbitrary type. The gate needs nothing from it; the designation needs Designated , whose injectivity field is what distinguishes a designation from a formality. (7)
Group member previews
Preview
Definition 16.3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortmediumTagscapstoneproved

The license, cashed. For a kind that is genuinely extensive under a measurement, the assembled magnitude over any decomposition is the value that measurement reports for the whole. This is what makes the license a claim about the world rather than a permission slip: the class licenses the sum to be written, and this theorem is what shows the sum is right. Volume on mixing has no Extensive witness, so it has no instance of this.

Lean code for Theorem16.5.1.1●1 theorem
  • theoremdefined in PropertyKindCalculus/Composite.lean
    complete
    theorem PropertyKindCalculus.assemble_eq_measured.{u, v} {O : Type u}
  {P : Type v} {k : PropertyKindCalculus.KindOfProperty}
  (σ : PropertyKindCalculus.SortOfSystem)
  [PropertyKindCalculus.Assembles σ k] (whole : O) (part : P → O)
  {m : PropertyKindCalculus.Measurement P}
  (h : PropertyKindCalculus.Extensive k m)
  (d : PropertyKindCalculus.Decomposition P) :
  (PropertyKindCalculus.assemble σ whole part d fun p =>
        {
          magnitude :=
            (m
                (PropertyKindCalculus.Decomposition.atom
                  p)).numeral }).magnitude =
    (m d).numeral
    theorem PropertyKindCalculus.assemble_eq_measured.{u,
    v}
  {O : Type u} {P : Type v}
  {k :
    PropertyKindCalculus.KindOfProperty}
  (σ : PropertyKindCalculus.SortOfSystem)
  [PropertyKindCalculus.Assembles σ k]
  (whole : O) (part : P → O)
  {m : PropertyKindCalculus.Measurement P}
  (h : PropertyKindCalculus.Extensive k m)
  (d :
    PropertyKindCalculus.Decomposition
      P) :
  (PropertyKindCalculus.assemble σ whole
        part d fun p =>
        {
          magnitude :=
            (m
                (PropertyKindCalculus.Decomposition.atom
                  p)).numeral }).magnitude =
    (m d).numeral
    **The license, cashed (§13.5).** When the kind really is extensive under a measurement
`m`, the assembled magnitude over any decomposition **is** the value `m` reports for the
whole — the quantity-level eliminator and Dybkær's aggregation law computing the same
number, by `extensive_additive`.

This is what makes `Assembles` a claim about the world rather than a permission slip: the
class licenses the sum to be *written*, and this theorem is what an author shows to say the
sum is *right*. Its absence is exactly the volume-on-mixing case — `volMix` has no
`Extensive` witness, so no instance of this theorem exists for it.
Proof for Theorem 16.5.1.1
uses 0

extensive_additive applied to the decomposition, symmetrized: the assembled magnitude is leafSum by definitional unfolding of the shared fold, and leafSum is the whole's measured numeral by the aggregation capstone.