Pith. sign in
module module moderate

IndisputableMonolith.StandardModel.ProtonMass

show as:
view Lean formalization →

The ProtonMass module assembles the proton mass from up and down valence contributions plus binding energy on the phi-ladder imported from MassHierarchy. Researchers verifying RS baryon mass predictions would cite the final m_p expression and its positivity lemmas. The module consists of a chain of definitions and one-line positivity statements with no complex proofs.

claimThe proton mass satisfies $m_p = m_{valence} + E_{binding}$ where $m_{valence}$ is assembled from $m_u$ and $m_d$ rung contributions on the $\phi$-ladder and $E_{binding}$ is the coherent binding term with $r_{binding}$ the associated length scale.

background

The module imports Constants (fundamental RS time quantum $ au_0 = 1$ tick) and MassHierarchy (P-002: Fermion Mass Hierarchy from $\phi$-Ladder, which formalizes the RS derivation of the fermion mass hierarchy). It defines auxiliary objects including anchor for coherent energy, mass on a given rung, separate u and d quark contributions, the combined valence mass, binding radius and energy, and the final proton mass together with positivity statements for each.

proof idea

This is a definition module, no proofs. It organizes the proton mass calculation as a sequence of auxiliary definitions followed by positivity assertions for each component.

why it matters in Recognition Science

This module supplies the explicit proton mass formula inside the StandardModel section, extending the fermion mass hierarchy of P-002. It realizes the lightest baryon case using the phi-ladder and binding dominance from the imported MassHierarchy results.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)