complexityClassCount
plain-language theorem explainer
The theorem records that the Recognition Science complexity taxonomy contains exactly five classes. Workers formalizing structural P versus NP bounds inside the eight-tick recognition framework cite this cardinality when linking per-cycle budget to exponential search workloads. The proof is a direct computation via the decide tactic on the Fintype instance of the inductive enumeration.
Claim. The set of complexity classes $P$, $NP$, $coNP$, $PSPACE$, $EXPTIME$ has cardinality 5.
background
The module develops a structural account of P versus NP by anchoring per-cycle recognition budget at 360 = 8 × 45 and observing that exponential search 2^n eventually exceeds any polynomial number of cycles. The inductive type ComplexityClass enumerates the five canonical classes P, NP, coNP, PSPACE and EXPTIME, which the module equates to configDim D = 5. An upstream result in ComputationalComplexityFromRS records the identical cardinality for a lowercase variant of the same inductive type, confirming the count is stable across naming conventions.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance automatically derived from the inductive definition of ComplexityClass.
why it matters
This cardinality supplies the five_classes field required by the downstream pvsNPStructuralCert definition, which also records the 360-cycle budget and the structural factoring. It formalizes the claim that configDim D equals 5 inside the Recognition Science framework and thereby anchors the lower-bound argument separating polynomial from exponential regimes. The parent theorem pvsNPStructuralCert uses this count to certify the separation between P and NP regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.