gate_forces_rcl
plain-language theorem explainer
Any combiner P obeying the factorization associativity gate equals the RCL polynomial 2uv + 2u + 2v. Workers on the B2 bridge in Recognition Science cite this to select the canonical member of the bilinear family. The proof first extracts the general form c uv + 2u + 2v from the gate via an upstream lemma, then fixes c to 2 by evaluating at the unit diagonal and applying linear arithmetic.
Claim. Let $P : ℝ → ℝ → ℝ$ satisfy the factorization associativity gate (symmetry $P(u,v)=P(v,u)$, right-affine response, boundary $P(u,0)=2u$, and $P(1,1)=6$). Then $P(u,v)=2uv + 2u + 2v$ for all real $u,v$.
background
The FactorizationAssociativityGate packages symmetry, right-affine form in the second argument, zero boundary $P(u,0)=2u$, and unit diagonal $P(1,1)=6$. This module supplies the algebraic forcing after the analytic step that yields right-affine response. The upstream result gate_forces_bilinear_family establishes that any such P must be of the form $c uv + 2u + 2v$ for some constant $c$. From the module documentation, once affine response is available, symmetry and boundary law force the bilinear family, after which normalization selects the RCL member.
proof idea
The proof obtains the bilinear family expression from gate_forces_bilinear_family. It then evaluates the expression at u=v=1, uses the unit diagonal condition P(1,1)=6 together with the gate property to conclude c=2 by linear arithmetic. The general case follows by substitution.
why it matters
This result supplies the final normalization step that selects the RCL combiner inside the factorization forcing module. It is invoked by ledger_forces_rcl to derive the RCL form from ledger substitutivity and regrouping invariance, and by polynomial_consistency_forces_rcl to close the polynomial consistency gap. In the Recognition framework it completes the algebraic core of the B2 closure program leading to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.