`cabibbo_correction`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.PMNSCorrections on GitHub at line 136.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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
 161  norm_num
 162
 163/-! ## Summary Certificate -/
 164
 165/-- Certificate that all correction coefficients are geometrically derived.
 166

papers checked against this theorem

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