theorem
proved
term proof
interaction_forces_entanglement
show as:
view Lean formalization →
formal statement (Lean)
101theorem interaction_forces_entanglement (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
102 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
103 (hNorm : F 1 = 0)
104 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
105 (hInt : HasInteraction F) :
106 IsEntangling P :=
proof body
Term-mode proof.
107 interaction_implies_entangling F P hCons hNorm hSymm hInt
108
109/-! ## Gate 3: Curvature Characterizes the ODE -/
110
111/-- J's log-lift satisfies the hyperbolic ODE. -/