neutrino_generations_match
plain-language theorem explainer
The theorem asserts that the Recognition Science framework produces exactly three fermion generations, matching both neutrino and charged lepton families. A particle physicist deriving the Standard Model structure from first principles would reference this result when explaining the absence of a fourth generation. The proof reduces immediately to reflexivity on the explicit list of three Generation constructors.
Claim. The cardinality of the set of generations defined by the inductive constructors first, second, and third equals 3.
background
In the Recognition Science framework, Generation is an inductive type with three constructors corresponding to distinct parity patterns across the three spatial dimensions. These arise from indexing the 8-tick cycle phases by three bits, each tied to one dimension, as described in the module on SM-011. Upstream, SpectralEmergence.of states that exactly 3 particle generations arise from face-pair count in the Q3 structure, while the abbrev Generation := Fin 3 confirms the count matches the cube dimension.
proof idea
The proof is a term-mode reflexivity (rfl) that evaluates the length of the explicit list containing the three Generation constructors to 3 by definition.
why it matters
This result closes the derivation of the generation number in the 8-tick octave (T7) and 3D space (T8) of the forcing chain. It supports the experimental tests section by confirming the match to observed neutrino generations. The parent structure is the SpectralEmergence module, which forces 3 generations alongside the gauge content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.