factorization_gate_iff_rcl
plain-language theorem explainer
A real bivariate combiner satisfies the factorization/associativity gate if and only if it equals the canonical RCL polynomial $2uv+2u+2v$. Anyone forcing the Recognition Composition Law from the algebraic gate axioms cites this equivalence. The proof is a two-direction constructor: one side applies the prior forcing lemma, the other rebuilds the four gate fields by direct ring algebra.
Claim. For $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, the following are equivalent: (i) $P$ is symmetric, right-affine ($\forall u\,\exists\alpha,\beta\,\forall v:\,P(u,v)=\alpha v+\beta$), obeys the boundary $P(u,0)=2u$, and is normalized by $P(1,1)=6$; (ii) $P(u,v)=2uv+2u+2v$ for all real $u,v$.
background
This module isolates the pure-algebra half of the B2 closure program. After the hard analytic step has produced factorization plus three-way compatibility, the remaining work is to force a bivariate combiner $P$ down to a single polynomial. The packaged gate records exactly the four algebraic conditions used for that forcing: symmetry $P(u,v)=P(v,u)$, right-affinity in the second slot, the zero-boundary law $P(u,0)=2u$, and the unit-diagonal normalization $P(1,1)=6$.
The canonical target is the RCL combiner $2uv+2u+2v$. It is the bilinear expression that appears when the Recognition Composition Law is rewritten in additive coordinates (the same identity that underlies T5 J-uniqueness via $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$). Upstream, gate_forces_rcl already shows that any $P$ meeting the gate equals this polynomial; the present theorem closes the circle by proving the converse and packaging both directions as an iff.
proof idea
Term-mode constructor on the biconditional.
Forward: assume the gate; for arbitrary $u,v$ rewrite by gate_forces_rcl and finish with rfl against rclCombiner.
Reverse: assume $P$ equals rclCombiner pointwise; build a FactorizationAssociativityGate structure. Symmetry is $hP$ on both orders plus ring on the expanded polynomial. Right-affinity supplies the explicit coefficients $\alpha=2u+2$, $\beta=2u$ and checks the identity by ring. Zero-boundary and unit-diagonal are the same substitution at $v=0$ and at $(1,1)$, closed by ring and norm_num respectively.
why it matters
Gives the exact algebraic characterization of the RCL combiner inside the factorization/associativity bridge. The module doc states the program: once affinity is in hand, symmetry, $P(u,0)=2u$, and $P(1,1)=6$ force the RCL polynomial exactly; this theorem is that forcing statement written as an equivalence rather than a one-way implication.
It sits at the end of the local chain gate_forces_bilinear_family → gate_forces_rcl → iff, and therefore certifies that the gate is not merely sufficient but necessary for the canonical combiner. In the broader Recognition framework this is the algebraic core that feeds the Recognition Composition Law, which in turn is the functional equation behind T5 J-uniqueness. No downstream users are recorded yet; the declaration is the natural citation point for any later B2-closure or RCL-forcing theorem that needs the gate and the polynomial to be interchangeable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.