rightAffine_of_ledgerLinearResponse
plain-language theorem explainer
Ledger-linear response of a two-argument combiner forces affinity in the second slot: for each fixed first argument there are real coefficients making the map affine in the second. Anyone building the d'Alembert factorization gate from ledger data cites this extraction step. The proof is a one-line unpacking of the structure's right-response identity into existential form.
Claim. If a combiner $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ satisfies ledger-linear response (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and right-response $P(u,v)=(P(u,1)-P(u,0))\,v+P(u,0)$), then for every $u$ there exist $\alpha,\beta\in\mathbb{R}$ such that $P(u,v)=\alpha v+\beta$ for all $v$.
background
This module is the ledger-to-factorization bridge. Phase 3 asks that the T4-to-T5 step be derived from the recognition ledger rather than assumed as an analytic input. The free ledger already proves unconditional additivity; what remains is an algebraic condition on a two-variable combiner.
Ledger-linear response packages that condition: symmetry of $P$, the zero-boundary law $P(u,0)=2u$, the unit diagonal $P(1,1)=6$, and a right-response identity stating that the second argument is governed by response to one unit of posted ledger mass, namely $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$. A free-ledger-additivity field pins the bridge to the existing free-ledger theorem rather than leaving it as prose.
The d'Alembert factorization gate needs a right-affine field: for each fixed first argument, the map in the second is affine. This declaration extracts that field from the response identity.
proof idea
Term-mode one-liner. Fix the first argument $u$. Take affine coefficients $\alpha:=P(u,1)-P(u,0)$ and $\beta:=P(u,0)$. The structure field already asserts $\forall v,,P(u,v)=\alpha v+\beta$, so the existential goal is immediate. No further lemmas are applied.
why it matters
Direct input to factorizationGate_of_ledgerLinearResponse, which packages ledger-linear response into the full factorization associativity gate (symmetry, right-affinity, zero boundary, and the remaining gate fields). That gate is the algebraic premise that forces the Recognition Composition Law polynomial and thereby the T5 J-uniqueness step of the forcing chain ($J(x)=(x+x^{-1})/2-1$).
The module isolates this as the precise remaining condition: once the combiner has ledger-linear response, right-affinity is free; together with symmetry, the boundary law, and the unit diagonal, the existing gate theorem forces the RCL. The declaration therefore closes the T4-to-T5 bridge from ledger data rather than treating affinity as an external analytic assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.