nu1_spacing
plain-language theorem explainer
The definition fixes the lightest neutrino rung spacing at exactly 2 on the phi-ladder by taking one quarter of the 8-tick cycle. Neutrino mass derivations in the Recognition Science framework cite this value when positioning nu1 relative to nu2 on the deep ladder. It is introduced as a direct rational assignment drawn from the eight-tick octave structure.
Claim. The canonical spacing for the lightest neutrino rung is defined as $8/4 = 2$ on the $phi$-ladder, where a rung denotes a (possibly fractional) position in the self-similar mass scale.
background
The Neutrino Sector module places neutrinos on the deep ladder at even integer rungs near -50 to -58, with mass 3 at rung -54 and mass 2 at rung -58. The rung type is the abbreviation for rational numbers that embeds integer positions into the phi-ladder. This spacing implements the quarter-ladder hypothesis stated in the module, where the residue difference of 4 between generations aligns with a period of 4 rungs inside the 8-tick cycle.
proof idea
This is a direct definition that assigns the rational constant 8/4 to the Rung type. No lemmas or tactics are applied beyond the literal value.
why it matters
The definition supplies the subtraction term used by res_nu1 and the equality lemmas that follow, including rung_gap_is_seven_halves. It realizes the quarter-ladder structure inside the T14 neutrino sector derivation and is consistent with the eight-tick octave (T7) of the unified forcing chain. The module notes that absolute eV reporting remains a calibration seam rather than a parameter-free result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.