HypotheticalFermion
plain-language theorem explainer
HypotheticalFermion introduces an inductive extension of the standard RSBridge.Fermion type by adjoining a single constructor for a fourth sterile neutrino. Physicists testing neutrino-sector minimality in the Recognition Science framework cite this definition when checking whether a fourth generation can be added without breaking the surjectivity of genOf onto Fin 3. The declaration is a direct inductive extension of the upstream Fermion type with no additional proof obligations.
Claim. Inductive type extending the fermion enumeration with one additional constructor for a hypothetical fourth sterile neutrino generation.
background
The base Fermion type enumerates the twelve standard-model fermions: the six quarks (d, s, b, u, c, t), the three charged leptons (e, mu, tau), and the three neutrinos (nu1, nu2, nu3). RSBridge supplies the geometric structure that determines mixing angles and couplings from the underlying ledger. The SterileExclusion module encodes the modeling assumption that only three neutrino generations exist, expressed by the surjectivity of genOf onto Fin 3.
proof idea
The declaration is an inductive definition that directly extends the upstream Fermion inductive type by adding the sterile_nu4 constructor. No lemmas or tactics are invoked; the extension is stated verbatim.
why it matters
The definition supplies the hypothetical object used by genOf_hyp and no_sterile to derive the contradiction that a fourth generation cannot be surjective onto Fin 4 while preserving the three-generation minimality already enforced by RSBridge.genOf_surjective. It therefore closes the modeling choice for sterile-neutrino exclusion inside the three-generation structure required by the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.