Version history

Submission versions

  1. lax-222097current version

    Max Independent Set Remains NP-hard when Excluding a Planar Induced Minor

  2. lax-762056viewing

    Max Independent Set Remains NP-hard when Excluding a Planar Induced Minor

    GitHub sourceShown on this page

Proof of `Asteroidal cycle triples obstruct induced minors` (2nd statement)

groundedproofs/Lax762056Proofs/GridWitness.lean · lax-762056

What this proof establishes

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

Three corner squares form an asteroidal triple, joined pairwise by paths along the boundary of the grid.