sectorOf
plain-language theorem explainer
The sector assignment function maps each of the twelve Standard Model fermions to one of four sectors. Researchers computing fermion masses via the phi-ladder or Z-indexed gap function cite this classification to route quarks, leptons, and neutrinos correctly. The definition is realized by exhaustive case analysis on the fermion constructors.
Claim. The mapping that sends down-type quarks to the down sector, up-type quarks to the up sector, charged leptons to the lepton sector, and neutrinos to the neutrino sector.
background
The RSBridge.Anchor module introduces the Fermion inductive type listing the six quarks, three charged leptons, and three neutrinos. Sector is the four-way classification into up, down, lepton, and neutrino. The sector assignment supplies the canonical routing used downstream to compute the charge index Z = q̃² + q̃⁴ (+4 for quarks) and the gap function F(Z) = ln(1 + Z/φ)/ln(φ) asserted to equal the integrated renormalization-group residue at the anchor scale μ⋆.
proof idea
The definition is realized by direct pattern matching on the twelve Fermion constructors with no auxiliary lemmas or tactics required.
why it matters
The mapping is invoked by ZOf to select the sector-dependent formula for the integer index and by the rung constructors to select torsion values. It is a prerequisite for the QuarkAbsoluteMassResidual proposition that equates the structural mass formula to the gap-corrected expression. The definition thereby anchors the bridge from the Recognition Science forcing chain to the observed fermion spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.