Sector
plain-language theorem explainer
The declaration introduces five particle sectors for classifying masses on the phi-ladder: leptons, neutrinos, up quarks, down quarks, and electroweak bosons. Researchers constructing the mass spectrum from the Recognition Science forcing chain reference these sectors when assigning rung values. It is implemented as a simple inductive type with equality and representation instances to serve as a local copy preventing circular module dependencies.
Claim. The particle sectors form an inductive type whose constructors are lepton, neutrino, up-quark, down-quark, and electroweak.
background
The module supplies canonical species for the mass framework. This sector type is a local duplicate of the Anchor version to break import cycles. It separates neutrino from lepton because the two carry distinct baselines (0 versus 2) in rung calculations. Upstream, the lepton inductive from CubeFaceUniversality enumerates electron, muon, tau, and the three neutrino flavors. The rung definitions in Compat.Constants and AnchorPolicy supply integer offsets for each sector. These feed into derived quantities such as B_pow and r0 in the Anchor module.
proof idea
The declaration is a direct inductive definition with five constructors and automatic derivation of decidable equality and representation. No lemmas or tactics are applied; the type is introduced as the base for sector-specific mass formulas.
why it matters
This definition supports the mass ladder construction and appears in downstream results such as totalCost_nonneg in QRFT.SMLagrangianSkeleton, which requires nonnegative costs across sectors, and in SpectralSector for decomposing the cube geometry into color, weak, and hypercharge components. It realizes the sector constants derived from cube edge counting in the Recognition framework, linking to the eight-tick octave and three spatial dimensions via the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.