lemma proved term proof

`step_e_mu_bounds_v2`

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

formal statement (Lean)

 879lemma step_e_mu_bounds_v2 : (11.0795 : ℝ) < step_e_mu ∧ step_e_mu < (11.0796 : ℝ) := by

proof body

Term-mode proof.

 880  simp only [step_e_mu]; rw [E_passive_exact]
 881  have h_inv_lo := inv_4pi_lower_v2
 882  have h_inv_hi := inv_4pi_upper_v2
 883  have h_alpha := alpha_sq_bounds
 884  constructor <;> linarith
 885

used by (1)

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

predicted_residue_mu_bounds_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use

depends on (7)

Lean names referenced from this declaration's body.

alpha_sq_bounds in IndisputableMonolith.Physics.ElectronMass.Necessity decl_use
step_e_mu in IndisputableMonolith.Physics.LeptonGenerations.Defs decl_use
E_passive_exact in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
inv_4pi_lower_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
inv_4pi_upper_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
step_e_mu in IndisputableMonolith.RRF.Physics.LeptonGenerations.Defs decl_use
E_passive_exact in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use