pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Masses.MassHierarchy

show as:
view Lean formalization →

MassHierarchy supplies the RS mass formula E_coh · φ^r on the phi-ladder. Particle physicists deriving lepton and hadron masses from self-similarity cite it to link the J-cost ledger to the observed spectrum. The module is purely definitional, importing constants, phi forcing, and anchors to expose rung-based mass functions without internal theorems.

claimParticle mass in RS units takes the form $m = E_coh · φ^r$, where $r$ is the integer rung on the φ-ladder and $E_coh$ is the coherent energy scale set by the model.

background

The module operates in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants, the forcing of φ as the self-similar fixed point of the J-cost ledger from PhiForcing, and the canonical mass constants from Anchor. PhiForcing states that φ is forced by self-similarity in a discrete ledger with J-cost. Anchor centralises the parameter-free constants described in the mass manuscripts. The phi-ladder itself is the discrete scale structure generated by repeated application of the Recognition Composition Law.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

MassHierarchy supplies the rung parameterization that downstream modules apply to concrete particles. It feeds the proton-to-electron mass ratio (C-009), the lepton mass ladder for μ and τ (P-011), the proton mass derivation (C-008), and the hierarchy problem dissolution (P-013). Each of those modules imports the mass_on_rung and rung-assignment definitions to obtain parameter-free expressions from the same φ-ladder.

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)