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
proof body
Term-mode proof.
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. -/
depends on (20)
Lean names referenced from this declaration's body.