Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax47.Gap

Finite-Turing promise-gap algorithms for Max Independent Set

concepts/Lax47/Gap.lean · lax-47

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    The Håstad premise is stated only for functions certified by Lax51's genuine finite-Turing polynomial-time predicate. A randomized program fixes constants c,kc,k and receives exactly c(n+1)kc(n+1)^k uniform bits on an nn-vertex input. There is no special constructor for the reduction and no detached step annotation. For an integer q>2q>2, the high promise is n1−1/q≤α(H)n^{1-1/q}\leq\alpha(H), the low promise is α(H)≤n1/q\alpha(H)\leq n^{1/q}, and the acceptance threshold is nq+3≤∣S∣qn^{q+3}\leq |S|^q.

    Lean source view on GitHub

    1import Lax47.Complexity
    2
    3/-!
    4---
    5title: Finite-Turing promise-gap algorithms for Max Independent Set
    6type: definition
    7---
    8The Håstad premise is stated only for functions certified by Lax51's genuine
    9finite-Turing polynomial-time predicate. A randomized program fixes constants
    10c,kc,k and receives exactly c(n+1)kc(n+1)^k uniform bits on an nn-vertex input.
    11There is no special constructor for the reduction and no detached step
    12annotation. For an integer q>2q>2, the high promise is
    13n1−1/q≤α(H)n^{1-1/q}\leq\alpha(H), the low promise is
    14α(H)≤n1/q\alpha(H)\leq n^{1/q}, and the acceptance threshold is
    15nq+3≤∣S∣qn^{q+3}\leq |S|^q.
    16-/
    17
    18set_option autoImplicit false
    19
    20namespace Lax47.Gap
    21
    22open Lax47.Machine Lax47.Complexity
    23
    24/- ### Standard randomized finite-Turing programs -/
    25
    26/-- A polynomial-time finite-Turing program with one fixed monomial tape bound. -/
    27structure GapProgram (q : ℕ) where
    28 program : PolytimeProgram
    29 randomnessConstant : ℕ
    30 randomnessExponent : ℕ
    31 randomnessConstant_pos : 0 < randomnessConstant
    32
    33/-- The exact, uniformly specified random-tape length on order nn. -/
    34def GapProgram.randomBitCount {q : ℕ} (program : GapProgram q) (n : ℕ) : ℕ :=
    35 polynomialBound program.randomnessConstant program.randomnessExponent n
    36
    37/-- Finite uniform seed type read by a gap program on an nn-vertex graph. -/
    38abbrev GapProgram.Seed {q : ℕ} (program : GapProgram q) (n : ℕ) :=
    39 RandomSeed (program.randomBitCount n)
    40
    41/-- Boolean answer returned by the program's certified Turing computation. -/
    42def GapProgram.accepts {q : ℕ} (program : GapProgram q) (n : ℕ)
    43 (input : GraphCode n) (seed : program.Seed n) : Bool :=
    44 decide (program.program.output (pairBits input.bits seed.bits) = [1])
    45
    46/-- Uniform seed enumeration for a finite-Turing program. -/
    47def GapProgram.seeds {q : ℕ} (program : GapProgram q) (n : ℕ) :
    48 Finset (program.Seed n) :=
    49 Finset.univ
    50
    51/-- Seeds on which the finite-Turing program returns true. -/
    52def GapProgram.acceptingSeeds {q : ℕ} (program : GapProgram q)
    53 (n : ℕ) (input : GraphCode n) : Finset (program.Seed n) :=
    54 (program.seeds n).filter fun seed ↦ program.accepts n input seed
    55
    56/- ### Certified polynomial gap solvers -/
    57
    58/--
    59A bounded-error finite-Turing polynomial-time solver for Håstad's rational
    60promise gap. The uniform random-tape length is the fixed monomial stored in
    61the gap program.
    62-/
    63structure MISGapSolver (q : ℕ) where
    64 program : GapProgram q
    65 cutoff : ℕ
    66 completeness : ∀ (n : ℕ), cutoff ≤ n → ∀ input : GraphCode n,
    67 Real.rpow n (1 - (q : ℝ)⁻¹) ≤ (input.graph.indepNum : ℝ) →
    68 2 * (program.seeds n).card ≤
    69 3 * (program.acceptingSeeds n input).card
    70 soundness : ∀ (n : ℕ), cutoff ≤ n → ∀ input : GraphCode n,
    71 (input.graph.indepNum : ℝ) ≤ Real.rpow n ((q : ℝ)⁻¹) →
    72 3 * (program.acceptingSeeds n input).card ≤
    73 (program.seeds n).card
    74
    75end Lax47.Gap
    76

    Builds on

    Used by

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…