NeutrinoMassScaleScoreCardCert
plain-language theorem explainer
The NeutrinoMassScaleScoreCardCert structure assembles six numerical certificates for the RS neutrino model: three fractional mass predictions in eV, two squared-mass splittings inside NuFIT windows, and the exact equality (m3/m2)^2 = phi^7. A neutrino phenomenologist would cite it when checking consistency between the phi-ladder rung assignments and current oscillation data. The definition packages the imported predictions from NeutrinoSector by direct transcription of the bounds and the algebraic identity.
Claim. Let $m_i$ be the predicted neutrino mass in eV obtained from the fractional-rung model on rung $r_i$. The certificate asserts $0.04985 < m_3 < 0.04993$, $0.00924 < m_2 < 0.00928$, $0.00352 < m_1 < 0.00355$, $7.21×10^{-5} < Δm^2_{21} < 7.62×10^{-5}$, $2.455×10^{-3} < Δm^2_{31} < 2.567×10^{-3}$, and $(m_3/m_2)^2 = φ^7$, where the masses come from predicted_mass_eV_frac and the splittings from the dm2 function applied to those masses.
background
In the Recognition Science framework the neutrino sector is modeled by placing the three mass eigenstates on the phi-ladder at rungs fixed by the eight-tick octave. The definitions res_nu3, res_nu2 and res_nu1 enforce the spacing res_nu3 - res_nu2 = 7/2 so that the squared-mass ratio equals phi^7 exactly. The function predicted_mass_eV_frac converts a rung into an eV-scale mass using the legacy calibration, while dm2_21_frac_pred and dm2_31_frac_pred compute the squared splittings from those masses. The module places these predictions inside the NuFIT 1-sigma windows for the solar and atmospheric mass-squared differences.
proof idea
The structure is defined by direct transcription of the six inequalities and the algebraic identity. Each field pulls the corresponding value from the imported NeutrinoSector definitions (predicted_mass_eV_frac, dm2_21_frac_pred, dm2_31_frac_pred) and compares it against the stated numerical interval; the final field rewrites the squared ratio using toReal on the rungs and the goldenRatio constant.
why it matters
This certificate supplies the concrete numerical content for the P2-ν phase of the Recognition Science program. It is consumed by the theorem neutrinoMassScaleScoreCardCert_holds, which establishes that the structure is inhabited. The phi^7 equality follows from the rung spacing together with the self-similar fixed-point property of phi. The bounds close the loop between the structural mass formula and current experimental windows on Δm².
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.