three_generations
plain-language theorem explainer
The declaration establishes that the inductive type with three constructors for fermion generations has cardinality exactly three. Researchers closing the self-consistency argument for the Standard Model in Recognition Science would cite it to confirm that the 8-tick cycle in three dimensions forces three families. The proof is a one-line reflexivity on the explicit list of the three constructors.
Claim. The set of generations, defined via the three parity patterns across spatial dimensions, satisfies $|G| = 3$ where $G = $ {first, second, third}.
background
The module derives the number of fermion generations from the 8-tick cycle times three-dimensional space. Generation is an inductive type whose constructors first, second, and third label the distinct parity patterns across the three dimensions. Upstream results supply tick as the fundamental time quantum and the independent spatial semantics that treat voxels without neighbor coupling.
proof idea
The proof is a term-mode reflexivity that directly evaluates the length of the list containing the three explicit constructors.
why it matters
This result is invoked by framework_self_consistent to show that Recognition Science reproduces its own inputs of D=3, eight vertices, and three generations. It supports the numerological summary that Standard Model counts are cube numbers and feeds the master theorem spectral_emergence. It closes the T7 eight-tick octave and T8 D=3 steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.