atmospheric_coefficient

formal source

  86    contributes one unit of vacuum polarization to the atmospheric mixing.
  87    The μ-τ sector, being maximally mixed (sin²θ₂₃ ≈ 1/2), receives a
  88    symmetric correction from all faces. -/
  89def atmospheric_coefficient : ℕ := cube_faces 3
  90
  91theorem atmospheric_coefficient_eq_6 : atmospheric_coefficient = 6 := rfl
  92
  93/-- The atmospheric radiative correction is 6α. -/
  94noncomputable def atmospheric_correction : ℝ := (atmospheric_coefficient : ℝ) * alpha
  95
  96theorem atmospheric_correction_eq : atmospheric_correction = 6 * alpha := by
  97  unfold atmospheric_correction atmospheric_coefficient
  98  rfl
  99
 100/-! ## Derivation of the Coefficient 10 (Solar) -/
 101
 102/-- The solar correction coefficient is edges minus the active pair.
 103
 104    **Physical interpretation**: The solar sector involves 2-step torsion
 105    (φ⁻² weight), coupling via edges. The 12 edges minus the 2 active
 106    modes (e and ν_e in the 1-2 sector) gives 10 passive contributions. -/
 107def solar_coefficient : ℕ := cube_edges_count 3 - 2
 108
 109theorem solar_coefficient_eq_10 : solar_coefficient = 10 := rfl
 110
 111/-- The solar radiative correction is 10α. -/
 112noncomputable def solar_correction : ℝ := (solar_coefficient : ℝ) * alpha
 113
 114theorem solar_correction_eq : solar_correction = 10 * alpha := by
 115  unfold solar_correction solar_coefficient
 116  rfl
 117
 118/-! ## Derivation of the Coefficient 3/2 (Cabibbo) -/
 119