Pith. sign in
module module moderate

IndisputableMonolith.Constants.ProtonElectronMassRatio

show as:
view Lean formalization →

Constants.ProtonElectronMassRatio assembles electron mass and proton-electron ratio expressions from the phi-ladder in MassHierarchy together with anchor values. Researchers deriving RS particle masses cite these when mapping the observed ratio near 1836 onto the ladder rungs. The module consists entirely of structural definitions and implications with no proved theorems.

claim$m_e = E_{ m coh} \cdot \phi^2$ (C-007, $r_e=2$), with the proton-electron ratio obtained structurally from the $\phi$-ladder and gap parameters.

background

The module lives in the Constants domain of Recognition Science and imports the base time quantum $\tau_0=1$ tick, the canonical mass anchors, and the fermion mass hierarchy (P-002). Electron mass is placed at rung 2 on the ladder as $E_{ m coh} \cdot \phi^2$. The setting follows the mass manuscripts where all constants remain parameter-free and live in the Model layer.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These ratio definitions extend the P-002 fermion mass hierarchy to the specific proton-electron pair and supply concrete expressions for the broader constant derivations in the Recognition Science framework.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (5)