ledgerLinearResponse_forces_rcl
plain-language theorem explainer
Ledger-linear response on a two-variable combiner forces pointwise equality with the canonical RCL polynomial $2uv+2u+2v$. Anyone deriving the Recognition Composition Law from free-ledger posting semantics cites this bridge. The proof is a short rewrite: build the factorization gate from the response hypotheses, then apply the existing gate-forces-RCL theorem.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ satisfy ledger-linear response: symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and right-affine unit response $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$ (pinned to free-ledger additivity). Then for all real $u,v$, $P(u,v)=2uv+2u+2v$.
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: free-ledger additivity is already unconditional; if a combiner has the matching linear response in its second argument, the d'Alembert factorization gate follows.
Ledger-linear response packages symmetry, the zero boundary $P(u,0)=2u$, the unit diagonal $P(1,1)=6$, and right-response affineness $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$, with free-ledger additivity pinning the bridge to the existing ledger-cost theorem. The canonical RCL combiner is the bilinear polynomial $\mathrm{rclCombiner}(u,v)=2uv+2u+2v$.
Upstream, factorizationGate_of_ledgerLinearResponse turns those fields into a full factorization associativity gate (symmetry, right-affineness, zero boundary, unit diagonal). The gate theorem then states that canonical normalization selects the RCL member of the bilinear family.
proof idea
Short tactic proof. Introduce $u,v$. Rewrite the goal by gate_forces_rcl applied to $P$ and the gate instance built by factorizationGate_of_ledgerLinearResponse P h. That gate theorem already concludes $P(u,v)=2uv+2u+2v$, which is definitionally rclCombiner u v, so rfl closes. No new algebra is done here: the work is the composition of the two upstream lemmas.
why it matters
This is the clean one-direction arrow from ledger-linear response to the RCL polynomial, the algebraic content of the Recognition Composition Law used at T5 (J-uniqueness). Downstream it is the engine for the iff form ledgerLinearResponse_iff_rcl ("leaves one clean Phase 3 obligation: prove ledger-linear response from the free ledger interpretation") and for freeLedgerCombinerSemantics_iff_rcl.
It also closes every primitive-posting forcing route: continuity, monotone response, non-negativity of posted defect mass, and per-slice directional regularity all reduce to this theorem after manufacturing a LedgerLinearResponse instance. Those routes feed the T4-to-T5 ledger bridge without assuming the RCL polynomial as an analytic input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.