def
definition
cabibbo_coefficient
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 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