E_binding
plain-language theorem explainer
Binding energy for the proton is defined by applying the mass-on-rung function at the confinement level 14. This supplies the dominant contribution to m_p in the Recognition Science derivation, separating it from the small valence term at rung 4. The definition is a direct substitution of the fixed rung into the general mass formula.
Claim. $E_ {binding} := E_{coh} · ϕ^{14}$ in RS units, where $E_{coh}$ is the anchor coherence energy and ϕ the golden-ratio fixed point.
background
The module decomposes the proton mass into valence quarks (~1 percent) at rung 4 and QCD binding (~99 percent) at the confinement rung. mass_on_rung(r) returns Anchor.E_coh times ϕ^r, the general mass formula on the phi-ladder. r_binding is the integer constant 14 that places confinement ten rungs above the valence scale, producing the ϕ^{10} separation stated in the module documentation.
proof idea
This is a one-line definition that applies mass_on_rung to the constant r_binding = 14.
why it matters
E_binding supplies the dominant term in the proton-mass definition m_p := m_valence + E_binding. It is invoked to prove positivity of the binding energy and to establish that binding exceeds the valence contribution by more than a factor of 40. The definition realizes the phi-ladder structure for confinement inside the C-008 derivation and is consistent with the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.