pith. sign in
module module moderate

IndisputableMonolith.Physics.NeutrinoMassScaleScoreCard

show as:
view Lean formalization →

The module assembles a scorecard for neutrino masses using fractional placements on the phi-ladder in the deep ladder regime. Researchers checking Recognition Science mass predictions against oscillation data would cite the rows and certification. It consists of definition rows for each neutrino flavor fraction together with a holds statement for the overall scorecard.

claimCertification that neutrino mass ratios match rung fractions on the $\phi$-ladder for even rungs near $-50$, with explicit rows for $\nu_3$, $\nu_2$, $\nu_1$ fractions, $\Delta m^2_{21}$ and $\Delta m^2_{31}$ comparisons to NuFit values, and a square-mass ratio at $\phi^7$.

background

The module sits inside the T14 neutrino sector formalization. Neutrinos are hypothesized to occupy the deep ladder: even integer rungs far below the electron at rung 2, specifically near $-50$. The imported RungFractions module supplies a type-light representation for fractional rungs (quarter-ladder and similar) so that observed mass ratios can be expressed without forcing the core integer-rung mass model to change.

Recognition Science mass assignments follow the yardstick times $\phi$ to the power of (rung minus 8 plus gap), and the scorecard tests whether the deep-ladder neutrino placements reproduce the experimental square-mass differences. The module therefore acts as the reporting seam between the rigid integer ladder and the fractional refinements needed for neutrinos.

proof idea

This is a definition module, no proofs. It declares row definitions for the three neutrino fractions, the two NuFit square-mass rows, the $\phi^7$ ratio row, and the top-level NeutrinoMassScaleScoreCardCert object together with its holds statement.

why it matters in Recognition Science

The module supplies the concrete scorecard that validates the deep-ladder hypothesis inside T14. It therefore sits directly under the neutrino mass scale derivation and feeds any later claim that the observed masses are consistent with the phi-ladder formula. It touches the open question of whether fractional rungs are required only for neutrinos or appear elsewhere on the ladder.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)