inductive
definition
ComplexityClass
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.ComputationalComplexityFromRS on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
19
20namespace IndisputableMonolith.Mathematics.ComputationalComplexityFromRS
21
22inductive ComplexityClass where
23 | p | np | coNP | pspace | exp
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem complexityClassCount : Fintype.card ComplexityClass = 5 := by decide
27
28/-- DFT-8 size = 2^D = 8. -/
29def dft8Size : ℕ := 2 ^ 3
30theorem dft8Size_8 : dft8Size = 8 := by decide
31
32structure ComputationalComplexityCert where
33 five_classes : Fintype.card ComplexityClass = 5
34 dft_poly : dft8Size = 8
35
36def computationalComplexityCert : ComputationalComplexityCert where
37 five_classes := complexityClassCount
38 dft_poly := dft8Size_8
39
40end IndisputableMonolith.Mathematics.ComputationalComplexityFromRS