module module high

`IndisputableMonolith.Physics.MassHierarchy`

The MassHierarchy module supplies definitions for charged lepton masses in GeV together with up and down quark masses, observed values, cascade relations, and the Koide parameter. Particle physicists modeling spectra from the phi-ladder would cite these objects when comparing Recognition Science predictions to data. The module is a collection of definitions and short lemmas with no complex proofs.

claimDefines charged lepton masses $(m_e, m_μ, m_τ)$ in GeV, up-quark masses, down-quark masses, the Koide parameter $K$, and the cascade mass function linked to the Higgs field via the phi-ladder.

background

The module sits in the Physics domain and imports the Constants module, whose fundamental object is the RS time quantum τ₀ = 1 tick. It introduces sibling definitions including ChargedLeptonMasses, observedLeptons, UpQuarkMasses, DownQuarkMasses, cascadeMass, koideParameter, and phi_cascade_from_higgs. These objects encode the mass hierarchy on the phi-ladder with parameters such as rung and gap(Z).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete mass objects that feed into higher-level Recognition Science results on particle spectra and the mass formula yardstick * phi^(rung - 8 + gap(Z)). It fills the mass-hierarchy step that connects the phi fixed point to observed lepton and quark values.

scope and limits

Does not derive masses from the forcing chain T0-T8.
Does not include neutrino masses or mixing angles.
Does not prove numerical agreement with experiment beyond definitions.
Does not address running of masses with energy scale.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (21)

structure ChargedLeptonMasses L52
def observedLeptons L58
structure UpQuarkMasses L65
def observedUpQuarks L71
structure DownQuarkMasses L78
def observedDownQuarks L84
def cascadeMass L94
theorem cascade_decreases L98
def koideParameter L121
theorem koide_is_two_thirds L126
theorem phi_cascade_from_higgs L140
structure CascadeParameters L147
def leptonParams L156
theorem three_generations_from_8_tick L168
theorem no_fourth_generation L174
theorem georgi_jarlskog L185
theorem up_quark_hierarchy L192
def predictions L203
theorem fermion_mass_prediction L212
structure MassHierarchyFalsifier L224
def experimentalStatus L231