bilinear_implies_right_affine
plain-language theorem explainer
If a combiner P satisfies P(u,v) = 2u + 2v + c u v for some fixed real c, then for each u there exist real alpha and beta making P(u,v) equal to alpha v plus beta for all v. Researchers deriving the RCL polynomial from factorization in Recognition Science cite this algebraic closure of Gap 4. The proof constructs the coefficients explicitly for each u and confirms the identity by ring simplification.
Claim. If $P : ℝ → ℝ → ℝ$ and $c : ℝ$ satisfy $∀ u v, P(u,v) = 2u + 2v + c · u v$, then $∀ u, ∃ α β, ∀ v, P(u,v) = α v + β$.
background
The Right-Affine from Factorization module closes Gap 4 by deriving the right-affine property of the combiner P directly from its bilinear form, rather than encoding it as a hypothesis inside the FactorizationAssociativityGate. Right-affine means that for each fixed first argument u there exist coefficients α and β such that P(u,v) equals αv + β for every v. The bilinear hypothesis here is precisely the RCL polynomial form 2u + 2v + c uv that arises from the Recognition Composition Law after the J-uniqueness step.
proof idea
The term proof introduces the fixed u, supplies the witness pair α = 2 + c u and β = 2 u, then rewrites the target equality via the bilinear hypothesis and closes with the ring tactic.
why it matters
This supplies the direct algebraic step used by polynomial_consistency_implies_right_affine, which combines it with the Inevitability hypotheses to obtain right-affine from polynomial consistency alone. It thereby supports the gate-free route to the RCL polynomial via Unconditional.rcl_unconditional and the surjectivity of J, advancing the forcing chain from T5 J-uniqueness toward the eight-tick octave without leaving right-affine as an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.