runningAngle

formal source

 166    sin²(θ_W)(E) = sin²(θ_W)(GUT) × (1 - α log(E/E_GUT))
 167
 168    where α involves φ. -/
 169noncomputable def runningAngle (logEnergy : ℝ) : ℝ :=
 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. -/
 181def deepConnections : List String := [
 182  "Charge quantization from discrete phases",
 183  "Mass ratio from φ-constrained symmetry breaking",
 184  "Unification from φ-ladder convergence"
 185]
 186
 187/-! ## Experimental Tests -/
 188
 189/-- The Weinberg angle is one of the most precisely measured quantities in physics.
 190
 191    | Measurement | Value | Error |
 192    |-------------|-------|-------|
 193    | LEP (Z pole) | 0.2312 | 0.0002 |
 194    | SLD (asymmetries) | 0.2310 | 0.0002 |
 195    | Moller scattering | 0.2403 | 0.0013 |
 196    | νN DIS | 0.2277 | 0.0016 |
 197    | APV (Cs) | 0.2356 | 0.0020 |
 198
 199    The variation with energy ("running") is also measured. -/