nu_phase_offset_eq
plain-language theorem explainer
The lemma fixes the neutrino phase offset at negative one quarter in rational units. Researchers deriving solar and atmospheric neutrino scales on the Recognition Science phi-ladder cite it to close the quarter-rung spacing between generations. The proof is a one-line wrapper that unfolds the definition and normalizes the fraction.
Claim. The neutrino phase offset equals $ -1/4 $ in rational units, where the offset is defined as two-eighths of an octave on the negative side.
background
In the T14 neutrino sector the masses sit on the deep ladder at even negative rungs far below the electron rung. The module treats the atmospheric scale as rung -54 and the solar scale as rung -58, so the residue difference of four rungs suggests a quarter-ladder period. The upstream definition states that the neutrino phase offset is -2/8 of an octave, which is the quantity whose value is fixed here.
proof idea
The term proof unfolds the definition of nu_phase_offset and applies norm_num to reduce the fraction -2/8 directly to -1/4.
why it matters
It supplies the exact offset needed by the downstream simplification res_nu3_simp that computes the residue for the atmospheric neutrino. The result anchors the quarter-ladder structure inside the eight-tick octave of the forcing chain and closes the rung arithmetic for the neutrino mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.