nu_phase_offset
plain-language theorem explainer
The definition assigns the neutrino phase offset the rational value -2/8 on the phi-ladder rung scale. Neutrino mass derivations in the Recognition framework cite it to enforce the quarter-rung shift between atmospheric and solar scales. It is a direct constant assignment to the Rung type with no further computation.
Claim. The neutrino phase offset is the rational number $ -2/8 $.
background
The NeutrinoSector module places neutrinos on the deep phi-ladder at even integer rungs near -50 to -60, with mass 3 at rung -54 and mass 2 at rung -58. The Rung type is defined as the rationals to permit fractional offsets that capture the observed 4-rung residue spacing between generations. Upstream, the Rung abbreviation from Support.RungFractions simply embeds integers into rationals, while gap functions from AnchorPolicy and RSBridge supply the logarithmic residue map used for charged-lepton anchors.
proof idea
Direct definition that coerces the integer 2 into rationals and divides by 8. No lemmas or tactics are invoked beyond the type ascription to Rung.
why it matters
This supplies the fixed -1/4 rung offset consumed by res_nu3, which upgrades the integer atmospheric rung to the full quarter-ladder position. It realizes the module's interpretation of the 4-rung spacing as a quarter-octave structure, consistent with the eight-tick octave (T7) and the phi-ladder mass formula. The definition closes one seam in the T14 neutrino sector derivation before the display calibration to eV units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.