anchor_E_coh_pos
plain-language theorem explainer
Anchor coherence energy positivity is established for the phi-ladder base in proton mass calculations. Researchers deriving masses from the Recognition Science framework cite this to guarantee positive contributions from all rungs. The proof reduces directly to the known positivity of phi raised to any integer power.
Claim. $0 < E_{coh}$ where $E_{coh}$ is the anchor coherence energy at the base of the phi-ladder mass formula.
background
In the proton mass module the phi-ladder supplies valence quark masses at rung 4 and binding energy at rung 14. Anchor E_coh is the positive base factor such that mass on rung r equals E_coh multiplied by phi^r. Positivity of the anchor therefore propagates to every derived mass term via multiplication by positive powers of phi. The module derives the proton mass as the sum of valence and binding contributions, with binding dominant because the confinement rung lies ten steps higher.
proof idea
The proof is a one-line wrapper that applies zpow_pos to phi_pos.
why it matters
The lemma is invoked inside binding_dominates to compare binding and valence energies and inside mass_on_rung_pos to establish positivity of every rung mass. It supplies the base positivity required by the C-008 proton mass formula, connecting directly to the phi self-similar fixed point and the mass formula yardstick times phi to the (rung minus 8 plus gap).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.