complexityClassCount
plain-language theorem explainer
Five complexity classes are enumerated in the Recognition Science taxonomy. Researchers formalizing P versus NP from a structural standpoint cite the count. The proof applies the decide tactic to the Fintype instance of the inductive enumeration.
Claim. The cardinality of the finite set of complexity classes is $5$, where the classes are P, NP, coNP, PSPACE and EXP.
background
The module defines five canonical complexity classes corresponding to configDim D = 5. ComplexityClass is the inductive type with constructors p, np, coNP, pspace, exp that derives DecidableEq, Repr, BEq and Fintype. This aligns with the RS view that P versus NP concerns whether recognition cost can be verified in polynomial time, with the conjecture that NP-complete problems exhibit an exponential number of J = 0 basins. Upstream, the identical five-class count appears in the P_vs_NP_From_RS module, accompanied by the note that proving P ≠ NP requires Clay-level work.
proof idea
The proof is a term-mode application of the decide tactic. This succeeds because the inductive type derives Fintype, allowing automatic computation of the cardinality.
why it matters
The count supplies the five_classes field to computationalComplexityCert and to pvsNPStructuralCert. It formalizes the structural 5-class taxonomy as a prerequisite for discussing the P ≠ NP conjecture within Recognition Science, where the eight-tick octave and D = 3 spatial dimensions underpin the DFT-8 size being polynomial. The open question of actual P ≠ NP separation remains outside the scope of this structural count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.