pith. sign in
module module moderate

IndisputableMonolith.Constants.ProtonElectronMassRatio

show as:
view Lean formalization →

This module supplies RS-native definitions for the proton-electron mass ratio and related constants such as m_e. It assembles structural relations from the φ-ladder in MassHierarchy together with anchor masses. Researchers working on P-002 fermion hierarchy derivations cite these objects when expressing ratios without free parameters. The module is purely definitional with no theorems or proofs.

claim$m_e = E_{ m coh} \cdot \phi^2$ (C-007, $r_e=2$); $m_p/m_e$ obtained from structural ladder relations on the $\phi$-ladder with gap terms.

background

The module sits inside the Constants domain and imports the RS time quantum $ au_0=1$ tick, the canonical mass constants derived from first principles, and the P-002 fermion mass hierarchy. Electron mass is expressed directly as $E_{ m coh} \cdot \phi^2$. The $\phi$-ladder supplies rung and gap(Z) exponents for all fermion masses in RS units.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the concrete mass-ratio objects required by the P-002 derivation chain in MassHierarchy. The structural and ladder-based definitions close the parameter-free route from the Recognition Composition Law and T5 J-uniqueness to observable fermion ratios.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (5)