def
definition
def or abbrev
DefectCollapse
show as:
view Lean formalization →
formal statement (Lean)
53def DefectCollapse (x : ℝ) : Prop := 0 < x ∧ defect x = 0
proof body
Definition body.
54
55/-! ## Core Equivalence Theorems -/
56
57/-- **Defect Zero Characterization**: defect(x) = 0 ⟺ x = 1 (for x > 0). -/