pith. sign in
module module high

IndisputableMonolith.Masses.MassHierarchy

show as:
view Lean formalization →

The MassHierarchy module supplies the basic mass expression in Recognition Science units as coherence energy scaled by a power of phi on the ladder. Researchers deriving the proton-electron ratio, lepton masses, or resolving the hierarchy problem cite it as the common starting point. It is a definition module with no internal proofs.

claimMass in RS units is given by $m = E_{ m coh} \cdot \phi^r$, where $r$ is the integer rung on the $\phi$-ladder.

background

The module imports the RS time quantum $ au_0 = 1$ tick from Constants, the proof that $\phi$ is forced by self-similarity in a discrete ledger with J-cost from PhiForcing, and the canonical mass constants from Anchor. PhiForcing states: "This module proves that $\phi$ is forced by self-similarity in a discrete ledger with J-cost." Anchor states: "This module centralises the parameter-free constants described in the mass manuscripts." The supplied doc-comment defines the local object: mass equals coherence energy times $\phi$ to the rung power.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the mass expression used by the derivations of the proton-to-electron mass ratio (C-009), the lepton mass ladder (P-011), the hierarchy problem dissolution (P-013), and the proton mass (C-008). It therefore sits at the base of the mass-related registry items in the Recognition Science chain.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (6)