m_valence
plain-language theorem explainer
The definition sets the valence quark contribution to proton mass as twice the up-quark term plus the down-quark term, each taken from the phi-ladder at rung 4. A physicist working on the Recognition Science mass hierarchy would cite this split when isolating the small valence piece before adding binding energy. The definition is a direct linear combination of the two sibling quark contribution definitions.
Claim. The valence mass contribution is defined by $m_ {valence} := 2 m_{u, contrib} + m_{d, contrib}$, where each quark contribution equals the mass evaluated on rung 4 of the phi-ladder.
background
The module derives the proton mass by separating valence quarks from QCD binding energy. Valence quarks sit at rung 4 on the phi-ladder while binding uses the higher confinement rung, producing a factor of phi^10 separation. The module states that valence quarks supply roughly 1 percent of the total mass.
proof idea
This is a direct definition that adds the down-quark contribution to twice the up-quark contribution. Both quark terms are supplied by the sibling definitions that evaluate mass on rung 4.
why it matters
The definition supplies the valence term that enters the total proton mass definition and the binding-dominates comparison showing binding exceeds forty times the valence mass. It implements the first step of the C-008 proton mass derivation in the Recognition Science framework, placing valence quarks at rung 4 on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.