def
definition
atmospheric_weight
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.MixingGeometry on GitHub at line 57.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
54 ring
55
56/-- The atmospheric mixing weight (maximal parity mix). -/
57noncomputable def atmospheric_weight : ℝ := 1 / 2
58
59/-- The atmospheric radiative correction factor.
60 Estimated as Faces * alpha. -/
61noncomputable def atmospheric_radiative_correction : ℝ := 6 * Constants.alpha
62
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