discreteLedgerPosting_from_primitiveLedgerPosting
plain-language theorem explainer
If a two-variable combiner obeys primitive ledger-posting semantics (additivity under free defect-ledger costs), then it automatically obeys discrete posting on natural-number rank-one costs. Anyone deriving affine response from the free ledger rather than assuming it cites this specialization. The proof copies the shared fields and realizes natural additivity by posting two single-generator Unit ledgers.
Claim. Let $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$. If $P$ is symmetric, satisfies the zero boundary $P(u,0)=2u$, the unit diagonal $P(1,1)=6$, free-ledger additivity, and is additive in the second argument when that argument is the recognition cost of an arbitrary free defect ledger, then $P$ is additive in the second argument on natural numbers: $P(u,m+n)-P(u,0)=(P(u,m)-P(u,0))+(P(u,n)-P(u,0))$ for all $u\in\mathbb{R}$ and $m,n\in\mathbb{N}$.
background
This module isolates the remaining algebraic condition for the T4-to-T5 bridge: derive the d'Alembert factorization gate from the recognition ledger instead of taking it as analytic input. The free ledger already has unconditional additivity; the missing piece is a ledger-linear response of a two-variable combiner in its second argument.
A defect ledger is a finitely supported multiplicity map $I\to_0\mathbb{N}$ (the free commutative monoid on generators). Its recognition cost under weights $w$ is the total weighted multiplicity. Primitive posting semantics feed that cost directly into $P$ and require additivity when ledgers are summed. Discrete posting is the weaker surface that only demands the same additivity after restricting to natural-number costs on the rank-one unit ledger.
Shared boundary data for both surfaces: symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, and unit diagonal $P(1,1)=6$. Together with right-affine response these feed the existing gate that forces the Recognition Composition Law polynomial.
proof idea
Build a DiscreteLedgerPostingSemantics record by refining. Copy symmetric, zeroBoundary, unitDiagonal, and free_ledger_additivity straight from the primitive hypothesis.
The only obligation is rightNatPostedAdditive. For fixed $u$ and naturals $m,n$, take the rank-one index type Unit with constant weight $1$, and form single-generator ledgers $\Gamma=\mathrm{single}(),m$ and $\Delta=\mathrm{single}(),n$. Apply the primitive field rightLedgerPostedAdditive to these ledgers. The floor lemmas unit_cost_is_generator_count and ledgerCost_add identify the three ledger costs with $m$, $n$, and $m+n$ as reals, so the primitive identity specializes exactly to natural-number posted additivity.
why it matters
This is the specialization step that lets primitive (Phase-2-faithful) ledger posting imply the discrete rank-one surface used by the affine-response theorems. Downstream, primitiveLedgerPosting_forces_natAffineResponse is literally one line: apply discreteLedgerPosting_forces_natAffineResponse after this theorem.
In the module narrative, once right-affine response is obtained on natural costs, symmetry, boundary, and unit diagonal let the existing d'Alembert factorization gate force the RCL polynomial $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. That is the T4-to-T5 bridge derived from the ledger rather than assumed, feeding J-uniqueness (T5) and the rest of the forcing chain.
The declaration closes no open sorry; it is a proved link in the ledger-to-factorization spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.