ledgerLinearResponse_from_primitiveLedgerPosting
plain-language theorem explainer
Primitive ledger-posting semantics plus continuity in the second argument upgrades a real combiner to full ledger-linear response. Anyone closing the T4-to-T5 ledger-to-factorization bridge cites this. The proof is a one-line composition: lift to free-ledger combiner semantics, then apply the free-ledger linear-response lemma.
Claim. Let $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ satisfy 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 of $P(u,\cdot)$ to free defect-ledger posting. If $v\mapsto P(u,v)$ is continuous for every fixed $u$, then $P$ has ledger-linear response: $P(u,v)=(P(u,1)-P(u,0))\,v+P(u,0)$, together with free-ledger cost additivity.
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, the rightAffine field of the d'Alembert factorization gate follows, and with symmetry, boundary law, and unit diagonal the gate forces the RCL polynomial.
Primitive ledger-posting semantics is the Phase-2-near surface: the second coordinate is fed by costs of actual free defect ledgers, and additive posting of those ledgers is exactly the operation the combiner sees. It is stricter than the discrete (natural-number) posting surface. Ledger-linear response strengthens this to an explicit affine law $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$, pinning the bridge to the free-ledger additivity theorem rather than leaving it as prose.
Continuity in the second slot is the analytic glue that completes the real response from the ledger-posted additive law on the free-ledger image.
proof idea
One-line term wrapper. First apply freeLedgerCombinerSemantics_from_primitiveLedgerPosting to the given primitive posting hypothesis and the continuity assumption; that produces free-ledger combiner semantics for $P$. Then feed the result into ledgerLinearResponse_from_free_ledger, which already knows how to extract the completed real ledger-linear response (affine right response plus free-ledger cost additivity) from free-ledger combiner semantics.
why it matters
This is the middle rung of the ledger-to-factorization ladder. Downstream, factorizationGate_of_primitiveLedgerPosting wraps it once more to obtain the full factorization associativity gate, and primitiveLedgerPosting_forces_rcl composes further with ledgerLinearResponse_forces_rcl to conclude that $P$ equals the canonical RCL combiner pointwise.
In framework terms this is the concrete T4-to-T5 step: free-ledger posting plus continuity forces the Recognition Composition Law polynomial, which is the algebraic content behind T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). The module doc states the program explicitly: free ledger already gives unconditional additivity; ledger-linear response supplies rightAffine; the existing gate then forces RCL. Closing this theorem therefore retires an analytic input in favor of a ledger-derived hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.