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

SpectralSector

show as:
view Lean formalization →

The SpectralSector inductive type enumerates four layers of the B3 symmetry decomposition of the 3-cube Q3, with constructors color, weak, hypercharge, and conjugate. Researchers deriving Standard Model gauge structure from Recognition Science's forced D=3 would cite this when decomposing vertex count into sector dimensions. The definition proceeds by direct enumeration followed by pattern-matching assignments for dim, gauge_rank, and matter_dim.

claimThe spectral sectors of the binary 3-cube are the four types color (dimension 3, corresponding to SU(3)), weak (dimension 2, SU(2)), hypercharge (dimension 1, U(1)), and conjugate (dimension 2), with total dimension summing to 8 = 2^3.

background

In the Spectral Emergence module the binary cube is introduced via the sibling definition V(D) := 2^D, so that D=3 yields exactly eight vertices. The module document states that T8 forces Q3 whose symmetry B3 = S3 ⋉ (Z/2Z)^3 decomposes into the listed sectors, producing the gauge content SU(3) × SU(2) × U(1) together with a residual conjugate sector. Upstream results supply the Dimension structure (exponents for length, time, mass) and the native-unit gauge U with c=1, tau0=1 tick.

proof idea

The declaration is an inductive definition introducing the four constructors color, weak, hypercharge, conjugate. The three auxiliary functions dim, gauge_rank, and matter_dim are each defined by exhaustive pattern matching that assigns the fixed natural-number values listed in the doc-comment.

why it matters in Recognition Science

This definition supplies the sector decomposition on which downstream results such as sector_dim_sum, gauge_generators_eq_edges, and fermion_flavors rest; those theorems establish that gauge generators equal the edge count of Q3 and that chiral fermion flavors total 24. It fills the explicit step in the module's self-consistency loop from T8 (D=3) through the eight-tick octave to the Standard Model gauge group and the phi-ladder mass hierarchy. The framework landmark is the equality |Aut(Q3)| = 48 matching the chiral fermion state count.

scope and limits

formal statement (Lean)

 131inductive SpectralSector where
 132  | color : SpectralSector
 133  | weak : SpectralSector
 134  | hypercharge : SpectralSector
 135  | conjugate : SpectralSector
 136  deriving DecidableEq, Repr
 137
 138/-- Dimension of each spectral sector. -/
 139def SpectralSector.dim : SpectralSector → ℕ
 140  | .color => 3
 141  | .weak => 2
 142  | .hypercharge => 1
 143  | .conjugate => 2
 144
 145/-- The gauge group rank (dimension of the Lie algebra generators)
 146    associated with each sector. -/
 147def SpectralSector.gauge_rank : SpectralSector → ℕ
 148  | .color => 8           -- SU(3): 3²-1 = 8 generators
 149  | .weak => 3            -- SU(2): 2²-1 = 3 generators
 150  | .hypercharge => 1     -- U(1): 1 generator
 151  | .conjugate => 0       -- Not a gauge sector
 152
 153/-- The matter representation dimension (how many components
 154    a fermion field has in this sector). -/
 155def SpectralSector.matter_dim : SpectralSector → ℕ
 156  | .color => 3
 157  | .weak => 2
 158  | .hypercharge => 1
 159  | .conjugate => 2
 160
 161/-! ### Sector Dimension Theorems -/
 162
 163/-- **THEOREM**: Sector dimensions sum to 8 = |V(Q₃)|.
 164    The spectral decomposition accounts for every vertex. -/

used by (10)

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

depends on (32)

Lean names referenced from this declaration's body.

… and 2 more