module module moderate

`IndisputableMonolith.StandardModel.NeutrinoMassHierarchy`

Module collecting RS-native neutrino mass hierarchy quantities: solar and atmospheric mass-squared splittings, a cosmological sum bound, and a seesaw construction that ties a light neutrino mass to Dirac and Majorana scales. It links the seesaw heavy scale to explicit powers of the golden ratio (notably φ^7 and φ^13). Physicists matching oscillation data to the phi-ladder would cite it. Content is mostly definitions plus short algebraic lemmas on φ-powers.

claimCollects neutrino hierarchy data $\Delta m_{21}^2$, $\Delta m_{31}^2$, a sum-of-masses bound, and the seesaw map $m_\nu \sim m_D^2/M_R$, with typical Dirac and Majorana scales and mass ratios expressed via powers of $\varphi=(1+\sqrt{5})/2$ (including $\varphi^7$ and $\varphi^{13}$).

background

Recognition Science places particle masses on a $\varphi$-ladder (yardstick times $\varphi$ to a rung offset). Neutrinos are the lightest charged-lepton partners; their tiny masses are usually explained by a type-I seesaw: a Dirac mass $m_D$ suppressed by a heavy Majorana scale $M_R$, giving $m_\nu \approx m_D^2/M_R$.

This module sits in the StandardModel domain and imports RS constants together with rigorous interval bounds on $\varphi$. Sibling definitions name the solar and atmospheric squared-mass differences, a sum bound, typical $m_D$ and $M_R$, the seesaw formula itself, and explicit $\varphi$-power auxiliaries used to connect $M_R$ to the ladder.

Upstream, Constants supplies the RS time quantum and related units; PhiBounds supplies algebraic enclosures of $\varphi$ via rational bounds on $\sqrt{5}$, so numerical claims about $\varphi^n$ can be discharged without floating-point gaps.

proof idea

Definition-heavy module: mass-squared symbols, seesawMass, typical Dirac/Majorana scales, and massRatio are introduced as defs or abbrevs. Short lemmas (seesaw_gives_small_mass, seesaw_scale_phi_connection, phi_pow7, phi_pow13) reduce inequalities or equalities by rewriting powers of $\varphi$ and applying the imported PhiBounds enclosures; Fibonacci identities appear for the $\varphi^{13}$ auxiliary. No deep tactic scripts; structure is data plus algebraic scale checks.

why it matters in Recognition Science

Gives the Standard Model sector a concrete home for neutrino hierarchy inside the RS mass formula (yardstick $\times \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). The seesaw-to-$\varphi$ link lets oscillation scales sit on the same ladder as charged fermions, consistent with T6 ($\varphi$ as self-similar fixed point) and the overall forcing chain. used_by is empty in the graph snapshot, so this module is presently a leaf library for later SM or cosmology assembly rather than an immediate parent of a named theorem. It does not yet close a paper proposition on its own; it packages the hierarchy inputs those arguments need.

scope and limits

Does not prove oscillation parameters from first principles; it packages hierarchy scales.
Does not derive the seesaw Lagrangian or PMNS matrix entries.
Does not claim a unique Majorana scale beyond the stated φ-power connection.
Does not address sterile neutrinos, CP phases, or absolute mass ordering proofs.
Does not feed named downstream theorems in the current used_by graph.

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