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

tau_muon_ratio_bounds

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)

 143theorem tau_muon_ratio_bounds :
 144    (17 : ℝ) < phi ^ 6 ∧ phi ^ 6 < (18 : ℝ) := phi_pow_6_bounds

proof body

Term-mode proof.

 145
 146/-- The charm/up mass ratio: m_c/m_u = φ^(15-4) = φ¹¹ ≈ 199. -/

depends on (1)

Lean names referenced from this declaration's body.