fermionSector
fermionSector maps each of the nine charged fermions to one of three sectors for use in mass predictions. Mass-law applications in the SM verification module cite this assignment to select the correct yardstick before applying the phi-power formula. The definition is realized by exhaustive pattern matching on the Fermion constructors.
claimDefine the map from the fermion set to sectors by sending every lepton (electron, muon, tauon) to the Lepton sector, every up-type quark (up, charm, top) to the UpQuark sector, and every down-type quark (down, strange, bottom) to the DownQuark sector.
background
The SMVerification module states RS mass predictions for Standard Model particles via the law m(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z)), with sectors and yardsticks derived from cube geometry (D=3). The local Fermion inductive type enumerates the nine charged fermions. Upstream, the Sector type (from Anchor and RungConstructor) supplies the constructors Lepton, UpQuark, DownQuark, Electroweak whose constants are derived from cube faces.
proof idea
Direct definition by exhaustive pattern matching on the nine Fermion constructors, each routed to its fixed Sector value.
why it matters in Recognition Science
The mapping is invoked by fermionMass and fermionZ to supply the sector argument to predict_mass. It supplies the sector classification step required by the mass law, connecting to the phi-ladder and T8 (D=3) geometry. The module uses the result to document PDG comparisons as hypotheses.
scope and limits
- Does not compute numerical mass values.
- Does not include neutrinos.
- Does not derive yardstick constants or rung numbers.
- Does not perform experimental comparisons.
formal statement (Lean)
41def fermionSector : Fermion → Sector
42 | .electron | .muon | .tauon => .Lepton
43 | .up | .charm | .top => .UpQuark
44 | .down | .strange | .bottom => .DownQuark
45