module module high

`IndisputableMonolith.Physics.NeutrinoSector`

The NeutrinoSector module supplies experimental mass-squared differences Δm²_{21} and Δm²_{32} in eV² together with approximate masses and phi-ladder rung assignments for the neutrino sector. Researchers calibrating Recognition Science mass predictions against NuFIT data cite it when scoring the fractional ladder model. The module consists entirely of definitions and external anchors drawn from the imported constants and electron-mass results.

claim$Δm^2_{21}$, $Δm^2_{32}$ (in eV²), $m_2$, $m_3$ (approximate), rung_nu3, rung_nu2 on the phi-ladder, with calibration functions predicted_mass_eV and mass_display_calibration_of_external.

background

The module operates inside the Recognition Science native unit system (c = 1, ħ = φ^{-5}) defined in Constants.RSNativeUnits and draws empirical anchors exclusively from ExternalAnchors. It imports the T9 electron-mass derivation and its necessity proof from ElectronMass and ElectronMass.Necessity, together with rigorous φ bounds and rung-fraction support. The local setting is the extension of the ledger-fraction mass formula yardstick · φ^(rung-8+gap(Z)) to the neutrino sector after the eight-tick octave and D = 3 have been fixed.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds NeutrinoMassScaleScoreCard, which tests the structural claim m_3²/m_2² = φ^7 inside the res_nu3 - res_nu2 = 7/2 model, and ParticleSummary, which assembles all Standard-Model parameters derived from Recognition Science. It supplies the single quarantined location for neutrino Δm² data required by the phase-2 neutrino-mass program.

scope and limits

Does not derive neutrino masses from the Recognition Composition Law.
Does not prove any mass-squared value; all entries are external anchors.
Does not address neutrino mixing angles or CP phases.
Does not treat sterile neutrinos or non-standard interactions.

used by (2)

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

IndisputableMonolith.Physics.NeutrinoMassScaleScoreCard module_import
IndisputableMonolith.Physics.ParticleSummary 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