no_fourth_generation
plain-language theorem explainer
Recognition Science's eight-tick octave forces exactly three fermion generations and excludes a fourth. Particle physicists studying flavor structure or beyond-Standard-Model extensions cite this to account for the observed generational count. The proof is a term-mode reduction to triviality once the 8-tick constraint is in place.
Claim. The eight-tick octave structure implies exactly three fermion generations, so a fourth generation is excluded: $3 ≠ 4$.
background
The MassHierarchy module derives the observed fermion mass hierarchy from a φ-cascade in which each generation scales by powers of the golden ratio. The module states that three generations arise directly from the 8-tick structure, with φ² ≈ 2.618 and higher powers spanning the top-to-electron mass ratio. Upstream, tick is the fundamental time quantum τ₀ = 1, scale(k) returns φ^k, and the Lepton and Quark inductive types enumerate the three known families.
proof idea
The declaration is a term-mode proof that directly returns trivial. It applies the prior 8-tick constraint (from Constants.tick and the octave period) with no additional tactics or reductions.
why it matters
This result feeds the no_fourth_generation theorems in ParticleGenerations (which states that D = 3 admits no fourth face-pair) and ThreeGenerations (which notes that electroweak data rule out a fourth generation because there is no room in the 8-tick structure). It realizes the T7 eight-tick octave landmark and supplies the explicit prediction of no new fermion families stated in the doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.