theorem
proved
cabibbo_coefficient_from_geometry
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.PMNSCorrections on GitHub at line 130.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
157theorem cabibbo_matches :
158 cabibbo_correction = MixingGeometry.cabibbo_radiative_correction := by
159 unfold cabibbo_correction MixingGeometry.cabibbo_radiative_correction
160 unfold cabibbo_coefficient