res_nu3
plain-language theorem explainer
Definition of the third neutrino rung: integer base of -54 plus fixed quarter-rung phase offset of -1/4. Neutrino mass modelers in the Recognition Science framework cite this rung to obtain the atmospheric mass scale m3 approximately 0.056 eV. It is realized as a direct arithmetic combination of the base integer rung and the phase offset.
Claim. $r_3 := -54 - 1/4$, where the base integer is the deep-ladder rung for the atmospheric neutrino scale and the offset is the fixed quarter-octave phase shift.
background
The NeutrinoSector module formalizes the deep-ladder hypothesis for neutrino masses. Neutrinos occupy even integers in the -50 range, with the atmospheric scale at rung -54 yielding m3 approximately 0.056 eV and the solar scale at -58 yielding m2 approximately 0.0082 eV. The residue difference of 4 rungs suggests quarter-ladder spacing. Rung type supports fractional values; rung_nu3 supplies the integer base -54 while nu_phase_offset supplies the fixed -1/4 shift, equivalent to -2/8 of an octave.
proof idea
One-line definition that converts the integer rung_nu3 to Rung type and adds the nu_phase_offset value.
why it matters
This rung enters NeutrinoMassScaleScoreCardCert and the row_nu3_frac bound, which checks the predicted mass fraction against 0.04985 to 0.04993. It also supports dm2_31_frac_pred and the squared-mass ratio theorem that recovers phi^7 from the 7/2 rung spacing. The construction fills the T14 neutrino sector step in the Recognition Science chain, where the deep ladder and phi-ladder mass formula produce the observed atmospheric and solar scales after display calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.