sectorOf
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute numerical masses or gap values.
- Does not handle bosons or composite particles.
- Does not incorporate generation index or torsion.
- Does not prove any equality or inequality.
Lean usage
example : Sector := sectorOf .uformal statement (Lean)
38def sectorOf : Fermion → Sector
39| .d | .s | .b => .down
40| .u | .c | .t => .up
41| .e | .mu | .tau => .lepton
42| .nu1 | .nu2 | .nu3 => .neutrino
43