neutrinoMassScaleScoreCardCert_holds
plain-language theorem explainer
The declaration shows that the NeutrinoMassScaleScoreCardCert structure is inhabited by exhibiting explicit bounds on the fractional eV masses of the three neutrino eigenstates together with NuFIT-compatible squared mass splittings and the structural phi^7 ratio. Neutrino modelers working inside the Recognition Science phi-ladder would cite it to confirm consistency between predicted rung placements and oscillation data. The proof is a direct term-mode record construction that assembles the certificate from the six sibling row theorems.
Claim. The structure NeutrinoMassScaleScoreCardCert is non-empty, where it asserts the inequalities $(0.04985 : ℝ) < predicted_mass_eV_frac(res_nu3) < (0.04993 : ℝ)$, $(0.00924 : ℝ) < predicted_mass_eV_frac(res_nu2) < (0.00928 : ℝ)$, $(0.00352 : ℝ) < predicted_mass_eV_frac(res_nu1) < (0.00355 : ℝ)$, the squared-splitting windows $(7.21×10^{-5}) < dm2_21_frac_pred < (7.62×10^{-5})$ and $(2.455×10^{-3}) < dm2_31_frac_pred < (2.567×10^{-3})$, and the structural equality $m_3^2/m_2^2 = φ^7$.
background
In the Recognition Science neutrino sector the module packages a scorecard for mass scales on the phi-ladder. The function predicted_mass_eV_frac converts each resonance (res_nu1, res_nu2, res_nu3) into an eV-scale mass via the structural formula yardstick × φ^(rung-8 + gap(Z)). The derived quantities dm2_21_frac_pred and dm2_31_frac_pred are the squared mass differences required to lie inside NuFIT windows, while row_sqmass_ratio_phi7 enforces the rung-difference relation m_3^2/m_2^2 = φ^7 for the res_nu3 - res_nu2 = 7/2 model.
proof idea
The proof is a term-mode construction that directly builds an element of NeutrinoMassScaleScoreCardCert by substituting the six row theorems into the record fields: row_nu3_frac for nu3_frac, row_nu2_frac for nu2_frac, row_nu1_frac for nu1_frac, row_dm2_21_nufit for dm2_21, row_dm2_31_nufit for dm2_31, and row_sqmass_ratio_phi7 for sq_ratio_phi7.
why it matters
This theorem packages the neutrino mass bounds and the φ^7 structural ratio into a single certificate, completing the Phase 2 P2-ν scorecard described in the module documentation. It supplies the re-exported bounds and equality needed for consistency checks against NuFIT data while remaining tied to the phi-ladder mass formula and the eight-tick octave periodicity through the rung assignments. The result touches the Recognition Science mass formula but leaves absolute eV calibration dependent on the yardstick imported from NeutrinoSector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.