m_p_pos
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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of m_p in MeV.
- Does not derive or justify the rung numbers 4 and 14.
- Does not include electromagnetic or weak corrections.
- Does not extend to other baryons or the full hadron spectrum.
formal statement (Lean)
80theorem m_p_pos : 0 < m_p := by
proof body
Term-mode proof.
81 unfold m_p; linarith [m_valence_pos, E_binding_pos]
82
83end
84
85end ProtonMass
86end StandardModel
87end IndisputableMonolith