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

quark_mass_positive

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)

  89theorem quark_mass_positive (s : Sector) (r : ℤ) :
  90    0 < rs_mass_MeV s r := by

proof body

Term-mode proof.

  91  unfold rs_mass_MeV
  92  apply div_pos
  93  · apply mul_pos
  94    apply mul_pos
  95    apply mul_pos
  96    · exact zpow_pos (by norm_num : (0 : ℝ) < 2) _
  97    · exact zpow_pos Constants.phi_pos _
  98    · exact zpow_pos Constants.phi_pos _
  99    · exact zpow_pos Constants.phi_pos _
 100  · norm_num
 101
 102/-! ## Generation Structure: Torsion Determines Rung Spacing
 103
 104The key structural prediction: within each sector, generation spacing
 105is exactly {0, 11, 17} — the torsion schedule from cube geometry. -/
 106

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.