solar_correction_eq

formal source

 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
 125    weight in the dual lattice) gives 3/2. -/
 126def cabibbo_coefficient : ℚ := 3 / 2
 127
 128theorem cabibbo_coefficient_eq_3_2 : cabibbo_coefficient = 3/2 := rfl
 129
 130theorem cabibbo_coefficient_from_geometry :
 131    cabibbo_coefficient = (cube_faces 3 : ℚ) / 4 := by
 132  unfold cabibbo_coefficient cube_faces
 133  norm_num
 134
 135/-- The Cabibbo radiative correction is (3/2)α. -/
 136noncomputable def cabibbo_correction : ℝ := (cabibbo_coefficient : ℝ) * alpha
 137
 138theorem cabibbo_correction_eq : cabibbo_correction = (3/2) * alpha := by
 139  unfold cabibbo_correction cabibbo_coefficient
 140  norm_num
 141
 142/-! ## Verification Against MixingGeometry -/
 143
 144/-- Verify that our derived corrections match MixingGeometry definitions. -/