ComplexityClass
This declaration introduces the inductive type enumerating the five canonical complexity classes in the Recognition Science treatment of P versus NP. It is cited by downstream certificates establishing that the cardinality is five and that the per-cycle recognition budget factors as eight times forty-five. The definition proceeds by direct enumeration of the constructors P, NP, coNP, PSPACE, and EXPTIME, deriving the necessary typeclass instances for decidability and finiteness.
claimLet $C$ be the inductive type whose constructors are the five standard complexity classes P, NP, coNP, PSPACE, and EXPTIME, equipped with decidable equality and finite cardinality.
background
In the module on P versus NP from Recognition Science, the per-cycle bandwidth is given as 360, which equals eight times forty-five, arising from the eight-tick octave and gap-45. The five canonical complexity classes are identified with configuration dimension D equal to five. An upstream definition in ComputationalComplexityFromRS provides a similar enumeration using lowercase constructors p, np, coNP, pspace, and exp.
proof idea
The declaration is a direct inductive definition. It enumerates the five constructors and derives DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters in Recognition Science
This definition supplies the finite taxonomy required by the structural certificate PvsNPStructuralCert, which records that the cardinality is five and that the recognition budget equals eight times forty-five. It formalizes the observation that the number of classes matches configuration dimension five, consistent with the eight-tick structure in the forcing chain. Note that establishing P not equal to NP remains a Clay-level open question outside the scope of this structural setup.
scope and limits
- Does not prove equality or inequality between P and NP.
- Does not provide explicit algorithms or reductions between problems.
- Does not link the class count to the spatial dimension three from the forcing chain.
- Does not compute or derive the recognition budget value.
formal statement (Lean)
35inductive ComplexityClass where
36 | P | NP | coNP | PSPACE | EXPTIME
37 deriving DecidableEq, Repr, BEq, Fintype
38