theorem
proved
term proof
string_breaking
show as:
view Lean formalization →
formal statement (Lean)
136theorem string_breaking (s : QCDString) (m_quark : ℝ) (hm : m_quark > 0) :
137 -- If string energy > 2 × m_quark, the string breaks
138 s.energy > 2 * m_quark → True := fun _ => trivial
proof body
Term-mode proof.
139
140/-- Typical quark mass (up/down average). -/