pith. machine review for the scientific record. sign in
inductive definition def or abbrev high

Sector

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  31inductive Sector | up | down | lepton | neutrino
  32deriving DecidableEq, Repr
  33

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.