nu3_match
plain-language theorem explainer
Recognition Science assigns the atmospheric neutrino mass scale to the -54 rung on the phi-ladder, and this theorem verifies that the resulting prediction lies within 0.01 eV of the experimental value obtained from the square root of dm2_32. Researchers checking the deep-ladder neutrino spectrum would cite the bound to support the rung choice. The proof combines explicit interval lemmas for the predicted and approximate masses with a linear-arithmetic discharge of the absolute-difference inequality.
Claim. $|predicted_mass_eV(-54) - sqrt(Delta m_{32}^2)| < 0.01$, where the left-hand term is the structural mass multiplied by $phi^{-54}$ and scaled to eV under the legacy display convention.
background
The NeutrinoSector module places neutrinos on the deep ladder at large negative even rungs. The structural mass is taken from the electron sector and reused with a MeV display convention before conversion by 10^6 to reach eV. The quantity m3_approx is the positive square root of the experimental atmospheric splitting dm2_32_exp, while rung_nu3 is the integer -54. The upstream lemma nu3_pred_bounds establishes the interval (0.055, 0.058) for the predicted value at this rung using structural_mass_bounds and phi power bounds; m3_approx_bounds gives the companion interval (0.049, 0.050).
proof idea
The proof obtains the interval bounds from nu3_pred_bounds and m3_approx_bounds. It rewrites the goal with abs_lt and applies linarith to the four endpoint inequalities, confirming that the largest possible absolute difference remains below 0.01.
why it matters
This result supplies the m3_match field required by the neutrino_mass_verified theorem that certifies the neutrino mass sector. It realizes the T14 claim that m3 occupies the -54 rung, consistent with the phi-ladder and the eight-tick octave from the unified forcing chain. The verification closes one link from the Recognition Composition Law to observable neutrino scales, leaving open the derivation of the exact rung spacing from J-uniqueness alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.