pith. machine review for the scientific record. sign in
theorem proved term proof

massless_at_speed_c

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 303theorem massless_at_speed_c (E p₁ p₂ p₃ : ℝ)
 304    (h : E ^ 2 = p₁ ^ 2 + p₂ ^ 2 + p₃ ^ 2 + 0 ^ 2) :
 305    E ^ 2 = p₁ ^ 2 + p₂ ^ 2 + p₃ ^ 2 := by linarith

proof body

Term-mode proof.

 306
 307/-- **The minimum rest mass** is the Yang-Mills mass gap Δ = J(φ). -/

depends on (9)

Lean names referenced from this declaration's body.