Pith. sign in
module module moderate

IndisputableMonolith.Physics.NeutrinoMassFromPhiLadder

show as:
view Lean formalization →

Module defines the three active neutrino mass eigenstates on the phi-ladder. Particle physicists working in RS mass hierarchies cite these values for the neutrino sector. It consists of definitions that instantiate the general mass formula yardstick * phi^(rung-8+gap(Z)) for neutrinos using normal ordering and explicit mass ratios.

claimThe three neutrino mass eigenstates satisfy $m_i = au_0^{-1} \phi^{r_i-8+ ext{gap}(Z)}$ for rungs $r_i$ in normal ordering, with fixed mass ratio $m_2/m_3$ on the ladder.

background

The module sits inside the Recognition Science derivation of particle masses from the phi-ladder. It imports the Constants module whose sole content is the base time quantum $\tau_0=1$ tick. Sibling definitions neutrinoMass, normal_ordering, mass_ratio, and NeutrinoMassCert implement the rung assignments and gap corrections for the three active states.

The local setting is the mass formula yardstick * phi^(rung-8+gap(Z)) applied to the neutrino sector after the J-uniqueness and phi fixed-point steps of the forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the neutrino mass values required by the Recognition Science particle spectrum. It completes the neutrino rung assignments that feed the overall mass ladder used in downstream physics modules. The construction directly instantiates the phi-ladder mass rule after T5-T8 of the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)