Lax Lean Archive

Version history

Submission versions

  1. lax-783278current version

    Arc Kayles is PSPACE-complete

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceOpen version
  2. lax-689614viewing

    Arc Kayles is PSPACE-complete

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceShown on this page

Proof of `Correctness and complexity of the reduction` (3rd statement)

groundedproofs/Lax689614Proofs/TrueSimulation.lean · lax-689614

What this proof establishes

thm✓Lax689614.Reduction (3rd statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Simulate True's CNF strategy until the formula is satisfied, then consume the remaining regular moves. The last phase uses paired replies on a protected biclique with surviving literal witnesses for every clause.