coherence_exponent_eq
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.