Sector
plain-language theorem explainer
Sector enumerates four fermion classes (up, down, lepton, neutrino) that index mass and cost functions in the RS bridge to particle physics. Mass modelers cite it when mapping species to phi-ladder rungs via gap(Z) and sector offsets. The declaration is a bare inductive type with automatic DecidableEq and Repr derivations.
Claim. The inductive type Sector with four constructors up, down, lepton, neutrino.
background
The RSBridge.Anchor module supplies the interface from recognition framework to Standard Model fermion masses. Sector labels the four categories required for the charge-indexed ZOf and the gap display function F(Z) = ln(1 + Z/φ)/ln(φ). Upstream Sector copies exist in Masses.Anchor (Lepton, UpQuark, DownQuark, Electroweak) and RungConstructor.Basic (explicit Neutrino). The module states that gap(ZOf i) equals the integrated RG residue at anchor scale μ⋆ within ~1e-6 tolerance.
proof idea
The declaration is a direct inductive definition introducing four nullary constructors. It derives DecidableEq and Repr with no further structure. No lemmas or tactics are invoked; the type exists solely to index dependent definitions such as r0 and B_pow.
why it matters
Sector supplies the domain for B_pow and r0 that enter the mass formula yardstick * phi^(rung - 8 + gap(Z)). It is referenced by totalCost_nonneg in the QRFT Lagrangian skeleton and by SpectralSector in emergence constructions. The definition supports the single-anchor claim that family mass ratios are pure phi-powers for equal-Z species. It connects to the phi fixed point and eight-tick octave through the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.