Physics Neutrino Sector

The neutrino mass scale

Neutrinos are elementary particles that interact only through the weak force, which makes them extraordinarily difficult to detect. They come in three flavors, and experiments show they can oscillate between flavors, which requires that they have mass. The mass differences are tiny: the largest splitting, called the atmospheric scale, is about 0.05 electronvolts, and the smaller solar scale is about 0.009 electronvolts. These numbers are far below the electron mass of 511,000 electronvolts, and explaining why they are so small is an open problem in particle physics.

Recognition Science approaches the problem through its ledger, a discrete record of recognition events that the framework uses to derive physical structure. In this account, each particle family sits on a rung of a ladder, where the rung number determines the mass through a power of the golden ratio φ ≈ 1.618. The electron sits at rung 2, and the framework's hypothesis is that neutrinos occupy even rungs far below that, in the negative 50s. Specifically, the framework assigns the atmospheric neutrino to rung −54 and the solar neutrino to rung −58. The predicted masses are m₃ ≈ 0.056 eV and m₂ ≈ 0.0082 eV, which compare with the observed values of about 0.050 eV and 0.0086 eV.

The framework formalizes this comparison in a machine-checked library of formal theorems. It defines the rung assignments, computes the predicted masses, and proves that those predictions fall within the experimentally accepted ranges. The theorem neutrino_mass_verified certifies that both mass predictions match the measured values within their uncertainties. It also proves that the spacing between the neutrino rungs follows a regular pattern: the gap between the atmospheric and solar rungs is 7/2, and the gap to the lightest neutrino is 2. This quarter-ladder structure suggests a period of four rungs between generations.

The framework is honest about one important limitation. The masses are reported in electronvolts only after a display convention that treats the electron's structural mass as if it were measured in MeV and then converts with a factor of 10⁶. This is a calibration seam, not a parameter-free derivation of absolute eV scales. The framework's own native units would require a separate calibration pathway. What the framework does establish is that the neutrino mass ratios, not their absolute values, follow the golden-ratio ladder with no free parameters fitted to the neutrino data.

This matters because it turns a puzzling hierarchy into a structural prediction. If the neutrino masses are just two more rungs on the same ladder that produces the electron, then the vast gap between them is not an accident but a consequence of the framework's forcing chain. The agreement within the experimental windows is a check on that chain, and the framework's theorems make the check precise.

def rung_nu3 : ℤ := -54

def rung_nu2 : ℤ := -58

theorem neutrino_mass_verified : NeutrinoMassCert where
  m3_match := nu3_match
  m2_match := nu2_match

/-- The upgraded rung gap is exactly \(7/2\), hence the squared-mass ratio is \(φ^7\) in the pure law. -/
theorem rung_gap_is_seven_halves : res_nu3 - res_nu2 = (7 : ℚ) / 2 := by
  unfold res_nu2
  simp [nu_spacing_eq]

theorem rung_gap_21_is_two : res_nu2 - res_nu1 = (2 : ℚ) := by
  unfold res_nu1
  simp [nu1_spacing_eq]

What this page does not claim

This does not claim that the absolute neutrino masses in eV are derived without any calibration. This does not claim that the neutrino mass ordering (normal versus inverted) is determined by the framework. This does not claim that the framework explains why neutrinos are so much lighter than the electron.

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/NeutrinoSector.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: