coherence_exponent_eq
The coherence exponent equals 5 as the difference between the eight-tick octave period and three spatial dimensions. Researchers deriving lepton masses on the phi-ladder would cite this to fix the coherent energy scale without free parameters. The proof is a term-mode one-liner that unfolds the definition coherence_exponent := octave - D and normalizes the arithmetic.
claimThe coherence exponent, defined as the difference between the octave period and the spatial dimension $D$, equals 5.
background
In the T9 Electron Mass Definitions module the lepton sector constants are derived from cube geometry with $D=3$. The coherence exponent appears as octave minus $D$, representing the Fibonacci deficit $2^D - D$. The upstream definition in Masses.CoherenceExponent states: 'The Fibonacci deficit: 2^D - D = 5' and sets coherence_exponent : ℕ := octave - D. This module separates definitions from theorems to break import cycles and rests on the eight-tick octave (T7) together with $D=3$ (T8).
proof idea
The proof is a term-mode one-liner. It unfolds the definition of coherence_exponent as octave minus D, then applies norm_num to reduce the expression to the numeral 5 given the constants octave = 8 and D = 3.
why it matters in Recognition Science
This theorem supplies the fixed exponent for the downstream result E_coh_eq : E_coh = phi ^ (-5 : ℤ). It anchors the coherent energy scale in the electron mass derivation chain, where the exponent is forced by the eight-tick octave (T7) and three dimensions (T8) rather than chosen freely. The value 5 is consistent with the Recognition Composition Law and the phi-ladder mass formula; it closes the structural step that sets E_coh = phi^{-5} for the lepton sector.
scope and limits
- Does not derive the octave period or the value of D.
- Does not address higher lepton generations or other sectors.
- Does not incorporate the full mass formula with rung and gap terms.
- Does not treat empirical adjustments or renormalization.
Lean usage
theorem E_coh_eq : E_coh = phi ^ (-5 : ℤ) := by simp [E_coh, coherence_exponent_eq]formal statement (Lean)
120theorem coherence_exponent_eq : coherence_exponent = 5 := by
proof body
Term-mode proof.
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. -/