115theorem rcl_right_affine : 116 ∀ u, ∃ α β, ∀ v, (2*u*v + 2*u + 2*v) = α * v + β := by
proof body
Term-mode proof.
117 intro u 118 refine ⟨2 + 2*u, 2*u, ?_⟩ 119 intro v 120 ring 121 122/-! ## Part 2: Right-affine from polynomial consistency 123 124Combining `Inevitability.bilinear_family_forced` with the bilinear-implies- 125right-affine lemma, we get: if `P` is a symmetric quadratic polynomial and `F` 126satisfies the standard hypotheses, then `P` is right-affine. 127 128This means the `rightAffine` hypothesis in `FactorizationAssociativityGate` is 129redundant under the stronger assumption that `P` is polynomial. 130-/ 131 132/-- Right-affine follows from polynomial consistency with a cost functional `F`. 133 134This theorem takes the Inevitability hypotheses (F normalized, consistent with 135a symmetric quadratic polynomial P, non-trivial, continuous) and concludes 136that P is right-affine. -/
depends on (17)
Lean names referenced from this declaration's body.