theorem proved term proof

`complexityClassCount`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  39theorem complexityClassCount : Fintype.card ComplexityClass = 5 := by decide

proof body

Term-mode proof.

  40
  41/-- P ⊆ NP (structural). -/
  42-- Note: proving P ≠ NP requires Clay-level work, not doable here.
  43-- We just formalise the structural 5-class taxonomy.
  44

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

complexityClassCount in IndisputableMonolith.Mathematics.ComputationalComplexityFromRS decl_use
computationalComplexityCert in IndisputableMonolith.Mathematics.ComputationalComplexityFromRS decl_use
pvsNPStructuralCert in IndisputableMonolith.Mathematics.P_vs_NP_From_RS decl_use

depends on (3)

Lean names referenced from this declaration's body.

ComplexityClass in IndisputableMonolith.Mathematics.ComputationalComplexityFromRS decl_use
complexityClassCount in IndisputableMonolith.Mathematics.ComputationalComplexityFromRS decl_use
ComplexityClass in IndisputableMonolith.Mathematics.P_vs_NP_From_RS decl_use