Lax Lean Archive

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

Proof of `Exhaustive search for small independent-set targets` (3rd statement)

groundedproofs/Lax263307Proofs/ExhaustiveTargets.lean · lax-263307

What this proof establishes

thm✓Lax263307.ExhaustiveTargets (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

The first successful candidate is an independent set of size kk. If an independent set had size at least kk after failure, selecting a size-kk subset would give a successful candidate, a contradiction.

Attribution

Bonnet–Chang, exhaustive-search rejection in Lemma 14.