nu_spacing
plain-language theorem explainer
nu_spacing fixes the rung difference for the solar-to-atmospheric neutrino gap at 7/2 on the phi-ladder. Modelers of neutrino mass hierarchies cite this when computing the squared-mass ratio from the Recognition Science eight-tick structure. The definition is a direct arithmetic assignment of the rational value.
Claim. The neutrino rung spacing is the rational number $7/2$.
background
Rung is an abbreviation for the rationals ℚ and denotes (possibly fractional) positions on the φ-ladder. The NeutrinoSector module places neutrinos on the deep ladder with even integer rungs near -50, specifically m3 near -54 and m2 near -58. This spacing supplies the 7/2 difference that relates the two scales under the quarter-ladder interpretation of the eight-tick cycle.
proof idea
It is a one-line definition that evaluates the arithmetic expression ((8 : ℚ) - 1) / 2.
why it matters
The definition is required by the lemma nu_spacing_eq that verifies the value 7/2 and by res_nu2 that defines the solar rung as the atmospheric rung minus this spacing. It realizes the fixed offset inside the eight-tick octave (T7) of the forcing chain. The module connects this spacing to the observed Δm² scales through the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.