factorizationGate_of_ledgerLinearResponse
plain-language theorem explainer
Ledger-linear response on a real two-argument combiner yields the full factorization/associativity gate used by the d'Alembert bridge. Anyone closing the T4-to-T5 step from the recognition ledger, rather than assuming an analytic gate, cites this packaging theorem. The proof is a four-field structure assembly: three fields copy from the hypothesis, and right-affinity is read off by the companion coefficient lemma.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ satisfy ledger-linear response: $P(u,v)=P(v,u)$, $P(u,0)=2u$, $P(1,1)=6$, and $P(u,v)=(P(u,1)-P(u,0))\,v+P(u,0)$ for all $u,v$. Then $P$ satisfies the factorization associativity gate: symmetry, the zero-boundary and unit-diagonal laws above, and right-affinity ($\forall u\,\exists\alpha,\beta\,\forall v,\,P(u,v)=\alpha v+\beta$).
background
This module isolates the remaining algebraic condition for Phase 3: derive the T4-to-T5 bridge from the recognition ledger instead of taking it as an analytic input. The free ledger already gives unconditional additivity of posted defect mass. Ledger-linear response is the corresponding property for a two-variable combiner $P$: the second argument is governed by the response to one unit of posted ledger mass, pinned by a free-ledger additivity field rather than left as prose.
The target gate (from the d'Alembert factorization-forcing development) packages four properties on $P$: symmetry, existence of right-affine coefficients in the second slot, the zero-boundary law $P(u,0)=2u$, and the unit diagonal $P(1,1)=6$. Upstream, the companion lemma shows that the explicit right-response identity in ledger-linear response immediately supplies those affine coefficients $\alpha=P(u,1)-P(u,0)$ and $\beta=P(u,0)$.
Together with symmetry, boundary, and unit diagonal, the existing gate theorem is what forces the Recognition Composition Law (RCL) polynomial.
proof idea
Term-mode structure construction for the gate. Three fields are copied verbatim from the ledger-linear hypothesis: symmetry, zero boundary, and unit diagonal. The remaining field, right-affinity, is the companion theorem: for each fixed $u$ it exhibits $\alpha=P(u,1)-P(u,0)$ and $\beta=P(u,0)$, then applies the hypothesis right-response identity to conclude $P(u,v)=\alpha v+\beta$ for all $v$. No further algebraic work occurs here.
why it matters
This is the single packaging step that turns ledger-linear response into the gate the factorization bridge already knows how to discharge. Downstream, ledgerLinearResponse_forces_rcl applies the existing gate theorem to conclude $P$ equals the RCL combiner pointwise, which is the T4-to-T5 content the module advertises: the Recognition Composition Law polynomial forced from ledger structure rather than assumed.
Five sibling routes feed through this theorem: primitive ledger posting under continuity, monotonicity, directional regularity, or ledger-native non-negativity, and rational completed posting. Each first builds ledger-linear response, then calls this packaging step. In the forcing chain this sits at the entrance to T5 (J-uniqueness via the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$), so the ledger-native origin of the gate is what makes the later uniqueness of $J(x)=\cosh(\log x)-1$ ledger-derived rather than analytic input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.