m_valence_pos
The valence quark mass contribution to the proton is shown positive by expressing it as a linear combination of two instances of the mass-on-rung function evaluated at rung 4. Researchers assembling the proton mass from the phi-ladder within Recognition Science cite this when confirming that the small valence piece does not cancel the dominant binding term. The proof unfolds the three definitions and applies linear arithmetic to the known positivity of mass on rung 4.
claimLet $m_u$ and $m_d$ each equal the mass on rung 4 of the phi-ladder. Then the valence contribution satisfies $m_mathrm{valence} = 2m_u + m_d > 0$.
background
The module derives the proton mass as the sum of a valence-quark term from the phi-ladder at rung 4 and a binding term from the higher confinement rung. The auxiliary function mass_on_rung r returns a positive real for any integer r, obtained as the product of the positive anchor coherence energy and a positive integer power of phi. Both up and down contributions are defined to be exactly mass_on_rung 4, so the valence mass is their weighted sum 2 m_u + m_d. This construction appears inside the C-008 derivation that separates the ~1 percent valence piece from the ~99 percent binding piece.
proof idea
The term proof first unfolds m_valence, m_u_contrib and m_d_contrib, exposing the expression 2*(mass_on_rung 4) + (mass_on_rung 4). It then supplies the lemma mass_on_rung_pos applied at rung 4, whose own proof rests on the positivity of the anchor energy and of phi to any integer power. Linear arithmetic finishes the argument that the resulting sum is positive.
why it matters in Recognition Science
The result is invoked by the downstream theorem establishing positivity of the full proton mass m_p, which adds the valence term to the binding term. It supplies the required positivity step in the C-008 proton-mass derivation before the binding energy from rung 14 is adjoined. Within the Recognition Science chain it confirms that the phi-ladder mass formula at low rungs remains positive, consistent with the eight-tick octave and the separation of valence and confinement scales.
scope and limits
- Does not compute a numerical value in MeV for the valence contribution.
- Does not derive or bound the binding-energy term.
- Does not address higher-order QCD corrections beyond the ladder.
- Does not establish positivity for mass contributions at other rungs.
Lean usage
theorem m_p_pos : 0 < m_p := by unfold m_p; linarith [m_valence_pos, E_binding_pos]formal statement (Lean)
38theorem m_valence_pos : 0 < m_valence := by
proof body
Term-mode proof.
39 unfold m_valence m_u_contrib m_d_contrib
40 linarith [mass_on_rung_pos 4]
41