Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax434930.BasicProperties

Elementary properties of the complexity classes

concepts/Lax434930/BasicProperties.lean · lax-434930

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    This concept declares 7 statements. Each proof establishes one of them relative to its assumptions.

    1st statement co_co proven

    2nd statement L_subset_NL proven

    3rd statement L_subset_PSPACE proven

    4th statement mem_coNP_iff proven

    5th statement NL_subset_NPSPACE proven

    6th statement P_subset_EXPTIME proven

    7th statement PSPACE_subset_NPSPACE proven

    Theorem

    Deterministic space is contained in nondeterministic space, both for logarithmic and polynomial bounds. Logarithmic space is contained in polynomial space, in both settings. Polynomial time is contained in exponential time. Applying the class operation co twice recovers the original class, and a language belongs to coNP exactly when every polynomially bounded certificate is rejected by a suitable P verifier.

    Lean source view on GitHub

    1import Lax434930.LogarithmicSpace
    2import Lax434930.NondeterministicLogarithmicSpace
    3import Lax434930.PolynomialSpace
    4import Lax434930.NondeterministicPolynomialSpace
    5import Lax434930.ComplementClasses
    6import Lax434930.ExponentialTime
    7
    8/-!
    9---
    10title: Elementary properties of the complexity classes
    11type: theorem
    12---
    13Deterministic space is contained in nondeterministic space, both for
    14logarithmic and polynomial bounds. Logarithmic space is contained in
    15polynomial space, in both settings. Polynomial time is contained in
    16exponential time. Applying the class operation co twice recovers the
    17original class, and a language belongs to coNP exactly when every
    18polynomially bounded certificate is rejected by a suitable P verifier.
    19-/
    20
    21namespace Lax434930.BasicProperties
    22
    23open PolynomialTime LogarithmicSpace NondeterministicLogarithmicSpace
    24open PolynomialSpace NondeterministicPolynomialSpace ComplementClasses
    25open ExponentialTime Certificates
    26
    27axiom L_subset_NL : L ⊆ NL
    28
    29axiom PSPACE_subset_NPSPACE : PSPACE ⊆ NPSPACE
    30
    31axiom L_subset_PSPACE : L ⊆ PSPACE
    32
    33axiom NL_subset_NPSPACE : NL ⊆ NPSPACE
    34
    35axiom P_subset_EXPTIME : P ⊆ EXPTIME
    36
    37axiom co_co (C : Set Language) : co (co C) = C
    38
    39/-- Universal certificate characterization, with the same explicit encoding as NP. -/
    40axiom mem_coNP_iff (A : Language) : A ∈ coNP ↔
    41 ∃ V : Language, V ∈ P ∧ ∃ p : Polynomial ℕ, ∀ x : Word,
    42 x ∈ A ↔ ∀ y : Word, y.length ≤ p.eval x.length → pair x y ∉ V
    43
    44end Lax434930.BasicProperties
    45
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…