primitiveLedgerPosting_forces_rightPostedAdditive
plain-language theorem explainer
Primitive ledger-posting semantics already imply Cauchy additivity of the second-argument response for every real pair of postings: the excess cost of posting v+w equals the sum of the excesses for v and w. Anyone closing the T4-to-T5 ledger-to-factorization bridge cites this to drop a separate real-additivity axiom. The proof realizes v and w as costs of two rank-one defects on a two-generator Bool ledger and applies the structure's ledger-posted additivity field.
Claim. Let $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ satisfy primitive ledger-posting semantics (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and additivity of the second argument under posting of free weighted defect ledgers). Then for all real $u,v,w$, $$P(u,v+w)-P(u,0)=(P(u,v)-P(u,0))+(P(u,w)-P(u,0)).$$
background
Phase 3 of the foundation asks that the T4-to-T5 bridge be derived from the recognition ledger rather than assumed analytically. This module isolates the remaining algebraic condition: if a two-variable combiner has ledger-linear response in its second argument, then together with symmetry, the boundary law, and the unit diagonal, the d'Alembert factorization gate forces the Recognition Composition Law polynomial.
A defect ledger on an index type $I$ is a finitely supported multiplicity map $I\to_0\mathbb{N}$ (the free commutative monoid on $I$). Its recognition cost under a weight $w:I\to\mathbb{R}$ is the total weighted multiplicity. Primitive ledger-posting semantics feed the second coordinate of $P$ by such costs and require that posting ledgers additively is exactly the operation seen by the combiner; this sits closer to the Phase-2 free ledger than discrete natural-number posting surfaces.
The free ledger already proves unconditional additivity of costs. The present theorem lifts that ledger additivity to an unrestricted real Cauchy law for the combiner's second-argument excess $P(u,\cdot)-P(u,0)$.
proof idea
Fix $u,v,w$. Build a two-generator weight on $\mathrm{Bool}$ sending $\mathsf{false}\mapsto v$ and $\mathsf{true}\mapsto w$. Take the rank-one ledgers $\Gamma=\mathrm{single},\mathsf{false},1$ and $\Delta=\mathrm{single},\mathsf{true},1$. Three short simplifications give $\mathrm{ledgerCost}(w,\Gamma)=v$, $\mathrm{ledgerCost}(w,\Delta)=w$, and (via $\mathrm{ledgerCost_add}$) $\mathrm{ledgerCost}(w,\Gamma+\Delta)=v+w$. Instantiate the structure field $\mathrm{rightLedgerPostedAdditive}$ at these data; rewriting the three cost identities yields the real Cauchy identity.
why it matters
This is the algebraic hinge that turns primitive ledger posting into completed free-ledger and linear-response packages. Downstream, $\mathrm{freeLedgerCombinerSemantics_from_primitiveLedgerPosting}$ quotes it so that "the additive response law is no longer a separate assumption: realize arbitrary real postings $v$ and $w$ as the costs of two primitive defects in a two-generator ledger." The three linear-response closures (monotone, nonnegative, and the non-vacuous directional monotone-or-antitone form) likewise consume it to obtain $\mathrm{LedgerLinearResponse}$, whose $\mathrm{rightAffine}$ field feeds the d'Alembert factorization gate.
In the forcing chain this is infrastructure for T5 (J-uniqueness / RCL), not a direct citation of T6--T8. It removes an analytic input from the T4-to-T5 bridge and replaces it by ledger structure plus a regularity side condition chosen carefully so the target RCL combiner is not excluded (directional order, not global monotonicity).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.