FactorizationAssociativityGate
plain-language theorem explainer
FactorizationAssociativityGate packages four algebraic constraints on a combiner P that together force the bilinear family once right-affine response is known. Researchers closing the B2 factorization bridge or ledger regrouping arguments cite it to convert the analytic step into pure algebra. The declaration is a bare structure definition with no proof obligations or computational content.
Claim. Let $P : ℝ → ℝ → ℝ$. The factorization associativity gate holds when $P$ is symmetric ($P(u,v)=P(v,u)$ for all $u,v$), right-affine in its second argument (for each $u$ there exist scalars $α,β$ such that $P(u,v)=α v + β$ for all $v$), satisfies the zero-boundary law $P(u,0)=2u$ for all $u$, and meets the normalization $P(1,1)=6$.
background
The FactorizationForcing module isolates the algebraic core of the B2 closure program. Its module document states that the hard analytic step yields right-affine response for the combiner; the remaining work is pure algebra using symmetry, the boundary law $P(u,0)=2u$, and the unit-diagonal normalization $P(1,1)=6$ to recover the exact RCL polynomial. The combiner $P$ appears on the right-hand side of the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Upstream results include the cellular-automata step operator and various hypothesis-discharge predicates from ledger and game-theoretic modules that supply the right-affine property as an input to this gate.
proof idea
This declaration is a structure definition that directly encodes the four listed properties; it contains no proof body and serves as a hypothesis interface for downstream theorems.
why it matters
The gate is the central algebraic object in the factorization/associativity bridge. It is invoked by gate_forces_bilinear_family to extract the general bilinear form $cuv+2u+2v$ and by gate_forces_rcl to pin the coefficient $c=2$ via the normalization $P(1,1)=6$, thereby recovering the Recognition Composition Law. Downstream ledger factorization theorems (ledger_forces_regrouping, regrouping_forces_gate) and right-affine derivations invoke it to close the regrouping-invariance package. It completes the algebraic half of the T5 J-uniqueness forcing once the affine step is supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.