theorem proved term proof

`alpha_W_pos`

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

formal statement (Lean)

  57theorem alpha_W_pos : 0 < alpha_W := by

Term-mode proof.

  58  unfold alpha_W
  59  exact div_pos alpha_pos_aux sin2_theta_positive
  60
  61/-- α_W > α (since sin²θ_W < 1, dividing by it increases α). -/

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

weak_coupling_cert in IndisputableMonolith.StandardModel.WeakCoupling decl_use

Lean names referenced from this declaration's body.

sin2_theta_positive in IndisputableMonolith.Masses.ElectroweakMasses decl_use
alpha_W in IndisputableMonolith.QFT.RunningCouplings decl_use
alpha_pos_aux in IndisputableMonolith.StandardModel.WeakCoupling decl_use
alpha_W in IndisputableMonolith.StandardModel.WeakCoupling decl_use