tau_g
plain-language theorem explainer
tau_g assigns rung offsets 0, 11 and 17 to the three generations. CKM derivations in Recognition Science cite these offsets to obtain mixing angles theta_ij approximately phi to the power of minus half the rung difference. The definition is a direct case match on the Generation inductive type with no lemmas invoked.
Claim. Let $tau_g$ be the map on generations such that $tau_g(first)=0$, $tau_g(second)=11$ and $tau_g(third)=17$.
background
The CKM module treats generations as an inductive type with constructors first, second and third. Rung differences tau_g between up and down sectors produce angles theta_ij ~ phi^{-Delta tau / 2} and fix the Jarlskog invariant as a dimensionless output. Upstream, Generation appears as Fin 3 in SpectralEmergence, as a parity pattern across dimensions in ThreeGenerations, and as canonical torsion from Q3 cube geometry in RSLedger.
proof idea
The definition proceeds by exhaustive pattern matching on the three constructors of Generation, returning the literal integer in each branch. No upstream lemmas are applied; the implementation is a structural recursion on the inductive type.
why it matters
tau_g supplies the explicit rung offsets required by the geometric CKM predictions. It is invoked inside the no_sterile theorem to show that any fourth generation would break surjectivity onto Fin 3 and violate the eight-beat minimality. The values align with the T7 eight-tick octave and the three-generation structure forced by D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.