m_p
plain-language theorem explainer
The proton mass is defined as the sum of the valence quark contribution from the phi-ladder and the dominant QCD binding energy at the confinement rung. Recognition Science derivations of the proton-to-electron mass ratio cite this decomposition to obtain the structural form phi to a power. The definition is a direct one-line sum of the two sibling definitions m_valence and E_binding.
Claim. $m_p = m_{valence} + E_{binding}$, where $m_{valence} = 2 m_{u,contrib} + m_{d,contrib}$ is the sum of up- and down-quark contributions on the phi-ladder at rung 4 and $E_{binding}$ is the mass evaluated on the confinement rung of the same ladder.
background
Module C-008 derives the proton mass from the Recognition Science phi-ladder. Valence quarks supply roughly 1 percent at rung 4 while binding supplies 99 percent at the higher confinement rung, yielding the separation phi^10. The sibling definition m_valence expands to twice the up-quark term plus the down-quark term; E_binding is defined as mass_on_rung applied at r_binding. Upstream, mass_on_rung itself comes from the MassHierarchy module that places all masses on the self-similar phi-ladder fixed point.
proof idea
One-line definition that directly adds the two sibling definitions m_valence and E_binding.
why it matters
This definition supplies the explicit proton mass expression required by C-008 and is invoked by downstream results including proton_electron_ratio_from_ladder and mass_ratio_structural. Those theorems convert the definition into the parameter-free ratio m_p / m_e = phi^(r_p - 2). The construction sits inside the T5-T6 forcing chain that fixes phi and the eight-tick octave, and it closes the gap between the valence rung and the confinement rung that sets D = 3 spatial dimensions. The exact integer value of r_binding remains open and is constrained only by the measured ratio 1836.15.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.