theorem
proved
atmospheric_angle_forced
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 66.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
63/-- **THEOREM: Atmospheric Angle Forced**
64 The atmospheric mixing angle is derived from the maximal parity mix
65 with a face-mediated radiative correction. -/
66theorem atmospheric_angle_forced :
67 atmospheric_weight + atmospheric_radiative_correction = 1 / 2 + 6 * Constants.alpha := by
68 unfold atmospheric_weight atmospheric_radiative_correction
69 ring
70
71/-- The reactor mixing weight (octave closure). -/
72noncomputable def reactor_weight : ℝ := phi ^ (-8 : ℤ)
73
74/-! ## Quarter-Ladder Steps (Quark Sector) -/
75
76/-- Step from Top to Bottom: 7.75 rungs. -/
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