nu_phase_offset_eq
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive absolute neutrino masses in SI units.
- Does not address neutrino mixing angles or oscillation probabilities.
- Does not prove the assignment of rungs -54 and -58.
- Does not extend to charged-lepton or quark sectors.
Lean usage
simp [nu_phase_offset_eq]formal statement (Lean)
143lemma nu_phase_offset_eq : nu_phase_offset = (-1 : ℚ) / 4 := by
proof body
Term-mode proof.
144 unfold nu_phase_offset
145 norm_num
146