neutrino_squared_mass_ratio
plain-language theorem explainer
Recognition Science equates the neutrino squared-mass ratio m₃²/m₂² with φ⁷. This theorem proves the strict inequality 29 < φ⁷ < 30, aligning with NuFIT 5.3 data near 29.0 for normal ordering as a calibration-free output of the phi-ladder. Neutrino phenomenologists and RS model builders would cite it for its direct match to oscillation measurements. The proof is a one-line term that assembles the dedicated lower-bound lemma with the upper half of the parent interval theorem.
Claim. $29 < m_3^2 / m_2^2 < 30$ where $m_3^2 / m_2^2 = phi^7$ and $phi = (1 + sqrt(5))/2$.
background
The module supplies machine-verified bounds on every RS numerical prediction, each expressed as a formally proved inequality in Lean's type theory rather than a floating-point check. The table lists φ⁷ under the neutrino ratio entry with proved interval (28, 30) and measured value ~29.0. Upstream, phi_pow_7_bounds states (28 : ℝ) < phi ^ 7 ∧ phi ^ 7 < (30 : ℝ) and its doc-comment notes the tighter lower bound uses phi > 1.618 from PhiBounds because 13 × 1.618 + 8 = 29.034 > 29.
proof idea
The proof is a one-line term that pairs the lemma phi_pow_7_gt_29 (the strict lower bound) with the second conjunct of phi_pow_7_bounds (the upper bound).
why it matters
The result supplies the neutrino entry inside NumericalPredictionsCert, the master structure that certifies the full set of RS predictions including the alpha inverse interval (137.030, 137.039). It completes the phi^7 row of the module table and traces to the phi-ladder mass formula yardstick * phi^(rung - 8 + gap(Z)). The construction sits downstream of the forcing chain steps that fix phi as the self-similar fixed point and enforce the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.