ymSectorCount
plain-language theorem explainer
The theorem fixes the configuration dimension of the Recognition Science Yang-Mills lattice at exactly five sectors. A lattice QCD or discrete gauge theorist would cite it to anchor the discrete mass-gap construction before passing to the continuum bridge. The proof is a one-line decision procedure that exploits the automatically generated Fintype instance on the five-constructor inductive type.
Claim. Let $YMSector$ be the inductive type whose constructors are gluonCondensate, plasma, quarkGluon, hadronic and vacuum. Then the cardinality of $YMSector$ equals 5.
background
The module derives a discrete Yang-Mills mass gap from the Recognition Science recognition lattice: any non-vacuum configuration carries strictly positive J-cost, with the gap bounded below by J(φ). The local setting states that five canonical sectors (gluon condensate, plasma, quark-gluon, hadronic, vacuum) realize configDim D = 5. YMSector is the inductive type with precisely those five constructors, from which DecidableEq, Repr, BEq and Fintype are derived automatically. Upstream gap definitions supply the numerical value 45 used in the broader lattice-gap certificate, but are not invoked by this cardinality statement.
proof idea
One-line wrapper that applies the 'decide' tactic. The tactic succeeds because the inductive definition of YMSector yields a decidable equality and a computable Fintype instance whose cardinality is immediately 5.
why it matters
The result supplies the five_sectors field of ymLatticeGapCert, the top-level certificate that packages vacuum_zero, gap_exists and vacuum_unique. It directly implements the module claim that five sectors realize configDim D = 5 in the discrete Yang-Mills lattice. The declaration closes the finite-sector scaffolding required before any continuum-limit argument (S1) can be attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.