pith. sign in
module module high

IndisputableMonolith.StandardModel.ProtonMass

show as:
view Lean formalization →

The StandardModel.ProtonMass module assembles the proton mass m_p from the phi-ladder hierarchy. It defines up and down quark contributions, valence mass, binding radius, and binding energy using RS constants before stating the total. A researcher deriving Standard Model masses from Recognition Science would cite this module for the explicit proton value. The structure is a chain of definitions followed by positivity statements for each auxiliary quantity.

claim$m_p = m_{valence} + E_{binding}$ where $m_{valence} = m_{u,contrib} + m_{d,contrib}$, each term scaled by the yardstick on the appropriate rung of the phi-ladder, and $E_{binding}$ follows from the coherence energy anchor.

background

Recognition Science derives physics from the single J-functional equation whose self-similar fixed point is phi. The imported Constants module supplies the RS time quantum tau_0 = 1 tick in native units. The MassHierarchy module (P-002) formalizes the fermion mass hierarchy: masses are given by yardstick times phi to the power (rung minus 8 plus gap(Z)) on the phi-ladder. This ProtonMass module specializes that hierarchy to the proton by separating valence quark pieces and adding a binding correction.

proof idea

This is a definition module whose argument proceeds by successive definitions. It first anchors the coherence energy, defines mass on rung, then up and down contributions, valence mass, binding radius and energy, and finally assembles m_p together with its positivity statement. Each step is a direct definition or elementary positivity lemma.

why it matters in Recognition Science

This module supplies the concrete proton mass that completes the Standard Model mass sector inside Recognition Science. It directly applies the P-002 fermion mass hierarchy from the MassHierarchy import. The result feeds any downstream Standard Model construction that requires an explicit m_p value. It touches the numerical agreement of the derived proton mass with observation inside the alpha band.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)