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

tau_mass_step_hypothesis

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)

  93theorem tau_mass_step_hypothesis :
  94    abs (predicted_mass_tau - mass_tau_MeV) / mass_tau_MeV < 1 / 100 := by

proof body

Tactic-mode proof.

  95  have h_pred := tau_mass_pred_bounds
  96  simp only [mass_tau_MeV]
  97  have h_diff_bound : abs (predicted_mass_tau - 1776.86) < (16 : ℝ) := by
  98    rw [abs_lt]
  99    constructor <;> linarith [h_pred.1, h_pred.2]
 100  have h_pos : (0 : ℝ) < 1776.86 := by norm_num
 101  have h_div : abs (predicted_mass_tau - 1776.86) / 1776.86 < 16 / 1776.86 := by
 102    apply div_lt_div_of_pos_right h_diff_bound h_pos
 103  calc abs (predicted_mass_tau - 1776.86) / 1776.86
 104      < 16 / 1776.86 := h_div
 105    _ < 1 / 100 := by norm_num
 106
 107end LeptonGenerations
 108end Physics
 109end IndisputableMonolith

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.