theorem proved term proof

`sin2_lt_half`

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

formal statement (Lean)

  76theorem sin2_lt_half : sin2_theta_W_rs < 1/2 := sin2_theta_lt_half

Term-mode proof.

  77
  78/-- α_W > 2α (since sin²θ_W < 1/2). -/

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

alpha_W_gt_two_alpha in IndisputableMonolith.StandardModel.WeakCoupling decl_use

Lean names referenced from this declaration's body.

sin2_theta_lt_half in IndisputableMonolith.Masses.ElectroweakMasses decl_use
sin2_theta_W_rs in IndisputableMonolith.Masses.ElectroweakMasses decl_use