GenClass
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign specific particles to each generation class.
- Does not define or derive the torsion offsets 0, 11, 17.
- Does not state any theorems or equalities about the classes.
- Does not reference the J-function or recognition composition law.
formal statement (Lean)
19inductive GenClass | g1 | g2 | g3
20deriving DecidableEq, Repr
21