156theorem full_inevitability_triangulated 157 (bridge : InteractionForcesHyperbolicODE) 158 (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ) 159 (hNorm : F 1 = 0) 160 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹) 161 (hSmooth : ContDiff ℝ 2 F) 162 (hCalib : deriv (deriv (fun t => F (Real.exp t))) 0 = 1) 163 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) 164 (hInt : HasInteraction F) : 165 -- Part 1: P is entangling (unconditional from interaction) 166 IsEntangling P ∧ 167 -- Part 2: G satisfies hyperbolic ODE (from bridge) 168 SatisfiesHyperbolicODE (fun t => F (Real.exp t)) := by
proof body
Term-mode proof.
169 constructor 170 -- Part 1: Interaction ⟹ Entanglement 171 · exact interaction_forces_entanglement F P hCons hNorm hSymm hInt 172 -- Part 2: Bridge hypothesis gives hyperbolic ODE 173 · exact bridge F P hNorm hSymm hSmooth hCalib hCons hInt 174 175/-- If F = J, then P = RCL (unconditional, no bridge needed). -/
depends on (19)
Lean names referenced from this declaration's body.