Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Wide machines are complete for NEXPTIME and EXPSPACE

Lax822549.WideMachinesComplete · concepts/Lax822549/WideMachinesComplete.lean · lax-822549

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.

    Natural Language Statement

    Theorem

    Wide acceptance is in NEXPTIME, and wide acceptance with a regular channel is NEXPTIME-complete: a wide machine is an ordinary machine read over an exponential expansion, and hardness lays the computation of a problem of NEXPTIME out along the addresses, block by block. Wide acceptance in space is EXPSPACE-complete, deterministic or not. The three wide acceptance problems have yes-instances.

    Concept map
    22 concepts
    100%
    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.

    1 dwideAcceptSpace_EXPSPACE_complete proven

    2 dwideAcceptSpace_nonvacuous proven

    3 wideAccept_mem_NEXPTIME proven

    4 wideAccept_nonvacuous proven

    5 wideAcceptSpace_EXPSPACE_complete proven

    6 wideAcceptSpace_nonvacuous proven

    7 wideRegAccept_NEXPTIME_complete proven

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Classes
    3import Lax904597.Machines
    4import Lax485149.Problems
    5import Lax535992.DeterministicMachines
    6import Lax134656.SpaceBoundedMachines
    7import Lax480241.ExponentialClasses
    8import Lax822549.WideMachines
    9import Lax822549.WideRegChannel
    10import Lax822549.WideTilings
    11
    12/-!
    13---
    14title: Wide machines are complete for NEXPTIME and EXPSPACE
    15type: theorem
    16---
    17Wide acceptance is in NEXPTIME, and wide acceptance with a regular channel
    18is NEXPTIME-complete: a wide machine is an ordinary machine read over an
    19exponential expansion, and hardness lays the computation of a problem of
    20NEXPTIME out along the addresses, block by block. Wide acceptance in space
    21is EXPSPACE-complete, deterministic or not. The three wide acceptance
    22problems have yes-instances.
    23-/
    24
    25namespace Lax822549.WideMachinesComplete
    26
    27open FirstOrder FirstOrder.Language
    28open Lax904597.Problems Lax904597.Classes Lax904597.Machines Lax485149.Problems
    29 Lax480241.ExponentialClasses
    30open Lax822549.WideMachines Lax822549.WideRegChannel Lax822549.WideTilings
    31
    32/-- Wide acceptance is in NEXPTIME. -/
    33axiom wideAccept_mem_NEXPTIME :
    34 NEXPTIME.Mem WideAccept
    35
    36/-- Wide acceptance with a regular channel is NEXPTIME-complete. -/
    37axiom wideRegAccept_NEXPTIME_complete :
    38 NEXPTIME.Complete WideRegAccept
    39
    40/-- Wide acceptance in space is EXPSPACE-complete. -/
    41axiom wideAcceptSpace_EXPSPACE_complete :
    42 EXPSPACE.Complete WideAcceptSpace
    43
    44/-- Deterministic wide acceptance in space is EXPSPACE-complete. -/
    45axiom dwideAcceptSpace_EXPSPACE_complete :
    46 EXPSPACE.Complete DWideAcceptSpace
    47
    48/-- WideAccept has a finite yes-instance. -/
    49axiom wideAccept_nonvacuous :
    50 ∃ (A : Type) (_ : wide.Structure A), Finite A ∧ WideAccept A
    51
    52/-- WideAcceptSpace has a finite yes-instance. -/
    53axiom wideAcceptSpace_nonvacuous :
    54 ∃ (A : Type) (_ : wide.Structure A), Finite A ∧ WideAcceptSpace A
    55
    56/-- DWideAcceptSpace has a finite yes-instance. -/
    57axiom dwideAcceptSpace_nonvacuous :
    58 ∃ (A : Type) (_ : wide.Structure A), Finite A ∧ DWideAcceptSpace A
    59
    60end Lax822549.WideMachinesComplete
    61
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…