rclCombiner_satisfies_gate
plain-language theorem explainer
The canonical RCL combiner P(u,v)=2uv+2u+2v meets the full factorization/associativity gate: symmetry, right-affine response, boundary law P(u,0)=2u, and normalization P(1,1)=6. Anyone citing the algebraic B2 closure or ledger-to-factorization bridge needs this witness. The proof is pure ring arithmetic on each gate field after unfolding the combiner.
Claim. The map $P(u,v)=2uv+2u+2v$ satisfies the factorization associativity gate: $P(u,v)=P(v,u)$ for all real $u,v$; for each fixed $u$ there exist $\alpha,\beta$ with $P(u,v)=\alpha v+\beta$ for all $v$; $P(u,0)=2u$ for all $u$; and $P(1,1)=6$.
background
The module isolates the algebraic core of the B2 closure program. After the hard analytic step (factorization plus three-way compatibility implying affine response in the second argument), the remaining forcing is pure algebra: symmetry, the boundary law $P(u,0)=2u$, and the normalization $P(1,1)=6$ together pin the combiner to the Recognition Composition Law polynomial.
The packaged gate FactorizationAssociativityGate is a Prop-structure on a binary real map $P$ with four fields: symmetry, existence of a right-affine representation, the zero-boundary law, and the unit-diagonal value 6. The canonical combiner is the bilinear polynomial $P(u,v)=2uv+2u+2v$, which is exactly the right-hand side of the RCL identity written in cost variables (cf. $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ after the usual shift).
This declaration simply certifies that the canonical polynomial inhabits that gate structure, so later ledger and forcing lemmas can quote the four fields by projection rather than re-proving elementary identities.
proof idea
Four independent field proofs, each by unfolding the combiner definition.
- Symmetry:
intro u v, unfold,ring. - Right-affine: for fixed $u$, exhibit witnesses $\alpha=2u+2$ and $\beta=2u$; the identity $P(u,v)=(2u+2)v+2u$ is again
ring. - Zero-boundary: unfold and
ringgives $P(u,0)=2u$. - Unit-diagonal: unfold and
norm_numgives $P(1,1)=6$.
No external lemmas are required; the gate is discharged by elementary polynomial arithmetic.
why it matters
This is the algebraic witness that the RCL combiner sits inside the factorization/associativity gate used by the B2 closure. Downstream, five ledger-semantics theorems in LedgerToFactorization project its fields: discrete free-ledger posting, primitive free-ledger posting, rational completed posting, free-ledger combiner semantics, and ledger-linear response all quote symmetric, zeroBoundary, and unitDiagonal from this result, then supply their own additive/continuity obligations.
In the broader Recognition chain this anchors the pure-algebra half of the forcing that identifies the combiner with the RCL polynomial (the same identity that appears after T5 J-uniqueness). Sibling results gate_forces_bilinear_family, gate_forces_rcl, and factorization_gate_iff_rcl then promote the gate into uniqueness of the RCL form. Without this inhabitant, the ledger-to-factorization bridge has no concrete combiner to carry posting semantics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.