atmospheric_correction

formal source

  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
 120/-- The Cabibbo correction coefficient is faces / 4.
 121
 122    **Physical interpretation**: The quark sector's 3-generation torsion
 123    (φ⁻³ weight) couples via face-diagonal paths. The 6 faces divided by
 124    4 (the number of vertices per face, or equivalently the vertex-edge