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

Sector

show as:
view Lean formalization →

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.

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

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.

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.