freeLedgerCombinerSemantics_from_primitiveLedgerPosting
plain-language theorem explainer
Primitive ledger-posting semantics plus second-argument continuity upgrade a two-variable combiner to free-ledger combiner semantics. Cited by anyone closing the ledger-to-factorization bridge toward d'Alembert factorization. The proof is a structure package: shared boundary axioms copy over, and the real additive response field is supplied by the primitive-posting forcing lemma.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$. Suppose $P$ obeys primitive ledger-posting semantics: symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and additive response whenever the second argument is the cost of a free defect ledger. If moreover $v\mapsto P(u,v)$ is continuous for every fixed $u$, then $P$ satisfies free-ledger combiner semantics: the same boundary laws, additive response $P(u,v+w)-P(u,0)=(P(u,v)-P(u,0))+(P(u,w)-P(u,0))$ for arbitrary reals $v,w$, second-argument continuity, and free-ledger additivity.
background
This module is the Phase-3 ledger-to-factorization bridge. The free ledger already gives unconditional additivity; the remaining algebraic condition is a ledger-linear response of a two-variable combiner in its second argument, which yields the rightAffine input to the d'Alembert factorization gate and, with symmetry, boundary law, and unit diagonal, forces the RCL polynomial.
Primitive ledger-posting semantics feed the second coordinate by the cost of actual free defect ledgers (closer to the Phase-2 ledger than discrete natural-number posting). Free-ledger combiner semantics deliberately weaken full ledger-linear response: they record second-argument additive posting plus a continuity gate, leaving Cauchy linearization as a theorem rather than an axiom.
The key upstream lemma states that primitive ledger posting over arbitrary weighted defect ledgers already forces the additive response law for arbitrary real postings. Continuity is the only extra regularity needed to complete the free-ledger package.
proof idea
Term-mode structure construction via refine. Four fields copy directly from the primitive-posting hypothesis: symmetry, zero boundary, unit diagonal, and free-ledger additivity. Second-argument continuity is the extra hypothesis, inserted as the regularity field. The sole nontrivial obligation is right-posted additivity for arbitrary real second arguments; it is discharged in one step by the upstream theorem that primitive ledger posting forces the real additive response law.
why it matters
This is the intermediate upgrade from primitive ledger posting to free-ledger combiner semantics. The sole downstream consumer packages it further into completed real ledger-linear response: primitive posting plus continuity forces full linear response by routing through this theorem and then the free-ledger-to-linear-response step.
In the forcing chain this sits on the T4-to-T5 bridge: once ledger-linear response is in hand, the factorization gate (with symmetry, boundary, unit diagonal) forces the Recognition Composition Law polynomial, whose unique solution is the J-cost $J(x)=(x+x^{-1})/2-1$ (T5). The module isolates exactly the algebraic condition still needed so that the recognition ledger, rather than an analytic assumption, supplies the bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.