coherence_exponent_eq

formal source

 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
 149
 150/-- Alternative using explicit values (for compatibility). -/