def
definition
solar_weight
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.MixingGeometry on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
39noncomputable def torsion_overlap : ℝ := phi ^ (-3 : ℤ)
40
41/-- The solar mixing weight (2-step torsion gap). -/
42noncomputable def solar_weight : ℝ := phi ^ (-2 : ℤ)
43
44/-- The solar radiative correction factor.
45 Estimated as (E_passive - 1) * alpha. -/
46noncomputable def solar_radiative_correction : ℝ := 10 * Constants.alpha
47
48/-- **THEOREM: Solar Angle Forced**
49 The solar mixing angle is derived from the phi^-2 scaling with a
50 10-alpha radiative correction. -/
51theorem solar_angle_forced :
52 solar_weight - solar_radiative_correction = phi ^ (-2 : ℤ) - 10 * Constants.alpha := by
53 unfold solar_weight solar_radiative_correction
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 : ℤ)