rcl_without_gate

formal source

 217with some function P, then P equals the RCL polynomial on [0, ∞)². This holds
 218without any assumption on P's form (polynomial, right-affine, smooth, etc.).
 219-/
 220theorem rcl_without_gate
 221    (P : ℝ → ℝ → ℝ)
 222    (hCons : ∀ x y : ℝ, 0 < x → 0 < y →
 223      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y)) :
 224    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2*u*v + 2*u + 2*v :=
 225  Unconditional.rcl_unconditional P hCons
 226
 227/-! ## Part 5: Summary
 228
 229The Gap 4 question was: can `rightAffine` be derived from factorization +
 230associativity + continuity, rather than assumed?
 231
 232**Answer: YES, in two different ways:**
 233
 2341. **Via polynomial form (this module):** If `P` is a symmetric quadratic
 235   polynomial and `F` satisfies the Inevitability hypotheses, then `P` is
 236   right-affine as an immediate algebraic consequence of
 237   `bilinear_family_forced`. See `polynomial_consistency_implies_right_affine`.
 238
 2392. **Via surjectivity (Unconditional.lean):** If F = J, then for any function
 240   P satisfying the consistency relation, P equals the RCL polynomial on
 241   [0,∞)². No assumption on P at all. See `rcl_without_gate` (aliased from
 242   `Unconditional.rcl_unconditional`).
 243
 244Either route avoids needing `rightAffine` as an independent hypothesis. The
 245core RCL forcing claim therefore does not rest on an unproved right-affine
 246assumption: the gate can be dismantled by assuming more structure on P (path
 2471) OR assuming F = J and using surjectivity (path 2).
 248
 249**The remaining genuinely-open step** (not addressed by this module): proving
 250that P must be polynomial in the first place, starting only from F being C²