E_coh
plain-language theorem explainer
The declaration aliases the coherent energy from the Anchor module into the AnchorPolicy namespace as a noncomputable real number. Mass modelers cite this alias when composing rung-based predictions or applying the phi-ladder formula. The definition is a direct one-line re-export with no computation or lemmas.
Claim. Define the coherent energy by $E_0 := E_0^{(A)}$ where the right-hand side is the corresponding quantity supplied by the anchor module.
background
The AnchorPolicy module supplies abbreviations that configure mass calculations on the phi-ladder. Key siblings include rung, gap, and predict_mass, which together implement the yardstick scaling yardstick * phi^(rung - 8 + gap(Z)). The module imports Constants (providing RS-native units with c = 1, hbar = phi^{-5}) and the Anchor module that originates the base energy scale.
proof idea
This is a one-line abbreviation that directly re-exports Anchor.E_coh. No lemmas, tactics, or reductions are applied.
why it matters
The alias makes the coherent energy available inside policy definitions that feed mass predictions. It supports the Recognition Science mass formula and the transition from T5 J-uniqueness through the eight-tick octave to concrete particle masses. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.