def
definition
solar_coefficient
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.PMNSCorrections on GitHub at line 107.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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