time_bounded_eq_co_of_decider_negation_closed

theoremverifiedoriginal

Let T be a time bound and suppose the family of deciders computable within T steps is closed under Boolean negation, i.e. for every f : List Γ → Bool computed in time T there is g computed in time T with g w = !f w. Then the time-bounded class C = TimeBounded Γ T equals its complement class CoClass C: for every language L, L is decidable in time T if and only if its complement is.

Statement

theorem time_bounded_eq_co_of_decider_negation_closed {Γ : Type} {T : ℕ → ℕ}
    (hD : ∀ f : List Γ → Bool,
      (∃ M : Turing.TM2ComputableInTime (id : List Γ → List Γ) Computability.encodeBool f,
        ∀ n, M.time n ≤ T n) →
      ∃ M : Turing.TM2ComputableInTime (id : List Γ → List Γ) Computability.encodeBool
        (fun w => !f w), ∀ n, M.time n ≤ T n) :
    ∀ L : Language Γ, TimeBounded Γ T L ↔ CoClass (TimeBounded Γ T) L

Source

Bridges the existing knowledge-base definition CoClass with the time-bounded decider classes defined here (Sipser, Sec. 7.5 on complementation; Sipser, Thm. 7.29 for a concrete instance).

Verified

10 Sep 2026

Axioms

Classical.choiceQuot.soundpropext

Built on 3

TimeBoundedA language L over an alphabet Γ is decidable in time T (T : ℕ → ℕ) if there is a total decider f : List Γ → Bool together with a Turing…
CoClassThe complement class co(C) of a complexity class C on languages over alphabet α consists of all languages L whose complement is in C.
decider_class_eq_coAny complexity class defined by a family of deciders that is closed under negation equals its complement class.

Read back from the Lean

Fix an arbitrary type Γ (no finiteness or decidability assumed) and an arbitrary time-bound function T : ℕ → ℕ. The declaration takes one hypothesis, hD: for every Boolean-valued function f : List Γ → Bool, **if** f is computable by some Turing machine in time ≤ T (i.e. there exists an M : Turing.TM2ComputableInTime (id) (Computability.encodeBool) f with M.time n ≤ T n for every n), **then** the pointwise boolean negation fun w => !f w is likewise computable in time ≤ T (there exists such an M with M.time n ≤ T n for every n). So hD says the class of T-time-bounded deciders of Γ-lists is closed under boolean complementation. The conclusion asserts: for **every** language L : Language Γ (= every predicate on List Γ), TimeBounded Γ T L ↔ CoClass (TimeBounded Γ T) L, i.e. L is T-time-bounded if and only if the complementary class of L is T-time-bounded (CoClass C L is by definition C Lᶜ). Concretely: L is T-time-decidable (there is a Bool-valued decider f computed within T whose true-set is exactly L) **iff** the complement Lᶜ is T-time-decidable. The forward direction is hD applied to a decider of L; the backward direction is hD applied to a decider of Lᶜ (using Lᶜᶜ = L), so the biconditional is a genuine two-sided statement, both sides of which invoke the hypothesis. All binders are as written: Γ and T are arbitrary (not existentially quantified inside), f is universally quantified inside hD before the implication, L is universally quantified in the conclusion, and the time bounds are required to hold for *all* n, not merely infinitely many.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- A time-bounded class whose deciders are closed under negation equals its own complement class. -/
theorem time_bounded_eq_co_of_decider_negation_closed {Γ : Type} {T : ℕ → ℕ}
    (hD : ∀ f : List Γ → Bool,
      (∃ M : Turing.TM2ComputableInTime (id : List Γ → List Γ) Computability.encodeBool f,
        ∀ n, M.time n ≤ T n) →
      ∃ M : Turing.TM2ComputableInTime (id : List Γ → List Γ) Computability.encodeBool
        (fun w => !f w), ∀ n, M.time n ≤ T n) :
    ∀ L : Language Γ, TimeBounded Γ T L ↔ CoClass (TimeBounded Γ T) L := by
  intro L
  exact decider_class_eq_co (α := Γ)
    (fun f : List Γ → Bool => ∃ M : Turing.TM2ComputableInTime (id : List Γ → List Γ)
      Computability.encodeBool f, ∀ n, M.time n ≤ T n) hD L

Discuss this result Challenge it