solar_coefficient_eq_10

formal source

 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
 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