module module high

`IndisputableMonolith.Physics.NeutrinoSector`

Defines the Recognition Science neutrino sector: experimental Δm² anchors, approximate m₂ and m₃, fractional φ-ladder rungs for ν₂ and ν₃, and eV mass display via a calibration bridge from the electron-mass yardstick. Cited by the P2-ν mass-scale scorecard and the baseline choice-set enumerator. Mostly definitions and calibrated predictions, not a forcing proof.

claimThe module packages neutrino mass-squared differences $\Delta m_{21}^2$, $\Delta m_{32}^2$ (in eV$^2$), approximate masses $m_2$, $m_3$, fractional rungs $r_{\nu_2}$, $r_{\nu_3}$ on the $\varphi$-ladder, and a mass-display calibration that converts RS rung predictions into eV via the electron-mass yardstick and MeV$\to$eV conversion.

background

Recognition Science places particle masses on a $\varphi$-ladder: mass $\sim$ yardstick $\times \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$. The electron mass (T9) supplies the structural first-break yardstick and necessity proofs that the charged-lepton formula is forced from ledger quantization. Neutrinos sit far down the same ladder, so absolute eV values need a display calibration from that yardstick plus external CODATA/empirical anchors quarantined in ExternalAnchors.

This module is the physics-side home for neutrino sector constants and predictions: NuFIT-style experimental $\Delta m^2$ numbers, rough $m_2$ and $m_3$, and the fractional rung assignments $r_{\nu_2}$, $r_{\nu_3}$. Support.RungFractions and PhiBounds supply the fractional-rung and golden-ratio interval machinery; RSNativeUnits keep the ledger primitives available when SI display is not required.

The short module header flags mass-squared differences in eV$^2$ as the primary comparison surface with oscillation data.

proof idea

Definition and calibration module, not a forcing chain. It binds experimental $\Delta m^2$ anchors, approximate masses, and rung labels; builds a MassDisplayCalibration (legacy and external-anchor variants); converts MeV to eV; and exposes predicted_mass_eV / predicted_mass_eV_with that push ladder rungs through the electron-mass yardstick into eV. Interval facts on $\varphi$ and rung-fraction support are imported rather than reproved here.

why it matters in Recognition Science

Feeds NeutrinoMassScaleScoreCard (Phase 2 P2-ν): fractional rung placement, eV mass bands, squared splittings in NuFIT windows, and the structural claim $m_3^2/m_2^2=\varphi^7$ under the residue gap $\mathrm{res}{\nu_3}-\mathrm{res}{\nu_2}=7/2$. Also imported by Verification.NeutrinoBaselineChoiceSet, which enumerates lightest-neutrino quarter-rung numerators with gap profile $+2$ then $+7/2$, a deep-atmospheric window on $r_3$, and the canonical $-1/4$ phase class.

In the broader RS map this is the neutrino counterpart of the T9 electron-mass sector: same $\varphi$-ladder and yardstick logic, specialized to oscillation $\Delta m^2$ and absolute baseline search. It does not itself close T0–T8; it supplies the sector data those scorecards and choice-set proofs consume.

scope and limits

Does not prove neutrino masses are forced from T0–T8 alone.
Does not derive PMNS angles or CP phase.
Does not replace NuFIT/PDG; experimental Δm² enter as anchors.
Does not fix the absolute lightest-neutrino baseline (deferred to choice-set search).
Does not claim Dirac vs Majorana nature or sterile states.

used by (2)

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

IndisputableMonolith.Physics.NeutrinoMassScaleScoreCard module_import
IndisputableMonolith.Verification.NeutrinoBaselineChoiceSet module_import

depends on (7)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.ExternalAnchors module_import
IndisputableMonolith.Constants.RSNativeUnits module_import
IndisputableMonolith.Numerics.Interval.PhiBounds module_import
IndisputableMonolith.Physics.ElectronMass module_import
IndisputableMonolith.Physics.ElectronMass.Necessity module_import
IndisputableMonolith.Support.RungFractions module_import

declarations in this module (53)

def dm2_21_exp L57
def dm2_32_exp L58
def m2_approx L61
def m3_approx L62
def rung_nu3 L66
def rung_nu2 L67
structure MassDisplayCalibration L70
def legacy_mass_display_calibration L75
def mass_display_calibration_of_external L81
def MeV_to_eV L91
def predicted_mass_eV_with L94
def predicted_mass_eV L99
lemma predicted_mass_eV_legacy L102
def nu_phase_offset L138
def nu_spacing L141
lemma nu_phase_offset_eq L143
lemma nu_spacing_eq L147
def res_nu3 L152
def res_nu2 L155
def nu1_spacing L158
lemma nu1_spacing_eq L160
def res_nu1 L165
lemma res_nu3_simp L167
lemma res_nu2_simp L173
lemma res_nu1_simp L179
theorem rung_gap_21_is_two L185
def predicted_mass_eV_frac_with L190
def predicted_mass_eV_frac L195
lemma predicted_mass_eV_frac_legacy L198
theorem rung_gap_is_seven_halves L205
lemma nu3_frac_pred_bounds L224
lemma nu2_frac_pred_bounds L256
lemma nu1_frac_pred_bounds L284
def dm2 L392
def dm2_21_frac_pred L394
def dm2_31_frac_pred L397
def dm2_21_frac_pred_with L401
def dm2_31_frac_pred_with L405
lemma dm2_21_frac_pred_with_legacy L408
lemma dm2_31_frac_pred_with_legacy L412
lemma dm2_21_frac_pred_in_nufit_1sigma L417
lemma dm2_21_frac_pred_with_legacy_in_nufit_1sigma L486
lemma dm2_31_frac_pred_in_nufit_2sigma L492
lemma dm2_31_frac_pred_with_legacy_in_nufit_2sigma L556
theorem squared_mass_ratio_structural_phi7 L572
lemma nu3_pred_bounds L623
lemma m3_approx_bounds L651
theorem nu3_match L674
lemma nu2_pred_bounds L689
lemma m2_approx_bounds L717
theorem nu2_match L738
structure NeutrinoMassCert L748
theorem neutrino_mass_verified L752