rung_nu2
plain-language theorem explainer
Assigns the solar neutrino mass scale m2 to rung -58 on the Recognition Science phi-ladder. Researchers matching RS predictions to Delta m squared 21 oscillation data cite this assignment when verifying mass bounds. The declaration is a direct integer constant definition with no lemmas or tactics.
Claim. The solar neutrino mass scale occupies rung $R = -58$ on the phi-ladder, so that $m_2$ is obtained from the structural mass yardstick scaled by phi to the power -58 after the MeV-to-eV calibration seam.
background
In the neutrino sector module, neutrinos occupy the deep ladder with integer rungs far below the electron at rung 2. The solar scale m2 is placed at rung -58, producing a predicted mass near 0.0082 eV once the structural mass is treated as MeV and converted by the factor 10^6. Upstream, the scale function supplies phi raised to integer powers for ladder steps, while the for structure records meta-realization properties needed for self-reference coherence.
proof idea
The declaration is a direct constant definition that sets the integer value to -58. No lemmas are applied and no tactics are used; it serves as an input parameter for downstream bound lemmas such as nu2_pred_bounds.
why it matters
This rung supplies the input to the nu2_match theorem and the NeutrinoMassCert structure, which certifies that the predicted m2 lies within 0.001 eV of the observed solar splitting. It implements the T14 neutrino sector hypothesis inside the Recognition Science framework, where the phi-ladder mass formula, eight-tick octave, and D equals 3 dimensions determine the rung spacing. The assignment closes the reporting seam that reuses the electron structural mass for eV display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.