m_p_pos
plain-language theorem explainer
The declaration establishes strict positivity of the proton mass constructed from valence quarks and QCD binding on the phi-ladder. Researchers deriving hadron masses in Recognition Science would cite it to confirm physical consistency of the additive decomposition. The proof is a one-line term-mode reduction that unfolds the mass definition and invokes linear arithmetic on the separate positivity results for each component.
Claim. $m_p > 0$, where $m_p = m_{valence} + E_{binding}$, $m_{valence}$ is the valence quark contribution at rung 4, and $E_{binding}$ is the binding energy at confinement rung 14.
background
The StandardModel.ProtonMass module derives the proton mass as the sum of a small valence term from the phi-ladder at rung 4 and a dominant binding term at rung 14. The module doc states that binding dominates because the confinement rung is much higher, giving a phi^10 separation factor. Both components are obtained from the general mass_on_rung_pos lemma applied at the respective rungs.
proof idea
The proof is a one-line term proof. It unfolds the definition m_p := m_valence + E_binding, then applies linarith to the upstream theorems m_valence_pos and E_binding_pos.
why it matters
This theorem supplies the positivity check required for the proton mass formula in the Recognition Science mass hierarchy. It rests on the phi-ladder mass formula and the rung assignments given in the module doc, consistent with the self-similar fixed point phi and the eight-tick octave structure. No downstream uses are recorded, so the result functions as a local consistency lemma within the Standard Model derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.