def definition def or abbrev

`couplingRatio`

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

formal statement (Lean)

 145noncomputable def couplingRatio : ℝ :=

proof body

Definition body.

 146  -- tan(θ_W) = g'/g
 147  -- sin²(θ_W) = g'² / (g² + g'²) ≈ 0.223
 148  Real.sqrt (sin2ThetaW / (1 - sin2ThetaW))
 149
 150/-- **THEOREM**: tan(θ_W) ≈ 0.536. -/

depends on (1)

Lean names referenced from this declaration's body.

sin2ThetaW in IndisputableMonolith.StandardModel.WZMassRatio decl_use