ledgerLinearResponse_iff_rcl
plain-language theorem explainer
A real bivariate combiner satisfies the ledger-linear response axioms if and only if it equals the canonical RCL polynomial $2uv+2u+2v$ pointwise. Phase-3 workers deriving the T4-to-T5 bridge from the free recognition ledger cite this equivalence. One direction reuses the existing gate-forcing theorem; the converse checks the five structure fields by direct substitution and free-ledger additivity.
Claim. For $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, the following are equivalent: (i) $P$ is symmetric, obeys the zero boundary $P(u,0)=2u$, the unit diagonal $P(1,1)=6$, the right-affine response $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$, and free-ledger cost additivity; (ii) $P(u,v)=2uv+2u+2v$ for all real $u,v$.
background
Phase 3 of the foundation chain asks that the T4-to-T5 bridge be derived from the recognition ledger rather than taken as an analytic input. The free ledger already supplies unconditional cost additivity: the cost of a sum of defect ledgers equals the sum of the costs, with no independence restriction.
Ledger-linear response packages the algebraic target for a two-variable combiner $P$: symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and the right-response identity that the second argument is affine with slope fixed by the unit-mass response. Its free-ledger-additivity field is pinned to the existing free-ledger theorem rather than left as prose.
The canonical RCL combiner is the polynomial $2uv+2u+2v$. Upstream, ledger-linear response already forces this polynomial through the d'Alembert factorization gate. The present result closes the biconditional.
proof idea
Bidirectional constructor. The forward arrow is the one-line application of ledgerLinearResponse_forces_rcl, which routes through the factorization gate. The reverse arrow assumes $P$ equals the RCL combiner pointwise and builds a LedgerLinearResponse structure: symmetry, zero boundary, unit diagonal, and right response each reduce by rewriting both sides with the hypothesis, unfolding the combiner, and closing by ring (or norm_num on the unit diagonal). Free-ledger additivity is discharged by the unconditional theorem ledgerCost_add.
why it matters
This is the clean algebraic hinge of the ledger-to-factorization bridge: ledger-linear response is exactly the RCL polynomial, so the remaining Phase-3 obligation is only to derive ledger-linear response from free-ledger posting semantics. Downstream, both freeLedgerCombinerSemantics_iff_rcl and rationalLedgerPosting_iff_rcl route through this equivalence (or its one-sided force lemma) to identify free-ledger and rational completed posting with the canonical combiner.
In the forcing chain this feeds T5 (J-uniqueness) via the Recognition Composition Law, whose bilinear right-hand side is precisely the RCL combiner. Closing the free-ledger-to-linear-response step would finish the ledger-native derivation of that law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.