Encyclopedia Physics Physics Neutrino Mass Scale Score Card

ARTICLE 3 claims 3 theorems

Physics Neutrino Mass Scale Score Card

A machine-checked module predicts neutrino masses from a golden-ratio ladder and certifies the predictions fall inside the measured ranges.

The neutrino score card

Neutrinos are the lightest known particles of matter, and their masses are a stubborn puzzle: the Standard Model of particle physics does not predict them. Experiments measure differences between the squares of the masses, not the masses themselves, and the three known neutrinos have masses that are tiny but not zero. The puzzle is why those masses take the values they do, and whether any underlying pattern connects them.

Recognition Science (RS) proposes an answer. The framework treats reality as maintaining a discrete record of recognition events, and from that starting point derives a chain of results including a golden-ratio scaling law. The neutrino module applies that law to the three neutrino mass states, placing them on a fractional rung ladder. The rungs are not arbitrary: the ratio of the squared masses of the third and second states is exactly the golden ratio raised to the seventh power, phi^7, a structural equality that the module proves.

The module then checks its predictions against the best available measurements. It proves, in a machine-checked library of formal theorems, that the predicted mass for each of the three neutrino states falls inside a narrow band in electron-volts: the third state between 0.04985 and 0.04993 eV, the second between 0.00924 and 0.00928 eV, and the first between 0.00352 and 0.00355 eV. It also proves that the predicted squared-mass splittings, the differences that experiments actually measure, fall inside the 1-sigma and 2-sigma windows reported by the NuFIT collaboration: the 21 splitting between 7.21e-5 and 7.62e-5 eV^2, and the 31 splitting between 2.455e-3 and 2.567e-3 eV^2.

These are not loose agreements. The bands are tight, and the structural phi^7 equality is exact, not approximate. The module packages all of this into a single certificate, a formal object that bundles the six proved bounds and the equality into one checkable unit. The certificate is a claim about what the theory predicts, not a measurement itself; the measured values come from the external NuFIT data.

The score card's value is that it turns a vague hope about neutrino masses into a precise, falsifiable statement. If a future NuFIT or PDG update places either squared splitting outside the proved windows, the certificate fails, and the theory is wrong. That is the kind of sharp edge a good physical theory needs.

THEOREM row_sqmass_ratio_phi7 · IndisputableMonolith/Physics/NeutrinoMassScaleScoreCard.lean
theorem row_sqmass_ratio_phi7 :
    (Real.goldenRatio ^ (toReal res_nu3)) ^ (2 : ℕ) /
        (Real.goldenRatio ^ (toReal res_nu2)) ^ (2 : ℕ)
      = Real.goldenRatio ^ (7 : ℝ) := squared_mass_ratio_structural_phi7
THEOREM row_nu3_frac · row_nu2_frac · row_nu1_frac · IndisputableMonolith/Physics/NeutrinoMassScaleScoreCard.lean
theorem row_nu3_frac :
    (0.04985 : ℝ) < predicted_mass_eV_frac res_nu3 ∧
      predicted_mass_eV_frac res_nu3 < (0.04993 : ℝ) := nu3_frac_pred_bounds
theorem row_nu2_frac :
    (0.00924 : ℝ) < predicted_mass_eV_frac res_nu2 ∧
      predicted_mass_eV_frac res_nu2 < (0.00928 : ℝ) := nu2_frac_pred_bounds
theorem row_nu1_frac :
    (0.00352 : ℝ) < predicted_mass_eV_frac res_nu1 ∧
      predicted_mass_eV_frac res_nu1 < (0.00355 : ℝ) := nu1_frac_pred_bounds
THEOREM row_dm2_21_nufit · row_dm2_31_nufit · IndisputableMonolith/Physics/NeutrinoMassScaleScoreCard.lean
theorem row_dm2_21_nufit :
    (7.21e-5 : ℝ) < dm2_21_frac_pred ∧ dm2_21_frac_pred < (7.62e-5 : ℝ) :=
  dm2_21_frac_pred_in_nufit_1sigma
theorem row_dm2_31_nufit :
    (2.455e-3 : ℝ) < dm2_31_frac_pred ∧ dm2_31_frac_pred < (2.567e-3 : ℝ) :=
  dm2_31_frac_pred_in_nufit_2sigma

What this page does not claim

The module does not derive the absolute electron-volt values from the framework alone; it uses a reporting seam for the unit conversion. The NuFIT windows are external measured data, not derived by the framework. The score card does not prove that the golden-ratio ladder is the unique explanation for the neutrino masses.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/NeutrinoMassScaleScoreCard.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND