def
definition
step_bottom_charm
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.MixingGeometry on GitHub at line 80.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
77def step_top_bottom : ℚ := 31 / 4
78
79/-- Step from Bottom to Charm: 2.50 rungs. -/
80def step_bottom_charm : ℚ := 10 / 4
81
82/-- Step from Charm to Strange: 5.50 rungs. -/
83def step_charm_strange : ℚ := 22 / 4
84
85/-- The radiative correction factor for the Cabibbo angle.
86 Represented as 1.5 * alpha, derived from 6 faces / 4 vertex-edge weight. -/
87noncomputable def cabibbo_radiative_correction : ℝ := (3/2) * Constants.alpha
88
89/-- **THEOREM: Cabibbo Scaling Forced**
90 The Cabibbo scaling factor is forced by the torsion overlap and the
91 face-mediated radiative corrections. -/
92theorem cabibbo_scaling_forced :
93 torsion_overlap - cabibbo_radiative_correction = phi ^ (-3 : ℤ) - (3/2) * Constants.alpha := by
94 unfold torsion_overlap cabibbo_radiative_correction
95 ring
96
97end MixingGeometry
98end Physics
99end IndisputableMonolith