neutrino_mass_verified
plain-language theorem explainer
The neutrino mass certificate packages verified numerical matches of the atmospheric scale to the phi-ladder rung at -54 and the solar scale to rung -58. Researchers comparing RS-native mass predictions to oscillation data would cite this result when checking tolerance against Delta m squared measurements. The proof is a term-mode record construction that directly inserts the pre-established bounds from nu3_match and nu2_match into the NeutrinoMassCert structure.
Claim. Let $m_3^pred$ be the predicted neutrino mass in eV at rung $-54$ on the phi-ladder and $m_3^approx$ the approximate atmospheric mass; then $|m_3^pred - m_3^approx| < 0.01$. Similarly, for rung $-58$ and the solar mass, $|m_2^pred - m_2^approx| < 0.001$.
background
In the Recognition Science setting the neutrino sector occupies the deep phi-ladder at even integer rungs far below the electron rung at 2. The local NeutrinoMassCert structure collects two tolerance checks: the atmospheric mass at rung -54 (approximately 0.056 eV versus observed 0.050 eV) and the solar mass at rung -58 (approximately 0.0082 eV versus 0.0086 eV). These checks reuse the structural mass scale from the electron sector, converted via the MeV-to-eV display convention stated in the module documentation.
proof idea
The proof constructs the NeutrinoMassCert record in term mode. It supplies the m3_match field with the theorem nu3_match (which reduces the absolute-difference bound to interval arithmetic on predicted and approximate values) and the m2_match field with nu2_match (which performs the analogous reduction for the solar scale).
why it matters
This declaration completes the T14 neutrino-sector formalization by certifying the deep-ladder assignments against experimental scales. It rests on the phi-ladder mass formula and the rung spacing of 4 that is consistent with the eight-tick octave. The result supplies a concrete numerical anchor for the broader claim that fermion masses arise from the same self-similar fixed point without extra parameters. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.