`cabibbo_correction_eq`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.PMNSCorrections
domain: Physics
line: 138 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.PMNSCorrections on GitHub at line 138.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 161  norm_num
 162
 163/-! ## Summary Certificate -/
 164
 165/-- Certificate that all correction coefficients are geometrically derived.
 166
 167    This proves that the integers 6, 10, 3/2 are NOT free parameters but
 168    are FORCED by the topology of the 3D cubic ledger. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.