Generation
plain-language theorem explainer
Generation enumerates three fermion families via distinct parity patterns of the 8-tick phases distributed over three spatial dimensions. A particle physicist resolving the Standard Model family replication puzzle would cite this as the Recognition Science account of exactly three generations. The declaration is a direct inductive definition with three constructors and no attached proof body.
Claim. An inductive type with three constructors: first for parity pattern (0,0,*) or (1,1,*), second for (0,1,*) or (1,0,*), and third for special cases.
background
The module Physics.ThreeGenerations sets out to derive exactly three generations of fermions from the Recognition Science structure of an 8-tick cycle crossed with three-dimensional space. The 8-tick cycle supplies eight phases indexed by three bits, each bit aligned with one spatial dimension; generations are the three distinct parity combinations across those dimensions. This construction sits inside the broader derivation of physics from a single functional equation, with the eight-tick octave and D = 3 as upstream landmarks.
proof idea
The declaration is an inductive definition. Three constructors are introduced directly, each carrying an inline comment that records the associated bit-parity pattern. No lemmas, tactics, or reductions are applied; the body is empty.
why it matters
This definition supplies the generation modes required by downstream results such as three_generations_from_dimension, which states that face pairs in D_physical equal 3, and gauge_generators_eq_edges in SpectralEmergence. It fills the SM-011 target of obtaining the generation count from the 8-tick by 3D structure and connects to the eight-tick octave (T7) and spatial dimension forcing (T8). It leaves open the concrete assignment of observed fermion masses to each mode.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.