E_binding_pos
plain-language theorem explainer
The theorem shows that the binding energy contribution to the proton mass is strictly positive. A physicist deriving the proton mass within Recognition Science would cite this result to confirm the dominance of the confinement term over valence quarks. The proof is a one-line wrapper that unfolds the binding energy definition and applies the general positivity lemma for the mass on any integer rung of the phi-ladder.
Claim. $0 < E$ where $E$ is the mass contribution evaluated at rung 14 on the phi-ladder.
background
The module derives the proton mass as the sum of a small valence quark term at rung 4 and a large QCD binding term at the confinement rung. Here the binding energy is defined as the mass_on_rung function applied at r_binding equal to 14. The key upstream result is the lemma establishing positivity of mass_on_rung r for any integer r, obtained by multiplying the positive anchor coherence energy by a positive power of phi. The module document states that this binding term accounts for approximately 99 percent of the proton mass due to the rung separation of 10, which produces a factor of phi to the 10.
proof idea
This is a one-line wrapper proof. It first unfolds the definitions of the binding energy and the binding rung, then directly applies the positivity lemma for the mass on rung function at the specific value 14.
why it matters
The result is used in the proof that the full proton mass is positive, via linear arithmetic combining the valence and binding contributions. It completes the binding energy positivity step in the C-008 proton mass derivation. In the broader framework it supports the mass formula on the phi-ladder and the claim that binding dominates valence quarks by the large rung difference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.