no_fourth_generation
plain-language theorem explainer
The declaration shows that the explicit list of three generations has length unequal to four. A particle physicist excluding additional fermion families in beyond-Standard-Model models would cite this when invoking the 8-tick structure. The proof reduces to a direct decision procedure on the finite list of Generation constructors.
Claim. Let $G$ be the set of generations defined by the three distinct parity patterns across three spatial dimensions in the 8-tick cycle. Then $|G| = 3$, so in particular $|G| ≠ 4$.
background
Recognition Science obtains the fermion family count from the 8-tick octave (period $2^3$) combined with three spatial dimensions. Each generation is a discrete label arising from the parity pattern of the fundamental tick across the three orthogonal directions, producing exactly the modes first, second, and third. The module documentation states the hypothesis that 8 = 2³ and 3D space supplies three bit indices, so generations are the three distinct parity combinations.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the inequality on the length of the explicit list containing the three Generation constructors.
why it matters
This result supplies the concrete count of three generations that feeds the ParticleGenerations.no_fourth_generation theorem (which shows face_pairs 3 ≠ 4) and the MassHierarchy.no_fourth_generation theorem. It realizes the T7 eight-tick octave and T8 D = 3 landmarks by demonstrating that the three orthogonal directions admit no fourth parity pattern. The module documentation positions the statement as the derivation of generation number from RS structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.