15.5. The interface ledger — what parts exert across a cut
Every measurement above reads a node of a carving. A drive torque on a hub, a contact force
at a joint, the heat crossing a wall read no node at all: each is indexed by an ordered pair
of parts — an interface — and a Measurement has no slot for a pair. The ledger is that slot,
and its one law is the reason such quantities nonetheless aggregate.
An interface ledger over the parts of a carving is a pairwise action carrying its cancellation law as a field: the two readings of one interface sum to zero — for mechanical actions, Newton's third law. A pair of readings that does not cancel is not two readings of one interface, so the obligation is a field for the reason a re-carving's whole-preservation is.
Lean code for Definition15.5.1●1 definition
Associated Lean declarations
-
PropertyKindCalculus.InterfaceLedger[complete]
-
PropertyKindCalculus.InterfaceLedger[complete]
-
structuredefined in PropertyKindCalculus/InterfaceLedger.leancomplete
structure PropertyKindCalculus.InterfaceLedger.{u} (O : Type u) : Type u
structure PropertyKindCalculus.InterfaceLedger.{u} (O : Type u) : Type u
**An interface ledger**: a pairwise action between parts, carrying its cancellation law as a field — for mechanical actions, Newton's third law. A pair of readings that does not cancel is not two readings of one interface and should not be a term of this type; the obligation is a field for the reason `Recarving.preserves` is. A ledger is conveniently *entered* one direction at a time: `fun p q => raw p q - raw q p` antisymmetrizes any raw table, and its law is `omega`.
Fields
act : O → O → ℤ
What `p` exerts on `q` — signed, one fixed component of the action.
antisymm : ∀ (p q : O), self.act p q + self.act q p = 0
**The cancellation law**: the two readings of one interface sum to zero.
Realized as InterfaceLedger — act and antisymm — with netOn and netTotal reading
per-part nets against a carving and mutualTotal the flow across a cut. A ledger is entered
one direction at a time: fun p q => raw p q - raw q p antisymmetrizes any raw table, and
its law is omega. act_self is the law's own erasure clause: a carving that merges the two
ends of an interface hands both ends one name and the entry reads zero — which is why the
rover example's two drive trains (2/2 and 3/1 hub-to-rim splits) coarsen to the same
ledger, so internal-versus-external is the carving's fact rather than the machine's —
Dybkær's observer clause (§3.3 Note 5) with a proof attached.
The exact price of additivity. For any pairwise action over a carving, lawful or not, rolling up per-part nets over a union overshoots the two halves' own rollups by precisely the two cross-flows over the cut. A ledger that drops a reaction does not fail additivity vaguely — it fails it by this number. Stated with no law in scope, so it is the identity a violated law is measured against.
Lean code for Theorem15.5.2●1 theorem
Associated Lean declarations
-
PropertyKindCalculus.netTotal_union[complete]
-
PropertyKindCalculus.netTotal_union[complete]
-
theoremdefined in PropertyKindCalculus/InterfaceLedger.leancomplete
theorem PropertyKindCalculus.netTotal_union.{u} {O : Type u} (act : O → O → ℤ) (ext : O → ℤ) (a b : PropertyKindCalculus.Decomposition O) : PropertyKindCalculus.netTotal act ext (a.union b) = PropertyKindCalculus.netTotal act ext a + PropertyKindCalculus.netTotal act ext b + (PropertyKindCalculus.mutualTotal act a b + PropertyKindCalculus.mutualTotal act b a)
theorem PropertyKindCalculus.netTotal_union.{u} {O : Type u} (act : O → O → ℤ) (ext : O → ℤ) (a b : PropertyKindCalculus.Decomposition O) : PropertyKindCalculus.netTotal act ext (a.union b) = PropertyKindCalculus.netTotal act ext a + PropertyKindCalculus.netTotal act ext b + (PropertyKindCalculus.mutualTotal act a b + PropertyKindCalculus.mutualTotal act b a)
**The exact price of additivity** — for *any* pairwise action, lawful or not. Rolling up per-part nets over a union overshoots the two halves' own rollups by precisely the two cross-flows over the cut. Everything the antisymmetric layer proves is this identity with the price argued to zero; everything a lawless table gets wrong is this identity with the price left standing.
Six instances of the fold's linearity, assembled by omega. The rover example presents the
invoice: log the motor torques and forget the reactions, and the whole's rollup exceeds its
halves' by 16 — four motors' worth of uncancelled flow across the chassis–arms cut.
The rollup. Under the cancellation law the price at every cut is zero, so the sum over the parts of the per-part nets is the exogenous total alone. The reaction a motor induces on the body is real in the per-part net — it loads a bearing — and absent from the whole; both facts are this theorem, read at a part and at the carving. Builds on the ledger and the price identity.
Lean code for Theorem15.5.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/InterfaceLedger.leancomplete
theorem PropertyKindCalculus.InterfaceLedger.netTotal_eq_extTotal.{u} {O : Type u} (L : PropertyKindCalculus.InterfaceLedger O) (ext : O → ℤ) (d : PropertyKindCalculus.Decomposition O) : PropertyKindCalculus.netTotal L.act ext d = PropertyKindCalculus.partTotal ext d
theorem PropertyKindCalculus.InterfaceLedger.netTotal_eq_extTotal.{u} {O : Type u} (L : PropertyKindCalculus.InterfaceLedger O) (ext : O → ℤ) (d : PropertyKindCalculus.Decomposition O) : PropertyKindCalculus.netTotal L.act ext d = PropertyKindCalculus.partTotal ext d
**The rollup.** The sum over the parts of the per-part nets is the exogenous total alone: every interior interface is read once in each direction, and the law cancels the pair. The reaction a motor induces on the body is real in `netOn` — it loads a bearing — and absent from the whole; both facts are this theorem, read at a part and at the carving.
The flows across any cut cancel (mutualTotal_cancel, by induction from the field), so the
interior of one carving cancels outright and only the exogenous column survives. In the
rover: the chassis's net reads −16 (four motors' reactions), each hub's balances to zero, and
the rover's total is the ground torque alone.
Additivity, purchased. The net over a ledger satisfies the
extensive law — but where mass's additive field is the model's free choice, this one is a
theorem with a hypothesis: delete the cancellation field and
the price identity prices exactly what remains. One predicate,
two different licenses, which is the sense in which the scope of extensivity is
kind-specific: what varies between kinds is not whether a sum appears but which law licenses
it.
Lean code for Theorem15.5.4●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/InterfaceLedger.leancomplete
theorem PropertyKindCalculus.InterfaceLedger.netMeasurement_extensive.{u} {O : Type u} (L : PropertyKindCalculus.InterfaceLedger O) (k : PropertyKindCalculus.KindOfProperty) (ref : String) (ext : O → ℤ) : PropertyKindCalculus.Extensive k (L.netMeasurement k ref ext)
theorem PropertyKindCalculus.InterfaceLedger.netMeasurement_extensive.{u} {O : Type u} (L : PropertyKindCalculus.InterfaceLedger O) (k : PropertyKindCalculus.KindOfProperty) (ref : String) (ext : O → ℤ) : PropertyKindCalculus.Extensive k (L.netMeasurement k ref ext)
**Additivity, purchased.** The net over a ledger is extensive — but where mass's `additive` field is the model's free choice, this one is a theorem with a hypothesis: delete the `antisymm` field and `netTotal_union` prices exactly what remains. One predicate, `Extensive`, two different licenses — which is what makes the scope of extensivity kind-specific rather than a single yes-or-no.
Both fields follow from the rollup: the kind is fixed by construction, and additivity collapses to the fold's union case once each rollup is its exogenous total. The rover example instantiates it at the torque kind, with the lawless counter-witness beside it.