GenClass
plain-language theorem explainer
GenClass enumerates the three fermion generations via the constructors g1, g2, g3. Mass derivations cite it to select the generation label when computing rung values from word length and torsion. The declaration is a direct inductive type definition that automatically derives decidable equality and representation.
Claim. The generation class type consists of three elements denoted $g_1$, $g_2$, $g_3$.
background
The KernelTypes module supplies the basic types used to build the mass kernel. GenClass labels the three generations of fermions and is paired with a natural-number rung length ell inside the RungSpec structure. The sibling definition tauOf then maps the three classes to the integer offsets 0, 11, and 17.
proof idea
The declaration is the inductive definition of the three-element type with constructors g1, g2, g3 together with the derived DecidableEq and Repr instances. No lemmas or tactics are invoked.
why it matters
GenClass supplies the generation label required by RungSpec, tauOf, leptonRung, rungFrom, and massCanonFromWord. These functions use the label to insert the distinct torsion shifts 0, 11, 17 that separate the three families inside the canonical mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.