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 :=
proof body
Term-mode proof.
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² 251or smooth. This involves classical Aczél theory on functional equations and 252is non-trivial to formalize. However, the gate-free path (2) does not require 253this step at all, since it bypasses the question of P's form entirely. 254-/ 255 256end RightAffineFromFactorization 257end DAlembert 258end Foundation 259end IndisputableMonolith
depends on (33)
Lean names referenced from this declaration's body.