nuYardstick
plain-language theorem explainer
The nuYardstick definition supplies the base mass scale of 0.0031 eV for the neutrino phi-ladder in the Standard Model. Modelers of neutrino hierarchies in Recognition Science cite this constant when computing absolute masses from rung assignments and oscillation data. It is introduced by direct assignment, with the value fitted once to reproduce the solar Δm²₂₁ splitting.
Claim. Let $y_ν = 0.0031$ eV denote the neutrino yardstick. Then the predicted mass at rung $r$ satisfies $m_ν(r) = y_ν · ϕ^r$, where ϕ is the golden ratio.
background
The Recognition Science mass formula places particle masses on a phi-ladder, with the mass at rung r given by yardstick times phi to the power r. For the neutrino sector, the yardstick is fixed at 0.0031 eV to match the observed solar neutrino mass-squared difference. The module examines observed mass differences, using this scale to derive absolute mass predictions consistent with cosmological upper limits on the sum of neutrino masses.
proof idea
This declaration is a one-line definition that directly sets nuYardstick to the real constant 0.0031 in electronvolt units.
why it matters
This base scale is used by the downstream definitions nuMassAtRung and theorems such as nu1_abs_mass_upper, nu2_abs_mass_pos, nu_rung_gap_ratio to establish positive masses below 12 meV and the ratio m3/m2 equal to phi^6. It realizes the phi-ladder mass formula within the neutrino hierarchy, supporting the Recognition Science prediction of small neutrino masses via the eight-tick octave and D=3 spatial dimensions. The fitting from Δm²₂₁ leaves open the question of deriving the yardstick value from the J-uniqueness or RCL without external input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.