Lax Lean Archive

Correctness and complexity of the reduction

Lax689614.Reduction · concepts/Lax689614/Reduction.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

    Claims 9 and 10: for a formula with an odd number of clauses, the first player wins Arc Kayles on the constructed graph if and only if True wins the positive CNF game. The second player's winning implication is stated separately to expose the two strategy arguments.

    There is a polynomial-time many-one reduction on all binary strings. Before applying the construction, duplicate a clause if the nonempty clause list has even length. Handle the empty conjunction and malformed encodings separately by fixed yes and no instances.

    Concept map
    13 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 false_strategy proven

    2 polynomial_reduction proven

    3 true_strategy proven

    Lean source view on GitHub

    1import Lax689614.Construction
    2import Lax689614.PSPACE
    3
    4/-!
    5---
    6title: Correctness and complexity of the reduction
    7type: theorem
    8---
    9Claims 9 and 10: for a formula with an odd number of clauses, the first
    10player wins Arc Kayles on the constructed graph if and only if True wins
    11the positive CNF game. The second player's winning implication is stated
    12separately to expose the two strategy arguments.
    13
    14There is a polynomial-time many-one reduction on all binary strings.
    15Before applying the construction, duplicate a clause if the nonempty clause
    16list has even length. Handle the empty conjunction and malformed encodings
    17separately by fixed yes and no instances.
    18-/
    19
    20namespace Lax689614.Reduction
    21
    22open PositiveCNF Construction ArcKayles
    23
    24axiom false_strategy (φ : Formula) (hm : φ.clauses.length % 2 = 1)
    25 (h : ¬ FirstWins φ) : ¬ Winning (graph φ) (board φ)
    26
    27axiom true_strategy (φ : Formula) (hm : φ.clauses.length % 2 = 1)
    28 (h : FirstWins φ) : Winning (graph φ) (board φ)
    29
    30axiom polynomial_reduction :
    31 Lax429075.Reductions.ManyOne Encoding.positiveCNF Encoding.arcKayles
    32
    33end Lax689614.Reduction
    34
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…