IndisputableMonolith.Support.RungFractions
Support module defining fractional rungs on the φ-ladder: a rung type with integer embedding, quarter and half constructors, and a map to real values. Neutrino-sector work cites it for non-integer ladder placements (e.g. half-integer residue gaps). Definitions and elementary equalities only; no deep theorems.
claimA rung is a (possibly fractional) index on the $\varphi$-ladder. The module supplies an integer embedding, canonical quarter and half rungs, a real-valued evaluation map, and the identities that the quarter and half constructors evaluate as expected.
background
Recognition Science places particle masses on a discrete $\varphi$-ladder: mass scales as a yardstick times $\varphi$ raised to a rung offset (with charge-dependent gap). Integer rungs suffice for charged leptons and quarks; the neutrino sector needs fractional steps so that squared-mass ratios can sit at half-integer residue gaps (notably a gap of $7/2$ yielding the structural ratio $\varphi^7$).
This support module isolates that bookkeeping. A rung is an abstract ladder index that may be fractional. Integer rungs embed via a constructor; quarter and half supply the standard dyadic fractions used downstream; evaluation to $\mathbb{R}$ turns a rung into the exponent that enters the mass formula. The local setting is pure arithmetic support: Mathlib only, no physics axioms.
proof idea
This is a definition module, no substantive proofs. It introduces the rung type and the constructors ofInt, quarter, and half, the real evaluation map, and two elementary equalities identifying the real values of the quarter and half constructors. Argument structure is definitional equality and basic arithmetic, not a forcing or uniqueness argument.
why it matters in Recognition Science
Fractional rungs are the arithmetic substrate for the neutrino mass-scale program. NeutrinoSector (T14) formalizes neutrinos on the deep ladder far below the electron rung $R_e = 2$, and needs non-integer indices for even-integer placements in the $-50$ range and for residue gaps. NeutrinoMassScaleScoreCard (Phase 2, P2-$\nu$) scores fractional-ladder predictions against NuFit $\Delta m^2$ windows and the structural claim $m_3^2/m_2^2 = \varphi^7$ in the $\mathrm{res}{\nu 3}-\mathrm{res}{\nu 2}=7/2$ model. Without a shared fractional-rung type, those modules cannot state ladder placement or convert residues into real exponents cleanly. The module does not itself derive masses or fix $\varphi$; it only standardizes the index type the mass formula consumes.
scope and limits
- Does not derive neutrino masses, mixings, or NuFit band membership.
- Does not force $\varphi$, the eight-tick octave, or spatial dimension $D=3$.
- Does not prove uniqueness of fractional placements on the ladder.
- Does not define the mass yardstick, gap function, or full $\varphi$-ladder mass formula.
- Does not assert which physical species occupy which fractional rungs.