Sector
plain-language theorem explainer
This inductive definition introduces four constructors for fermion sectors in the RSBridge: up, down, lepton, and neutrino. Mass ladder calculations and spectral emergence proofs cite it to partition Standard Model fermions into recognition-derived categories for phi-exponent assignments. The definition is a direct inductive type declaration with automatic derivation of decidable equality and representation.
Claim. The inductive type with constructors up, down, lepton, and neutrino, used to classify fermion species for Z-indexing and gap functions in the recognition bridge.
background
The RSBridge.Anchor module defines the core bridge from the recognition framework to particle physics. It introduces Fermion as the 12 Standard Model species, ZOf as the charge-indexed integer Z_i = q̃² + q̃⁴ (+4 for quarks), and gap(F) as the closed-form display function F(Z) = ln(1 + Z/φ)/ln(φ). Sector partitions these into four categories, with neutrino kept distinct from lepton due to its zero baseline. Upstream results supply parallel inductive Sector types: one with Lepton/UpQuark/DownQuark/Electroweak in Masses.Anchor, and one with five variants including Neutrino in RungConstructor.Basic.
proof idea
Inductive definition with four constructors, deriving DecidableEq and Repr. No lemmas or tactics are invoked; it serves as the base type for downstream functions such as sectorOf and gap.
why it matters
Sector supplies the partitioning used by totalCost_nonneg to verify nonnegative costs over physical domains, by SpectralSector for the B3 decomposition into color/weak/hypercharge layers, and by B_pow and r0 to derive sector-specific powers and phi-exponent offsets from cube geometry. It fills the fermion classification step in the single-anchor phenomenology claim, where gap(ZOf i) approximates the integrated RG residue at the anchor scale μ⋆, connecting to the phi-ladder mass formula and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.