complete_forcing_chain

formal source

 191/-! ## Corollary: The Full Chain -/
 192
 193/-- The complete forcing chain with NO polynomial assumption on P. -/
 194theorem complete_forcing_chain :
 195    -- 1. F = J is forced (by symmetry + calibration + ODE uniqueness)
 196    -- This is established in CostUniqueness and FunctionalEquation
 197    (∀ x : ℝ, 0 < x → Cost.Jcost x = (x + x⁻¹) / 2 - 1) ∧
 198    -- 2. J satisfies the cosh-add identity
 199    (∀ t u : ℝ, G Cost.Jcost (t + u) + G Cost.Jcost (t - u) =
 200      2 * (G Cost.Jcost t * G Cost.Jcost u) + 2 * (G Cost.Jcost t + G Cost.Jcost u)) ∧
 201    -- 3. The multiplicative form is the RCL
 202    (∀ x y : ℝ, 0 < x → 0 < y →
 203      Cost.Jcost (x * y) + Cost.Jcost (x / y) =
 204      2 * Cost.Jcost x * Cost.Jcost y + 2 * Cost.Jcost x + 2 * Cost.Jcost y) := by
 205  refine ⟨?_, ?_, ?_⟩
 206  · intro x hx
 207    simp only [Cost.Jcost]
 208  · exact Jcost_cosh_add_identity
 209  · exact J_computes_P
 210
 211/-! ## Meta-Theorem: P Cannot Be Anything Else -/
 212
 213/-- If any P satisfies the consistency equation with J, it must be the RCL.
 214    This rules out ALL alternatives, polynomial or not. -/
 215theorem P_uniqueness (P Q : ℝ → ℝ → ℝ)
 216    (hP : ∀ x y : ℝ, 0 < x → 0 < y →
 217      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y))
 218    (hQ : ∀ x y : ℝ, 0 < x → 0 < y →
 219      Cost.Jcost (x * y) + Cost.Jcost (x / y) = Q (Cost.Jcost x) (Cost.Jcost y)) :
 220    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = Q u v := by
 221  intro u v hu hv
 222  have hP' := rcl_unconditional P hP u v hu hv
 223  have hQ' := rcl_unconditional Q hQ u v hu hv
 224  rw [hP', hQ']