no_sterile
plain-language theorem explainer
The theorem shows that the generation assignment for hypothetical fermions cannot be surjective onto four indices. Particle physicists working within the Recognition Science bridge would cite it to enforce exactly three neutrino generations. The proof assumes surjectivity, extracts a preimage for index 3, identifies it as the sterile neutrino constructor, and derives a contradiction with the established surjectivity of the base RSBridge generation map onto Fin 3.
Claim. Let $genOf_{hyp}$ map hypothetical fermions to the four-element set $Fin 4$. Then $genOf_{hyp}$ is not surjective.
background
The module encodes the modelling choice that only three neutrino generations are available. RSBridge.genOf is surjective onto Fin 3, which indexes the observed generations. HypotheticalFermion extends the RSBridge fermions by a single sterile_nu4 constructor whose generation index would fall outside this range. Upstream results supply the rung natural-number indexing for fermion sectors and the band operation that multiplies stable-state bits.
proof idea
The tactic proof assumes surjectivity of genOf_hyp. It obtains a preimage f for the index 3. Case analysis on f forces f to be the sterile_nu4 constructor. This produces an immediate contradiction because genOf_hyp on any toRSBridge fermion reduces to RSBridge.genOf, whose image lies strictly inside Fin 3.
why it matters
The result justifies the three-generation modelling choice inside the Recognition Science framework. It closes the hypothetical extension while preserving minimality of the generation map. The argument aligns with the eight-tick octave that discretizes the generation structure and prevents extension beyond Fin 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.