pith. sign in
module module high

IndisputableMonolith.Masses.MassHierarchy

show as:
view Lean formalization →

The MassHierarchy module supplies the rung-based mass assignments in RS units, with each mass expressed as the coherent energy scale times a power of phi. It is imported by lepton mass, proton mass, and hierarchy dissolution derivations. The module contains only definitions and re-exports, with no internal theorem proofs.

claim$m(r) = E_{ m coh} \cdot \phi^r$ for rung index $r$ on the phi-ladder.

background

The module resides in the Masses domain and imports the RS time quantum tau_0 from Constants, the self-similarity argument that forces phi from PhiForcing, and the canonical mass constants from Anchor. PhiForcing states that phi is forced by self-similarity in a discrete ledger with J-cost. Anchor centralises the parameter-free constants described in the mass manuscripts, with everything in the Model layer.

The supplied doc comment gives the core relation: Mass in RS units: E_coh · φ^r where r is the rung. Sibling definitions include mass_on_rung, r_electron, r_muon, r_tau, lepton_hierarchy_geometric, and lepton_mass_increasing.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the mass ladder used by downstream modules: ProtonElectronMassRatio for the proton-to-electron ratio, HierarchyDissolution for the hierarchy problem resolution, LeptonMassLadder for muon and tau masses, and ProtonMass for the proton mass derivation from valence quarks and QCD binding. The module fills the mass hierarchy step in the RS chain that begins from PhiForcing and Anchor.

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)