Lax Lean Archive

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

Tilings one exponential up are complete

Lax822549.TilingsComplete · concepts/Lax822549/TilingsComplete.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

    Square tiling one exponential up is NEXPTIME-complete and corridor tiling one exponential up is EXPSPACE-complete, the classical second complete problems of the two classes beside a machine: the rows of a tiling are the configurations of a wide machine.

    Concept map
    22 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 wideCorridor_EXPSPACE_complete proven

    2 wideTiling_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: Tilings one exponential up are complete
    15type: theorem
    16---
    17Square tiling one exponential up is NEXPTIME-complete and corridor tiling
    18one exponential up is EXPSPACE-complete, the classical second complete
    19problems of the two classes beside a machine: the rows of a tiling are the
    20configurations of a wide machine.
    21-/
    22
    23namespace Lax822549.TilingsComplete
    24
    25open FirstOrder FirstOrder.Language
    26open Lax904597.Problems Lax904597.Classes Lax904597.Machines Lax485149.Problems
    27 Lax480241.ExponentialClasses
    28open Lax822549.WideMachines Lax822549.WideRegChannel Lax822549.WideTilings
    29
    30/-- Square tiling one exponential up is NEXPTIME-complete. -/
    31axiom wideTiling_NEXPTIME_complete :
    32 NEXPTIME.Complete WideTiling
    33
    34/-- Corridor tiling one exponential up is EXPSPACE-complete. -/
    35axiom wideCorridor_EXPSPACE_complete :
    36 EXPSPACE.Complete WideCorridor
    37
    38end Lax822549.TilingsComplete
    39
    Show 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…