pith. sign in
module module moderate

IndisputableMonolith.Support.RungFractions

show as:
view Lean formalization →

Support.RungFractions defines the type of a possibly fractional rung on the phi-ladder together with quarter, half, and toReal operations. Neutrino mass modelers cite it when placing neutrinos on the deep ladder at even integers near -50. The module supplies only definitions and equalities with no proofs.

claimA rung $r$ on the $phi$-ladder may be fractional. The constructors ofInt, quarter, and half produce such rungs, and toReal embeds them into the reals, satisfying quarter_eq and half_eq.

background

Recognition Science places masses on the phi-ladder via yardstick times phi to the power (rung minus 8 plus gap(Z)). The supplied doc-comment states that a rung may be fractional. NeutrinoSector places neutrinos on even integers in the -50 range of this ladder, while NeutrinoMassScaleScoreCard uses fractional placements to match NuFIT Delta m squared bands and the structural relation m_3 squared over m_2 squared equals phi to the 7.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies rung infrastructure that feeds NeutrinoSector (T14 neutrino sector derivation on the deep ladder) and NeutrinoMassScaleScoreCard (phase 2 predictions for fractional rung placement and phi^7 structure in squared splittings). It enables the hypothesis that neutrinos occupy even integers near -50 while allowing the fractional adjustments required for mass-scale comparisons.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (7)