polynomial_consistency_forces_rcl
plain-language theorem explainer
If a normalized continuous F on positive reals obeys multiplicative consistency with a symmetric quadratic polynomial P meeting P(1,1)=6 and P(u,0)=2u, then P equals the RCL form 2uv + 2u + 2v. Researchers deriving the Recognition Composition Law from polynomial assumptions on the combiner would cite this. The proof is a one-line term wrapper that feeds the gate extracted by gate_from_polynomial_consistency into gate_forces_rcl.
Claim. Let $F: (0,∞) → ℝ$ satisfy $F(1)=0$ and be continuous, and let $P: ℝ × ℝ → ℝ$ be symmetric quadratic with $P(1,1)=6$, $P(u,0)=2u$, and non-trivial. If $F(xy) + F(x/y) = P(F(x),F(y))$ holds for all positive $x,y$, then $P(u,v) = 2uv + 2u + 2v$ for all real $u,v$.
background
The module closes Gap 4 by deriving right-affine from polynomial consistency rather than taking it as hypothesis. IsNormalized requires $F(1)=0$. HasMultiplicativeConsistency encodes the relation $F(xy) + F(x/y) = P(F(x),F(y))$. Upstream gate_forces_rcl assumes the full FactorizationAssociativityGate (symmetric, right-affine, zero-boundary, unit-diagonal) to force P to the RCL polynomial 2uv + 2u + 2v. The local setting is the d'Alembert factorization route to the Recognition Composition Law, where polynomial form on P replaces an explicit right-affine assumption.
proof idea
Term-mode one-line wrapper. It applies gate_forces_rcl to the FactorizationAssociativityGate constructed by gate_from_polynomial_consistency, which uses the quadratic hypothesis, symmetry, boundary values, normalization, continuity, and non-triviality to satisfy the gate conditions.
why it matters
This is the main theorem of the module and shows right-affine is a consequence of polynomial consistency under Inevitability hypotheses, rather than an extra assumption. It advances the forcing chain toward the RCL identity central to T5 J-uniqueness. The result supports the claim that polynomial assumptions suffice to recover the RCL polynomial without separate right-affine input. It leaves open the fully unconditional route documented in Unconditional.lean, which uses only J-surjectivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.