SpectralSector
plain-language theorem explainer
SpectralSector enumerates the five canonical sectors of the Recognition Hamiltonian spectrum as vacuum, Goldstone, massive scalar, massive vector, and massive tensor. Researchers analyzing the mass gap and QFT decomposition in the Recognition Science model cite this classification when separating ground-state and excited modes. The definition is a direct inductive enumeration that derives decidable equality, representation, and finiteness instances with no further lemmas.
Claim. The Recognition Hamiltonian spectrum decomposes into five sectors: the vacuum sector (ground state with $J=0$), the Goldstone sector, the massive scalar sector, the massive vector sector, and the massive tensor sector.
background
The module defines the spectrum of the Recognition Hamiltonian on its associated Hilbert space. Ground state carries J-cost zero while excited states carry positive J-cost; the spectral gap is the infimum of J(r) for r > 0, r ≠ 1, which is positive once the underlying lattice is discretized. This five-sector partition equals configDim D = 5. It rests on the vacuum gauge-bond configuration (all bonds at rung 0) and on the upstream Q3 spectral decomposition into color, weak, hypercharge, and conjugate sectors whose dimensions sum to eight.
proof idea
The declaration is an inductive definition that introduces the five constructors vacuum, goldstone, massiveScalar, massiveVector, massiveTensor and immediately derives the instances DecidableEq, Repr, BEq, Fintype. No lemmas are invoked; the construction is self-contained.
why it matters
The type supplies the sector labels required by downstream results on sector-dimension sums, gauge-generator counts, fermion-flavor totals, and conjugate-dimension forcing in SpectralEmergence. It fills the S1 QFT-depth slot by connecting the Hamiltonian spectrum to the Yang-Mills mass-gap analysis. Within the Recognition framework it bridges J-uniqueness to the emergence of the eight-tick octave and the three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.