module module moderate

`IndisputableMonolith.StandardModel.NeutrinoMassHierarchy`

The NeutrinoMassHierarchy module supplies definitions for neutrino mass-squared differences and seesaw scales together with an auxiliary lemma expressing phi^13 via Fibonacci numbers. Physicists constructing phi-ladder mass predictions in Recognition Science would cite these results when fitting observed Delta m^2 values. The proofs proceed by direct algebraic reduction using the Fibonacci recurrence for powers of phi combined with interval bounds imported from PhiBounds.

claimThe module defines quantities such as $Δm_{21}^2$, $Δm_{31}^2$, the seesaw mass scale, and the auxiliary identity $φ^{13} = F_{13} φ + F_{12}$ (Fibonacci numbers $F_n$).

background

This module sits inside the Standard Model sector of Recognition Science and imports the RS time quantum τ₀ = 1 tick together with rigorous algebraic bounds on φ = (1 + √5)/2. It introduces the seesaw mechanism for generating small neutrino masses and places them on the phi-ladder mass formula (yardstick × φ^(rung − 8 + gap(Z))). Upstream results supply the Recognition Composition Law and the eight-tick octave structure that fix the allowed exponents.

proof idea

The module is a collection of definitions followed by targeted lemmas. The central phi_pow13 lemma is obtained by applying the Fibonacci recurrence relation φ^n = φ^{n−1} + φ^{n−2} iteratively and confirming the resulting integer coefficients against the interval bounds on φ.

why it matters in Recognition Science

The module supplies the neutrino-sector mass relations required by the broader Standard Model construction in Recognition Science. It directly supports phi-based predictions for the mass hierarchy and connects to the mass formula and RCL through the phi^13 and phi^7 auxiliary results. No downstream theorems are listed in the current graph, but the definitions close the gap between the general phi-ladder and concrete neutrino observables.

scope and limits

Does not derive neutrino mixing angles or PMNS matrix elements.
Does not compute absolute mass eigenvalues beyond squared-difference bounds.
Does not address sterile neutrinos or non-standard interactions.
Does not extend the phi-ladder beyond the listed powers (7 and 13).

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Numerics.Interval.PhiBounds module_import

declarations in this module (38)

def deltam21_sq L15
def deltam31_sq L16
def sum_mass_bound L17
def seesawMass L21
def typicalDiracMass L22
def typicalMajoranaMass L23
theorem seesaw_gives_small_mass L25
def phiPredictedMR L32
lemma phi_pow13 L35
theorem seesaw_scale_phi_connection L50
def massRatio L78
lemma phi_pow7 L80
theorem mass_ratio_phi7 L89
def m2_estimate L111
def m3_estimate L112
def m3_m2_ratio L113
lemma phi_pow4 L115
theorem mass_ratio_phi4 L121
inductive MassOrdering L157
def rsPrediction L162
structure NuRungAssignments L179
def canonicalNuRungs L191
def nuYardstick L203
def nuMassAtRung L205
def m_nu1_pred L209
def m_nu2_pred L211
def m_nu3_pred L213
theorem nu_rung_gap_ratio L216
theorem nu_solar_rung_ratio L226
lemma zpow_neg_lt_one L236
theorem nu_sum_bound_consistent L246
theorem nu1_abs_mass_upper L283
theorem nu2_abs_mass_pos L290
theorem nu2_abs_mass_upper L295
theorem nu2_abs_mass_interval L302
theorem nu3_abs_mass_positive L307
structure NuAbsMassCert L312
def nuAbsMassCert L321