sectorOf
plain-language theorem explainer
This definition maps each canonical Species (fermions via RSBridge or the bosons W, Z, H) to its Sector identifier for use in rung construction. Mass-ladder derivations in Recognition Science cite it when assigning particles to Lepton, Neutrino, UpQuark, DownQuark or Electroweak before applying the phi-ladder formula. The implementation is a direct pattern match that delegates fermion cases to the RSBridge classification and assigns bosons uniformly to Electroweak.
Claim. The function sectorOf : Species → Sector is defined by cases: for fermion f it returns Lepton when RSBridge.sectorOf f is lepton, Neutrino when neutrino, UpQuark when up, DownQuark when down; for W, Z or H it returns Electroweak.
background
In the Masses.RungConstructor.Basic module the inductive type Species classifies particles as fermion f (where f ranges over RSBridge.Fermion) or the bosons W, Z, H. The companion inductive Sector supplies the five identifiers Lepton, Neutrino, UpQuark, DownQuark, Electroweak; the module note records that Neutrino is kept distinct from Lepton because the two carry different baseline rung values (0 versus 2). The local setting is the canonical species list required by the mass framework so that every particle can be routed to the correct phi-ladder rung constructor. The definition depends on the upstream RSBridge.sectorOf (which performs the lepton/neutrino/up/down split) and on the CostAlgebra and RSNativeUnits constants that later supply the numerical yardstick and gap corrections.
proof idea
The definition is a direct pattern match on the Species constructor. Fermion cases invoke RSBridge.sectorOf and translate its four possible results into the local Sector constructors; the three boson cases are hard-coded to Electroweak. No lemmas or tactics are invoked; the body is a pure definitional expansion.
why it matters
sectorOf is invoked by compute_rung_sdgt and compute_rung to select the sector-dependent torsion terms ell_baseline and tau_sdgt, and by QuarkAbsoluteMassResidual to equate the structural rs_mass_MeV formula with the gap-corrected massAtAnchor expression on a chosen quark sector. It therefore supplies the sector-assignment step inside the Recognition mass formula yardstick · phi^(rung − 8 + gap(Z)), linking the J-functional equation and the phi fixed point (T5–T6) to concrete particle masses. The declaration closes the interface between the RSBridge fermion taxonomy and the local rung motifs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.