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

tau_mass_pred_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)

  83theorem tau_mass_pred_bounds :
  84  (1768 : ℝ) < predicted_mass_tau ∧ predicted_mass_tau < (1792 : ℝ) :=

proof body

Term-mode proof.

  85  Necessity.tau_mass_pred_bounds_proven
  86
  87/-- T10 Theorem: Tau mass follows the Face Symmetry Step.
  88
  89    Proof: From tau_mass_pred_bounds and mass_tau_MeV = 1776.86,
  90    |pred - exp| / exp < 1% ✓
  91
  92    NOTE: Accuracy reduced from 5e-4 to 1% due to corrected interval bounds. -/

used by (3)

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

depends on (11)

Lean names referenced from this declaration's body.