def
definition
coherence_exponent
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ElectronMass.Defs on GitHub at line 118.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
115/-- The coherence exponent: 2^D - D = 8 - 3 = 5 (Fibonacci deficit).
116 See Foundation.CoherenceExponent for the full derivation
117 via two independent routes (Fibonacci deficit and integration measure). -/
118def coherence_exponent : ℕ := 2 ^ D - D
119
120theorem coherence_exponent_eq : coherence_exponent = 5 := by
121 unfold coherence_exponent D; norm_num
122
123/-- Coherent Energy Scale E_coh = φ^{-coherence_exponent} = φ⁻⁵.
124 The exponent is structurally determined, not a free parameter. -/
125noncomputable def E_coh : ℝ := phi ^ (-(coherence_exponent : ℤ))
126
127/-- E_coh evaluates to φ⁻⁵. -/
128theorem E_coh_eq : E_coh = phi ^ (-5 : ℤ) := by
129 simp [E_coh, coherence_exponent_eq]
130
131/-! ## Electron Geometry -/
132
133/-- Electron rung r = 2.
134 This equals the baseline (generation 1 lepton). -/
135def electron_rung : ℤ := electron_baseline_rung
136
137/-- Verify electron_rung = 2. -/
138theorem electron_rung_eq : electron_rung = 2 := rfl
139
140/-- Electron charge q = -1 (in units of e). -/
141def electron_charge : ℤ := -1
142
143/-! ## Structural Mass Derivation -/
144
145/-- The Yardstick (Sector Scale): Y = 2^B · E_coh · φ^R0.
146 Using derived values: Y = 2^(-22) · φ^(-5) · φ^62. -/
147noncomputable def lepton_yardstick : ℝ :=
148 (2 : ℝ) ^ lepton_B * E_coh * phi ^ lepton_R0