tau_neutrino
plain-language theorem explainer
The neutrino generation torsion function supplies the cumulative offset for neutrino species as a function of generation number. It evaluates to zero for the base case, the primary step constant for the first generation, and the sum of the primary and neutrino-specific secondary step for all higher generations. Mass spectrum calculations within Recognition Science cite this when placing neutrinos on the phi-ladder. The definition is realized through direct case analysis on the generation index.
Claim. $τ_ν : ℕ → ℤ$ is defined piecewise by $τ_ν(0) = 0$, $τ_ν(1) = s_1$, and $τ_ν(g) = s_1 + s_{2ν}$ for $g ≥ 2$, where $s_1$ is the first-generation step constant and $s_{2ν}$ is the neutrino second-generation step constant.
background
The module defines generation torsion constants drawn from simplicial ledger cube geometry. These form the cycle V+F-C=13, E_pass=11, F=6, V=8, which partition N_3=55. Neutrinos belong to the lepton sector and employ the pair {11, 6} for total torsion 17, following the legacy convention retained for leptons. Upstream results include LedgerFactorization, which calibrates the J-cost underlying discrete rung steps, and PhiForcingDerived, which supplies the recognition manifold structure for these offsets.
proof idea
The definition is realized by pattern matching on the generation argument. The zero case returns the constant 0. The singleton case returns the value of the imported first-generation step. The default case for generations two and higher returns the sum of the first-generation step and the neutrino-specific second-generation step.
why it matters
This supplies the torsion component for neutrino rungs in the legacy compute_rung function, which remains accurate for leptons. It fills the generation offset in the mass formula yardstick × φ^(rung - 8 + gap(Z)) on the phi-ladder, supporting the eight-tick octave (T7) and D=3 spatial dimensions (T8). The module documentation notes that the lepton assignment is derived from edge and face geometry while quark assignments remain hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.