E_coh
plain-language theorem explainer
E_coh sets the coherence energy scale to phi raised to the negative fifth power in dimensionless RS units. Mass derivations in the Recognition framework cite this constant to fix the base yardstick on the phi-ladder. The definition is a direct assignment that imports phi from the Constants bundle and applies the fixed exponent.
Claim. The coherence energy unit is $E_0 = phi^{-5}$, where $phi$ is the self-similar fixed point satisfying the Recognition Composition Law.
background
The Masses.Anchor module centralises parameter-free constants derived from cube geometry in D=3. It records E_total equal to twelve edges, E_passive equal to eleven, W equal to seventeen wallpaper groups, and A equal to one active edge per tick. Sector identifiers label lepton, up-quark, down-quark, and electroweak cases, each carrying its own B_pow and r0 exponents for the mass formula yardstick times phi to the rung power.
proof idea
The declaration is a direct noncomputable definition. It evaluates the imported phi constant to the integer power negative five and attaches the simp attribute for rewriting.
why it matters
This definition supplies the base energy for all rung-based mass expressions in the module. It anchors the phi-ladder after the forcing chain fixes phi at T6 and sets D=3 at T8. The module doc states that downstream code should import these values rather than duplicate literals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.