dimensionToGeneration
plain-language theorem explainer
The definition supplies the explicit structural map from the three spatial dimension indices in Fin 3 to the three fermion generations, aligning the lightest family with dimension 0. Researchers tracing the origin of the three-generation structure in the Standard Model would cite it when linking the 8-tick cycle to parity patterns across orthogonal directions. The implementation is a direct exhaustive case split with no auxiliary lemmas.
Claim. Let $k$ range over the three spatial dimensions indexed by $0,1,2$. Define the generation $G(k)$ by the assignment $G(0)=$ first (lightest family), $G(1)=$ second (intermediate family), $G(2)=$ third (heaviest family). This is a fixed structural correspondence between dimension index and generational quantum number.
background
The module derives the existence of exactly three fermion generations from the Recognition Science 8-tick cycle in three-dimensional space. Generation is an inductive type whose constructors first, second, and third label the distinct parity patterns that arise when the eight phases are distributed across three orthogonal directions. Upstream, the same concept appears as the finite type Fin 3 in SpectralEmergence, confirming that the generation count matches the cube dimension.
proof idea
The definition is realized by direct pattern matching on the Fin 3 input, sending each index to the corresponding Generation constructor. No lemmas are invoked; the mapping is exhaustive by construction on the three-element domain.
why it matters
This definition supplies the concrete correspondence required by the module's core hypothesis that the 8-tick octave (T7) together with three spatial dimensions (T8) produces exactly three generations. It precedes the mass-hierarchy pattern in the same file and supports the broader claim that generational structure emerges from the simplicial ledger and forcing chain. The module is positioned as a potential PRL contribution on the first derivation of the generation number.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.