nu_phase_offset
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the base integer rungs -54 or -58.
- Does not compute absolute masses in eV without the electron-mass calibration seam.
- Does not address neutrino mixing angles or CP phases.
- Does not prove the deep-ladder hypothesis itself.
formal statement (Lean)
138def nu_phase_offset : Rung := (-(2 : ℚ)) / 8
proof body
Definition body.
139
140/-- Neutrino spacing for the solar-to-atmospheric gap: \((8-1)/2 = 7/2\) rungs. -/