IndisputableMonolith.Support.RungFractions
This module defines the Rung type and its constructors for possibly fractional positions on the phi-ladder. Neutrino mass modelers cite it when placing particles on deep even-integer rungs far below the electron. The module supplies only definitions and basic conversion lemmas with no theorems proved.
claimA rung \( r \) on the \(\phi\)-ladder, possibly fractional, equipped with constructors ofInt, quarter, half and the map toReal.
background
Recognition Science places particle masses on a phi-ladder via the formula yardstick times phi to the power (rung minus 8 plus gap(Z)). The Rung type extends integer rungs to fractions so that neutrino masses can occupy deep even-integer positions around rung -50. The module is imported by NeutrinoSector (T14) and NeutrinoMassScaleScoreCard to support fractional rung placement and squared-mass predictions.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
Supplies the rung objects required by NeutrinoSector (T14: derivation of the neutrino mass scale on the deep ladder) and by NeutrinoMassScaleScoreCard (phase-2 neutrino mass bands and phi^7 structural relation). It closes the support layer that lets fractional rungs enter the T14 hypothesis.
scope and limits
- Does not prove any properties of the phi-ladder itself.
- Does not encode the mass formula or gap function.
- Does not restrict the allowed range of fractional rungs.
- Does not connect rungs to specific particle species.