Lax Lean Archive

Arc Kayles is PSPACE-complete

Lax689614.Completeness · concepts/Lax689614/Completeness.lean · lax-689614

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

    Theorem 1. Determining the winner of Arc Kayles on a finite simple undirected graph is PSPACE-complete under polynomial-time many-one reductions. Membership follows by depth-first evaluation of the game tree: at most n/2n/2 moves are played and each position uses O(n2)O(n^2) bits. Hardness follows from the positive CNF game and the reduction graph.

    Concept map
    15 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 membership proven

    2 pspace_complete proven

    Lean source view on GitHub

    1import Lax689614.Reduction
    2import Lax689614.PositiveCNFHardness
    3
    4/-!
    5---
    6title: Arc Kayles is PSPACE-complete
    7type: theorem
    8---
    9Theorem 1. Determining the winner of Arc Kayles on a finite simple
    10undirected graph is PSPACE-complete under polynomial-time many-one
    11reductions. Membership follows by depth-first evaluation of the game tree:
    12at most n/2n/2 moves are played and each position uses O(n2)O(n^2) bits.
    13Hardness follows from the positive CNF game and the reduction graph.
    14-/
    15
    16namespace Lax689614.Completeness
    17
    18axiom membership : Encoding.arcKayles ∈ Lax434930.PolynomialSpace.PSPACE
    19
    20axiom pspace_complete : PSPACE.Complete Encoding.arcKayles
    21
    22end Lax689614.Completeness
    23
    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…