ComplexityClass
plain-language theorem explainer
Recognition Science encodes the standard complexity hierarchy as an inductive type whose five constructors stand for P, NP, coNP, PSPACE, and EXP. Researchers formalizing the structural side of the P versus NP question inside the Recognition framework cite this type when counting classes or building certificates. The declaration proceeds by direct enumeration of the constructors followed by a deriving clause that installs decidable equality, representation, boolean equality, and a finite-type instance.
Claim. The inductive type of complexity classes is generated by the five constructors corresponding to P, NP, coNP, PSPACE, and EXP and carries instances of decidable equality and finite type.
background
The module Computational Complexity from RS identifies the five canonical complexity classes with configuration dimension D = 5. In Recognition Science the P versus NP distinction asks whether recognition cost can be verified in polynomial time; the conjecture asserts inequality because NP-complete problems possess a J-cost landscape containing an exponential number of J = 0 basins. The DFT computation over Z/8Z lies in P because the group order equals 2^D = 8.
proof idea
The declaration is a direct inductive definition that lists the five constructors and attaches the deriving clause for DecidableEq, Repr, BEq, and Fintype.
why it matters
This definition supplies the taxonomy required by the downstream theorem complexityClassCount establishing cardinality five and by the structure ComputationalComplexityCert that records the class count together with DFT size eight. It fills the structural slot in the RS treatment of P versus NP, where the five-class count aligns with the eight-tick octave and the forcing-chain dimension D = 5. The open question whether P equals NP lies outside the present formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.