def
definition
cabibbo_coefficient
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.PMNSCorrections on GitHub at line 126.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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. -/
145theorem atmospheric_matches :
146 atmospheric_correction = MixingGeometry.atmospheric_radiative_correction := by
147 unfold atmospheric_correction MixingGeometry.atmospheric_radiative_correction
148 unfold atmospheric_coefficient
149 rfl
150
151theorem solar_matches :
152 solar_correction = MixingGeometry.solar_radiative_correction := by
153 unfold solar_correction MixingGeometry.solar_radiative_correction
154 unfold solar_coefficient
155 rfl
156