Standard Model Neutrino Mass Hierarchy

The neutrino mass ordering

Neutrinos are elementary particles that rarely interact with matter. They come in three types, or flavors: electron, muon, and tau. Quantum mechanics says these flavors mix, and the three mass states that mix are called ν₁, ν₂, and ν₃. The mass hierarchy is the question of which state is lightest and which is heaviest. In the normal hierarchy, ν₁ is lightest, then ν₂, then ν₃. In the inverted hierarchy, ν₃ is lightest. Experiments have measured the differences between the squared masses: the solar gap, Δm²₂₁, is about 7.42 × 10⁻⁵ eV², and the atmospheric gap, Δm²₃₁, is about 2.51 × 10⁻³ eV². These numbers come from oscillations, where neutrinos change flavor as they travel. The absolute masses, however, are not known, only the differences.

The ordering matters for physics beyond the Standard Model. It affects how neutrinos could have gotten their tiny masses, which are at least a million times smaller than the electron's. The leading explanation is the seesaw mechanism, proposed in the late 1970s by Peter Minkowski and others. It posits a very heavy right-handed neutrino, with a mass around 10¹⁴ GeV. The light neutrino mass then equals the square of a typical Dirac mass, around 100 GeV, divided by that heavy mass. With those numbers, the light mass comes out to 10⁻¹⁰ GeV, or about 0.1 eV. The seesaw naturally produces small masses, but it does not by itself say which state is lightest.

In Recognition Science, the framework models particle masses as sitting on a ladder of powers of the golden ratio, φ ≈ 1.618. The framework's library, a machine-checked collection of formal theorems, assigns each neutrino a rung on this ladder. The lightest, ν₁, sits at rung -28; ν₂ at rung -26; and ν₃ at rung -20. The gaps between these rungs match the measured solar and atmospheric splittings: a 2-rung gap for the solar difference and an 8-rung gap for the atmospheric difference. The framework's prediction is the normal hierarchy, with ν₁ lightest. This is a definitional choice, a model, not a derived theorem.

What the module proves is internal consistency. It shows that the predicted masses are positive, that each is below 0.012 eV, and that their sum is below the cosmological bound of 0.12 eV. It proves the rung ratios exactly: the ratio of ν₃ to ν₂ is φ⁶, and the ratio of ν₂ to ν₁ is φ². These are theorems in the machine-checked library. The comparison to measured mass differences is an empirical check, not a theorem. The framework does not prove the normal hierarchy is the real one; it asserts it as a model and checks that the model is internally coherent.

The practical upshot is a concrete target for experiments. If the framework's model is right, the sum of neutrino masses is about 0.0031 eV, well below current limits. Next-generation experiments like JUNO and Hyper-Kamiokande aim to determine the ordering by 2030. The framework's prediction is falsifiable: if experiments find the inverted hierarchy, the model fails. The module does not claim to have settled the question; it offers a structured guess, with the mathematics checked and the physics left to measurement.

def rsPrediction : MassOrdering := MassOrdering.Normal

/-- RS neutrino rung assignments.

    The neutrino masses sit on the φ-ladder shifted by the seesaw offset from
    the Majorana scale. The φ-ladder yardstick is m₀ = φ⁻⁵ in RS-native units.

    Normal hierarchy assignment (consistent with oscillation data):
    - ν₁: rung -28 (lightest, m₁ < 0.01 eV)
    - ν₂: rung -26 (solar splitting: Δm²₂₁ ~ φ⁻⁵² eV²)
    - ν₃: rung -20 (atmospheric splitting: Δm²₃₁ ~ φ⁻⁴⁰ eV²)

    The gap between ν₂ and ν₃ is 6 rungs = Δ ln(m) ≈ 6 ln φ ≈ 2.87,
    giving m₃/m₂ ≈ e^2.87 ≈ 17.6. From oscillation data: √(Δm²₃₁)/√(Δm²₂₁)
    ≈ 50.1/8.62 ≈ 5.81 meV ratio, consistent with rung-4 gap (φ⁴ ≈ 6.85). -/
structure NuRungAssignments where
  rung_nu1 : ℤ  -- ν₁ rung (most negative = lightest)
  rung_nu2 : ℤ  -- ν₂ rung
  rung_nu3 : ℤ  -- ν₃ rung
  /-- Normal hierarchy: ν₁ is lightest -/
  normal_hierarchy : rung_nu1 < rung_nu2 ∧ rung_nu2 < rung_nu3
  /-- Solar splitting corresponds to 2-rung gap -/
  solar_gap : rung_nu2 - rung_nu1 = 2
  /-- Atmospheric splitting corresponds to 6-rung gap -/
  atm_gap : rung_nu3 - rung_nu1 = 8

/-- The rung-gap ratio m₃/m₂ = φ⁶ is close to the observed oscillation ratio. -/
theorem nu_rung_gap_ratio :
    m_nu3_pred / m_nu2_pred = phi ^ (6 : ℤ) := by
  unfold m_nu3_pred m_nu2_pred nuMassAtRung
  have hphi_ne : phi ≠ 0 := ne_of_gt phi_pos
  have hys_ne : (nuYardstick : ℝ) ≠ 0 := by unfold nuYardstick; norm_num
  have hden_ne : nuYardstick * phi ^ (-26 : ℤ) ≠ 0 :=
    ne_of_gt (mul_pos (by unfold nuYardstick; norm_num) (zpow_pos phi_pos _))
  field_simp [hden_ne, hys_ne]

/-- ν₂/ν₁ mass ratio = φ² (2-rung gap). -/
theorem nu_solar_rung_ratio :
    m_nu2_pred / m_nu1_pred = phi ^ (2 : ℤ) := by
  unfold m_nu2_pred m_nu1_pred nuMassAtRung
  have hphi_ne : phi ≠ 0 := ne_of_gt phi_pos
  have hys_ne : (nuYardstick : ℝ) ≠ 0 := by unfold nuYardstick; norm_num
  have hden_ne : nuYardstick * phi ^ (-28 : ℤ) ≠ 0 :=
    ne_of_gt (mul_pos (by unfold nuYardstick; norm_num) (zpow_pos phi_pos _))
  field_simp [hden_ne, hys_ne]

def nuAbsMassCert : NuAbsMassCert := {
  nu1_upper := nu1_abs_mass_upper
  nu2_upper := nu2_abs_mass_upper
  nu2_pos   := nu2_abs_mass_pos
  nu3_positive := nu3_abs_mass_positive
  sum_bound := nu_sum_bound_consistent
  rung_gap_ratio := nu_rung_gap_ratio
  solar_gap_ratio := nu_solar_rung_ratio
}

What this page does not claim

The normal hierarchy is not proved; it is a model choice. The absolute neutrino masses are not measured, only predicted by the model. The seesaw mechanism is not derived by the framework; it is a standard physics input.

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/StandardModel/NeutrinoMassHierarchy.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: