Lax Lean Archive

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

Randomized promise-gap algorithms for Max Independent Set

Lax253009.IndependentSetGap · concepts/Lax253009/IndependentSetGap.lean · lax-253009

definition

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

    Definition

    A randomized polynomial-time algorithm distinguishes graphs with independence number at most n1/qn^{1/q} from graphs with independence number at least n1−1/qn^{1-1/q}, with error at most 1/31/3 on either promise. The guarantee may start at a fixed input-size cutoff.

    The algorithm is a fixed finite Turing machine, certified polynomial-time by lax-759944. Its input is a pair of natural-number words: the vertex count followed by the row-major adjacency matrix, and exactly c(n+1)kc(n+1)^k independent uniform bits. The pair is prefixed by the length of its first word. These words use the canonical binary encoding of lax-759944. The constants and the machine are fixed before the input graph is chosen.

    Concept map
    4 concepts; 1 descendant hidden
    100%
    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax253009.Graphs
    2import Lax759944.TuringPolytime
    3import Mathlib.Analysis.SpecialFunctions.Pow.Real
    4
    5/-!
    6---
    7title: Randomized promise-gap algorithms for Max Independent Set
    8type: definition
    9---
    10A randomized polynomial-time algorithm distinguishes graphs with independence
    11number at most n1/qn^{1/q} from graphs with independence number at least
    12n1−1/qn^{1-1/q}, with error at most 1/31/3 on either promise. The guarantee may
    13start at a fixed input-size cutoff.
    14
    15The algorithm is a fixed finite Turing machine, certified polynomial-time
    16by lax-759944. Its input is a pair of natural-number words: the vertex count
    17followed by the row-major adjacency matrix, and exactly c(n+1)kc(n+1)^k independent
    18uniform bits. The pair is prefixed by the length of its first word. These
    19words use the canonical binary encoding of lax-759944. The constants and
    20the machine are fixed before the input graph is chosen.
    21-/
    22
    23namespace Lax253009.IndependentSetGap
    24
    25open Graphs Lax759944.TuringPolytime
    26
    27/-- Vertex count followed by the complete row-major adjacency matrix. -/
    28def graphWord {n : ℕ} (G : Graph n) : List ℕ :=
    29 n :: List.ofFn fun rank : Fin (n * n) ↦
    30 let vertex := finProdFinEquiv.symm rank
    31 if G.adjacent vertex.1 vertex.2 then 1 else 0
    32
    33/-- A uniform tape of exactly `r` independent bits. -/
    34abbrev Seed (r : ℕ) := Fin r → Bool
    35
    36def seedWord {r : ℕ} (seed : Seed r) : List ℕ :=
    37 (List.ofFn seed).map fun bit ↦ if bit then 1 else 0
    38
    39def pairWords (left right : List ℕ) : List ℕ :=
    40 left.length :: left ++ right
    41
    42/-- One polynomial-time machine with a fixed polynomial random-tape bound. -/
    43structure Program where
    44 function : List ℕ → List ℕ
    45 polytime : TuringPolytime function
    46 randomnessConstant : ℕ
    47 randomnessExponent : ℕ
    48 randomnessConstant_pos : 0 < randomnessConstant
    49
    50def Program.randomBitCount (program : Program) (n : ℕ) : ℕ :=
    51 program.randomnessConstant * (n + 1) ^ program.randomnessExponent
    52
    53abbrev Program.Seed (program : Program) (n : ℕ) :=
    54 IndependentSetGap.Seed (program.randomBitCount n)
    55
    56def Program.accepts (program : Program) (n : ℕ)
    57 (G : Graph n) (seed : program.Seed n) : Bool :=
    58 decide (program.function (pairWords (graphWord G) (seedWord seed)) = [1])
    59
    60def Program.seeds (program : Program) (n : ℕ) : Finset (program.Seed n) :=
    61 Finset.univ
    62
    63def Program.acceptingSeeds (program : Program) (n : ℕ) (G : Graph n) :
    64 Finset (program.Seed n) :=
    65 (program.seeds n).filter fun seed ↦ program.accepts n G seed
    66
    67/-- A bounded-error polynomial-time solver for the rational Independent Set gap. -/
    68structure Solver (q : ℕ) where
    69 program : Program
    70 cutoff : ℕ
    71 completeness : ∀ n : ℕ, cutoff ≤ n → ∀ G : Graph n,
    72 Real.rpow n (1 - (q : ℝ)⁻¹) ≤ (G.simpleGraph.indepNum : ℝ) →
    73 2 * (program.seeds n).card ≤ 3 * (program.acceptingSeeds n G).card
    74 soundness : ∀ n : ℕ, cutoff ≤ n → ∀ G : Graph n,
    75 (G.simpleGraph.indepNum : ℝ) ≤ Real.rpow n ((q : ℝ)⁻¹) →
    76 3 * (program.acceptingSeeds n G).card ≤ (program.seeds n).card
    77
    78end Lax253009.IndependentSetGap
    79
    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…