gate_from_polynomial_consistency
plain-language theorem explainer
The theorem shows that if F is normalized at 1 and multiplicatively consistent with a symmetric quadratic polynomial combiner P that satisfies the zero-boundary condition, unit-diagonal calibration, continuity on positives, and non-triviality, then P satisfies the four properties of the FactorizationAssociativityGate. Researchers closing derivation gaps in the Recognition Composition Law would cite it to replace the right-affine hypothesis with a derived property. The proof is a term-mode structure constructor that invokes the sibling lemma for
Claim. Let $F:ℝ→ℝ$ and $P:ℝ→ℝ→ℝ$. Suppose $F(1)=0$, $F(xy)+F(x/y)=P(F(x),F(y))$ for all $x,y>0$, $P$ is a symmetric quadratic polynomial, $F$ is continuous on $(0,∞)$ and non-vanishing at some positive point, $P(1,1)=6$, and $P(u,0)=2u$ for all $u$. Then $P$ is symmetric, right-affine in its second argument, obeys the zero-boundary condition, and satisfies the unit-diagonal condition.
background
In Recognition Science the function $F$ encodes the J-cost with $J(x)=(x+x^{-1})/2-1$, and multiplicative consistency states that $F(xy)+F(x/y)$ equals the combiner $P$ applied to the values $F(x)$ and $F(y)$. IsNormalized requires $F(1)=0$ as calibration. HasMultiplicativeConsistency is the functional equation above. The FactorizationAssociativityGate is the structure containing symmetry of $P$, right-affineness (for each fixed $u$ there exist $α,β$ such that $P(u,v)=αv+β$ for all $v$), the zero-boundary $P(u,0)=2u$, and the unit-diagonal $P(1,1)=6$ (from FactorizationForcing).
proof idea
The proof is a term-mode constructor of the FactorizationAssociativityGate structure. It supplies the symmetric field directly from the symmetry hypothesis, the zeroBoundary field from the zero-boundary hypothesis, and the unitDiagonal field from the unit-diagonal hypothesis. The rightAffine field is obtained by applying the sibling lemma polynomial_consistency_implies_right_affine to the normalization, consistency, polynomial form, symmetry, non-triviality, and continuity hypotheses.
why it matters
This declaration feeds the main theorem polynomial_consistency_forces_rcl of the same module, which derives the Recognition Composition Law from polynomial consistency without a separate right-affine assumption. It closes Gap 4 by turning right-affine into a theorem under the polynomial hypothesis, matching the paper claim that right-affine follows from factorization plus associativity and continuity. The module also records the alternative unconditional route via surjectivity of J that bypasses the gate entirely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.