ledgerLinearResponse_from_free_ledger
plain-language theorem explainer
Continuous free-ledger combiners are fully ledger-linear in the second argument: additivity plus continuity upgrades to the affine response law P(u,v)=(P(u,1)-P(u,0))v+P(u,0). Anyone closing the T4–T5 ledger-to-factorization bridge cites this. The proof builds the continuous additive response map and applies real scalar homogeneity.
Claim. If a combiner $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ is symmetric, obeys the zero boundary $P(u,0)=2u$ and unit diagonal $P(1,1)=6$, is additive in posted second-argument increments, is continuous in the second argument, and satisfies free-ledger cost additivity, then it has ledger-linear response: $P(u,v)=(P(u,1)-P(u,0))\,v+P(u,0)$ for all $u,v$.
background
This module isolates the remaining algebraic gate on the T4-to-T5 path: derive the d'Alembert factorization input from recognition-ledger structure rather than assume it analytically. The free ledger already supplies unconditional cost additivity; what remains is to promote second-argument posting laws into the affine response used by the factorization gate.
FreeLedgerCombinerSemantics packages symmetry, boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, additive posting of increments in the second coordinate, continuity in that coordinate, and free-ledger additivity. Its response law is intentionally weaker than full linearity: Cauchy linearization is left as a theorem.
LedgerLinearResponse keeps the same symmetry, boundary, diagonal, and free-ledger fields, but replaces additive posting plus continuity by the closed form $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$. That affine law is exactly the rightAffine input the factorization gate needs, together with symmetry and the boundary data, to force the Recognition Composition Law polynomial.
proof idea
Refine the target structure by copying symmetry, zero boundary, unit diagonal, and free-ledger additivity from the hypothesis; only rightResponse remains.
For fixed $u$, define the additive monoid homomorphism $t\mapsto P(u,t)-P(u,0)$. Additivity is exactly rightPostedAdditive; the zero map is immediate. Continuity of this response follows from rightContinuous minus a constant.
Promote the continuous additive map to a continuous $\mathbb{R}$-linear map via AddMonoidHom.toRealLinearMap. Scalar homogeneity at $v\cdot 1$ yields $P(u,v)-P(u,0)=v,(P(u,1)-P(u,0))$. Commute the product and rearrange by linarith to the affine response identity.
why it matters
Phase 3 of the foundation chain asks that the T4-to-T5 bridge be ledger-derived. This theorem is the Cauchy-linearization step: free-ledger posting plus continuity becomes completed real ledger-linear response, so the d'Alembert gate can force the RCL polynomial without an external analytic assumption.
It is the forward half of freeLedgerCombinerSemantics_iff_ledgerLinearResponse (completed linear response is exactly free-ledger semantics plus continuity) and the workhorse inside ledgerLinearResponse_from_primitiveLedgerPosting, which lifts primitive posting plus continuity through free-ledger semantics into the same linear response.
In the forcing chain this feeds T5 J-uniqueness: once the combiner is ledger-linear, the existing gate yields $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law, rather than treating that functional equation as an input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.