tau
plain-language theorem explainer
The generation torsion function assigns integer offsets to fermion families for use in phi-ladder mass formulas: zero at the base, eleven at the first generation, and seventeen for all higher generations. Mass and complexity modelers cite it when fixing rung indices for leptons and quarks. The definition is a direct case split on the natural-number input that pulls the passive-edge and wallpaper-group constants from sibling abbreviations.
Claim. Define the function $τ:ℕ→ℤ$ by $τ(0)=0$, $τ(1)=11$, and $τ(n)=17$ for all $n≥2$.
background
The module assembles parameter-free constants derived from three-dimensional cube geometry. Total cube edges equal twelve, so the passive edge count E_passive is defined as twelve minus one. The wallpaper group count W is fixed at seventeen from two-dimensional symmetry considerations in the mass topology layer.
proof idea
The definition is a pattern match on the generation index. It returns the literal zero for input zero, casts the sibling E_passive abbreviation to ℤ for input one, and casts the sibling W abbreviation to ℤ for every larger index. No external lemmas are applied.
why it matters
This supplies the generation-dependent torsion term required by downstream mass formulas and by the high-depth non-naturalness theorems that bound complexity properties for τ>1. It closes the integer map from cube geometry (D=3) to the rung offsets on the phi-ladder, consistent with the eight-tick octave and the sector yardsticks listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.