rcl_right_affine
plain-language theorem explainer
The RCL polynomial 2uv + 2u + 2v satisfies right-affine form: for each fixed u there exist coefficients α and β such that the expression equals αv + β for all v. Researchers closing the factorization-associativity gap in Recognition Science cite this to drop the rightAffine hypothesis from the gate once the combiner is identified with the RCL case. The proof is a direct term-mode construction that exhibits α = 2 + 2u and β = 2u then verifies the identity by ring normalization.
Claim. For every real number $u$, there exist real numbers $α$ and $β$ such that for every real number $v$, $2uv + 2u + 2v = αv + β$.
background
In Recognition Science the Recognition Composition Law produces the quadratic combiner $P(u,v) = 2uv + 2u + 2v$ under multiplicative consistency of the cost functional. The right-affine property requires that $P(u,v)$ be linear in the second argument for each fixed first argument; this property is packaged as a hypothesis inside the FactorizationAssociativityGate structure that bridges factorization and associativity. The present module closes Gap 4 by proving the property directly for the RCL polynomial itself.
proof idea
The proof is a term-mode construction. For arbitrary $u$ it supplies the explicit pair of coefficients $2 + 2u$ and $2u$. The universal quantifier over $v$ is discharged by a single ring tactic that normalizes both sides of the equality to the same expression.
why it matters
This result removes the need to postulate right-affine behavior once the combiner is known to be the RCL polynomial, thereby tightening the FactorizationAssociativityGate. It supports the compositional route that derives right-affine from polynomial consistency via the upstream bilinear_family_forced theorem. In the forcing chain it contributes to T5 J-uniqueness and the eight-tick octave without extra hypotheses on the combiner.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.