gate_forces_bilinear_family
plain-language theorem explainer
Any combiner P obeying the FactorizationAssociativityGate axioms must take the bilinear form c u v + 2 u + 2 v for some real constant c. Algebraic closure arguments in the Recognition Science framework cite this result to reduce the combiner to a one-parameter family before normalization. The proof extracts the right-affine coefficients, fixes the linear term via the zero-boundary condition, and solves for the coefficient c using symmetry at the unit point.
Claim. Let $P : ℝ → ℝ → ℝ$ satisfy the FactorizationAssociativityGate conditions: symmetry $P(u,v) = P(v,u)$, right-affineness $∀ u ∃ α,β ∀ v, P(u,v) = α v + β$, zero boundary $P(u,0) = 2u$, and unit diagonal $P(1,1) = 6$. Then there exists $c ∈ ℝ$ such that $P(u,v) = c u v + 2u + 2v$ for all real $u,v$.
background
The FactorizationAssociativityGate structure encodes the minimal algebraic properties required for the combiner in the factorization bridge: it is symmetric, affine in the second argument for each fixed first argument, vanishes to 2u on the zero boundary, and evaluates to 6 at the unit diagonal. This module isolates the pure algebraic forcing that follows once the hard analytic step of establishing right-affineness has been completed elsewhere. Upstream results supply the J-cost structure and the ledger factorization that motivate the specific boundary and diagonal normalizations.
proof idea
The proof begins by invoking classical choice to extract the affine coefficients α and β from the rightAffine field of the gate. It then uses the zeroBoundary condition to show that β u equals 2u for every u. Defining c as α 1 minus 2, symmetry is applied to equate the affine expressions at (u,1) and (1,u), which determines α u as c u plus 2. Substituting these expressions back into the affine form and simplifying with ring arithmetic yields the desired bilinear expression.
why it matters
This result supplies the bilinear family that the subsequent gate_forces_rcl theorem normalizes to the exact Recognition Composition Law form by fixing c to 2 via the unit diagonal. It completes the algebraic half of the factorization/associativity bridge described in the module documentation, bridging the affine-response step to the RCL polynomial. In the broader framework it supports the derivation of the eight-tick octave and the phi-ladder mass formula by ensuring the combiner satisfies the functional equation J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.