pith. machine review for the scientific record. sign in
structure definition def or abbrev

RecognitionComplete

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  56structure RecognitionComplete where
  57  /-- Computation complexity: internal evolution steps -/
  58  Tc : ℕ → ℕ
  59  /-- Recognition complexity: observation operations -/
  60  Tr : ℕ → ℕ
  61  /-- Computation is sub-polynomial -/
  62  Tc_subpoly : ∃ (c : ℝ) (k : ℝ), 0 < k ∧ k < 1 ∧ ∀ n, n > 0 → Tc n ≤ c * n^k * Real.log n
  63  /-- Recognition is at least linear -/
  64  Tr_linear : ∃ (c : ℝ), c > 0 ∧ ∀ n, n > 0 → Tr n ≥ c * n
  65
  66/-- The Turing model as a special case with zero recognition complexity. -/

used by (6)

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

depends on (8)

Lean names referenced from this declaration's body.