complexityClassCount
complexityClassCount establishes that the finite type of complexity classes has cardinality five. Researchers formalizing P versus NP distinctions inside Recognition Science would cite it to fix the taxonomy before constructing certificates. The proof is a one-line wrapper that invokes the decide tactic on the derived Fintype instance.
claimLet $C$ be the finite type whose elements are the five complexity classes P, NP, coNP, PSPACE and EXP. Then $|C| = 5$.
background
The module defines an inductive type ComplexityClass with constructors p, np, coNP, pspace, exp that derives DecidableEq, Repr, BEq and Fintype. The module doc states that these five classes equal configDim D = 5 and that DFT computation of size 8 = 2^D lies in P. An identical inductive definition and the same cardinality statement appear in the sibling module P_vs_NP_From_RS, where the doc notes that the result only formalises the structural taxonomy.
proof idea
The proof is a term-mode one-liner that applies the decide tactic. Because ComplexityClass derives Fintype, decide evaluates Fintype.card directly to 5.
why it matters in Recognition Science
The theorem supplies the five_classes field required by computationalComplexityCert and pvsNPStructuralCert. It anchors the five-class taxonomy used to express the RS conjecture that P ≠ NP follows from an exponential number of J = 0 basins in the J-cost landscape. The result aligns with the framework claim that configDim D = 5 and that DFT-8 size equals 2^D.
scope and limits
- Does not prove P ≠ NP.
- Does not compute J-cost for concrete problems.
- Does not derive the classes from the T0-T8 forcing chain.
- Does not supply explicit time or space bounds.
Lean usage
def cert : ComputationalComplexityCert := { five_classes := complexityClassCount, dft_poly := dft8Size_8 }formal statement (Lean)
26theorem complexityClassCount : Fintype.card ComplexityClass = 5 := by decide
proof body
Term-mode proof.
27
28/-- DFT-8 size = 2^D = 8. -/