E_coh_eq
plain-language theorem explainer
The coherent energy scale equals phi to the minus five. Researchers deriving lepton masses cite this to fix the energy scale in the Recognition Science framework. The proof reduces directly via simplification of the definition of E_coh together with the prior result that the coherence exponent equals five.
Claim. The coherent energy scale satisfies $E_{coh} = phi^{-5}$.
background
In the T9 electron mass definitions module, the coherent energy scale is introduced as the noncomputable definition E_coh = phi raised to the negative of the coherence exponent. The coherence exponent is fixed at five by the sibling theorem coherence_exponent_eq, which unfolds the definitions of coherence_exponent and D then applies norm_num. The module derives lepton sector constants from cube geometry in D equals three: twelve total edges, eleven passive field edges, and seventeen wallpaper groups, with the electron rung set at two as the baseline lepton generation.
proof idea
The proof is a one-line term-mode simplification that unfolds the definition of E_coh and applies the coherence_exponent_eq theorem.
why it matters
This supplies the energy scale for the structural mass in electron_structural_mass_forced, where it combines with lepton_B_eq and lepton_R0_eq to produce 2^{-22} times phi^{51}. It closes part of the T9 derivation chain that forces lepton constants from D equals three and the eight-tick octave. The parent theorem electron_structural_mass_forced uses it to confirm the mass formula without free parameters, and lepton_yardstick_eq_explicit applies it to equate the derived yardstick to its explicit form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.