pith. sign in
module module high

IndisputableMonolith.Constants.ProtonElectronMassRatio

show as:
view Lean formalization →

The ProtonElectronMassRatio module assembles definitions and structural relations for the proton-electron mass ratio on the phi-ladder in Recognition Science. Researchers deriving fermion masses from first principles would cite its ladder-based results. It organizes the electron mass as E_coh · φ² together with ratio implications drawn from the imported mass hierarchy.

claimThe electron mass satisfies $m_e = E_{coh} · φ^2$ (with rung offset from C-007). The proton-electron ratio is the structural difference $m_p / m_e = φ^{r_p - r_e + gap}$ on the phi-ladder.

background

Recognition Science places all masses on the phi-ladder with the formula yardstick · φ^(rung - 8 + gap(Z)). The upstream MassHierarchy module formalizes P-002, the fermion mass hierarchy derivation from this ladder. The Anchor module centralizes the resulting parameter-free constants, while Constants supplies the base time quantum τ₀ = 1 tick. This module imports those three and adds the specific proton-electron ratio on top of the electron mass definition E_coh · φ².

proof idea

This is a definition module, no proofs. It supplies the electron mass definition, the structural ratio lemma, the ladder extraction, and the phi-gap implication as sibling declarations.

why it matters in Recognition Science

The module supplies the concrete proton-electron ratio needed by the fermion mass hierarchy in P-002. It closes the ladder step for the lightest two fermions and feeds the mass formula used throughout the Recognition framework.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (5)