NeutrinoMassCert
plain-language theorem explainer
The NeutrinoMassCert structure certifies that the phi-ladder mass predictions at rungs -54 and -58 reproduce the observed atmospheric and solar neutrino scales to within 0.01 eV and 0.001 eV. Physicists verifying the deep-ladder assignments in the Recognition Science neutrino sector cite this certificate when checking consistency with experimental Delta m squared values. It is introduced as a plain structure definition that directly assembles the two absolute-difference inequalities under the legacy calibration.
Claim. The certificate holds when $|predicted(mass at rung -54) - sqrt(Delta m^2_{32})| < 0.01$ and $|predicted(mass at rung -58) - sqrt(Delta m^2_{21})| < 0.001$, where the predicted mass at a given rung is the structural mass scaled by phi to that rung power and converted to eV via the legacy display convention.
background
In the Neutrino Sector module neutrinos occupy the deep phi-ladder at even negative integer rungs far below the electron rung of 2. The constants rung_nu3 = -54 and rung_nu2 = -58 label the atmospheric (m3) and solar (m2) scales. Approximate masses are obtained as m3_approx = sqrt(dm2_32_exp) and m2_approx = sqrt(dm2_21_exp), assuming the lightest neutrino mass is negligible. The function predicted_mass_eV applies the phi-ladder mass formula with the legacy calibration that treats the electron structural mass as if measured in MeV before multiplying by 10^6 to reach eV units.
proof idea
This is a structure definition whose two fields are the match inequalities. The fields directly invoke the rung constants rung_nu3 and rung_nu2, the approximation definitions m3_approx and m2_approx, and the prediction function predicted_mass_eV. No lemmas or tactics are applied; the structure simply records the two absolute-value bounds.
why it matters
The certificate supplies the concrete verification step for T14 in the neutrino sector. It is consumed by the theorem neutrino_mass_verified and by the abstract NeutrinoMassCert structure in NeutrinoMassFromPhiLadder, which encodes normal ordering and exact phi ratios. Within the Recognition Science framework it instantiates the mass formula yardstick times phi to the power (rung minus 8) for Z=0 particles at deep negative rungs, consistent with the eight-tick octave. It leaves open the question of replacing the legacy calibration seam with a fully RS-native eV reporting path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.