spectralSectorCount
Recognition Science models the Hamiltonian spectrum with exactly five sectors: vacuum, Goldstone, massive scalar, massive vector, and massive tensor. A physicist checking the discrete spectrum count against configDim D would cite this result when confirming the mass gap setup. The proof reduces to a single decision procedure that enumerates the constructors of the finite inductive type.
claimThe finite set of spectral sectors has cardinality 5, where the sectors are the vacuum sector (J-cost zero), the Goldstone sector, and the massive scalar, vector, and tensor sectors.
background
The Recognition Hamiltonian spectrum module partitions the spectrum of Ĥ_RS into five canonical sectors that equal configDim D = 5. These sectors are vacuum (ground state with J = 0), Goldstone, massive scalar, massive vector, and massive tensor. The module notes that the spectral gap Δ_RS is positive once the lattice spacing a is introduced, consistent with the mass gap for Yang-Mills.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic computes the cardinality of the finite type by enumerating its five constructors and confirms equality to 5.
why it matters in Recognition Science
The result supplies the five_sectors component of the HamiltonianSpectrumCert definition downstream. It fills the module step that sets the sector count equal to configDim D = 5 and supports the discretization argument for the spectral gap. In the framework it connects to T8 on spatial dimensions and the overall count of physical modes.
scope and limits
- Does not compute explicit J-cost values for the excited sectors.
- Does not prove positivity of the spectral gap.
- Does not address the continuous limit of the spectrum.
- Does not establish dynamical stability of individual sectors.
Lean usage
five_sectors := spectralSectorCountformal statement (Lean)
32theorem spectralSectorCount : Fintype.card SpectralSector = 5 := by decide
proof body
Term-mode proof.
33
34/-- Vacuum sector: J = 0. -/