E_coh
plain-language theorem explainer
E_coh supplies the coherent energy scale as phi raised to the negative coherence exponent. Researchers assembling lepton masses from the phi-ladder cite it to anchor the base energy unit once the exponent is fixed. The definition is a direct abbreviation that inserts the integer 5 obtained from 2^D - D at D = 3.
Claim. $E_ {coh} := phi^{-5}$, where the exponent equals the coherence exponent $2^D - D$ evaluated at spatial dimension $D = 3$.
background
The module T9 Electron Mass Definitions isolates core constants for the lepton sector to avoid import cycles. It derives these constants from cube geometry in D = 3 dimensions: cube_edges(3) = 12, active_edges_per_tick = 1, passive_field_edges = 11, and wallpaper_groups = 17. The coherence exponent is introduced as 2^D - D, which equals 5 and is called the Fibonacci deficit in the upstream result from Masses.CoherenceExponent.
proof idea
One-line definition that applies the coherence_exponent value of 5 directly to the power of phi. The local sibling coherence_exponent supplies the integer 5 via the same 2^D - D expression.
why it matters
This definition fixes the energy scale inside the T9 derivation chain for the electron mass. It removes a free parameter by tying the exponent to the geometric constraints of D = 3 (from T8) and the eight-tick octave structure. The result feeds the phi-ladder mass formula yardstick * phi^(rung - 8 + gap(Z)) once the rung for the electron is set at 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.