pith. machine review for the scientific record. sign in
def definition def or abbrev

runningAngle

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)

 169noncomputable def runningAngle (logEnergy : ℝ) : ℝ :=

proof body

Definition body.

 170  sin2ThetaW_GUT * (1 - logEnergy / (16 * Real.pi^2))
 171
 172/-! ## The Deep Connection -/
 173
 174/-- The Weinberg angle encodes fundamental information:
 175
 176    1. **Charge quantization**: Q = I₃ + Y/2, where I₃ and Y mix by θ_W
 177    2. **Mass relations**: m_W = m_Z × cos(θ_W)
 178    3. **Coupling unification**: At high energy, couplings merge
 179
 180    In RS, all three emerge from the 8-tick structure with φ-optimization. -/

depends on (16)

Lean names referenced from this declaration's body.