Lax Lean Archive

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

Exhaustive search for small independent-set targets

Lax263307.ExhaustiveTargets · concepts/Lax263307/ExhaustiveTargets.lean · lax-263307

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

    For a small target kk, enumerate exactly the kk-element vertex sets and test independence. The first success has size exactly kk. If the search fails, every independent set has size less than kk. There are exactly (nk)≤nk\binom nk\le n^k candidates.

    Concept map
    2 concepts; 4 descendants 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 candidate_complete proven

    2 candidate_count proven

    3 search_correct proven

    Lean source view on GitHub

    1import Lax263307.LinearRelaxation
    2import Mathlib.Data.List.FinRange
    3import Mathlib.Data.List.Sublists
    4
    5/-!
    6---
    7title: Exhaustive search for small independent-set targets
    8type: theorem
    9---
    10For a small target kk, enumerate exactly the kk-element vertex sets and
    11test independence. The first success has size exactly kk. If the search
    12fails, every independent set has size less than kk. There are exactly
    13(nk)≤nk\binom nk\le n^k candidates.
    14
    15# Formalization notes
    16
    17The executable enumeration generates sublists of length kk, without
    18materializing all vertex subsets. The candidate count is separate from
    19the eventual RAM instruction bound.
    20
    21# Attribution
    22
    23Bonnet–Chang, the small-target branch of Algorithm 1.
    24-/
    25
    26namespace Lax263307.ExhaustiveTargets
    27
    28/-- Enumerate the vertex sets of one prescribed cardinality. -/
    29def candidates (n k : ℕ) : List (Finset (Fin n)) :=
    30 ((List.finRange n).sublistsLen k).map List.toFinset
    31
    32/-- Deterministic exact search at target `k`. -/
    33def findIndependentSet {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    34 (k : ℕ) : Option (Finset (Fin n)) :=
    35 (candidates n k).find? fun I => decide (G.IsIndepSet (I : Set (Fin n)))
    36
    37/-- Every size-`k` vertex set occurs, and no other cardinality occurs. -/
    38axiom candidate_complete (n k : ℕ) (I : Finset (Fin n)) :
    39 I ∈ candidates n k ↔ I.card = k
    40
    41/-- Exact candidate count and its bound by a power of the graph order. -/
    42axiom candidate_count (n k : ℕ) :
    43 (candidates n k).length = n.choose k ∧ (candidates n k).length ≤ n ^ k
    44
    45/-- Search success is exact; search failure excludes every larger independent set. -/
    46axiom search_correct {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (k : ℕ) :
    47 match findIndependentSet G k with
    48 | some I => G.IsIndepSet (I : Set (Fin n)) ∧ I.card = k
    49 | none => ∀ J : Finset (Fin n), G.IsIndepSet (J : Set (Fin n)) → J.card < k
    50
    51end Lax263307.ExhaustiveTargets
    52
    Show ProofShow ProofShow Proof
    Formalization notes

    The executable enumeration generates sublists of length kk, without materializing all vertex subsets. The candidate count is separate from the eventual RAM instruction bound.

    Attribution

    Bonnet–Chang, the small-target branch of Algorithm 1.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…