Finite-Turing promise-gap algorithms for Max Independent Set
Lax47.Gap · concepts/Lax47/Gap.lean · lax-47
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The Håstad premise is stated only for functions certified by Lax759944's genuine finite-Turing polynomial-time predicate. A randomized program fixes constants and receives exactly uniform bits on an -vertex input. There is no special constructor for the reduction and no detached step annotation. For an integer , the high promise is , the low promise is , and the acceptance threshold is .
Concept map
Lean source view on GitHub
| 1 | import Lax47.Complexity |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Finite-Turing promise-gap algorithms for Max Independent Set |
| 6 | type: definition |
| 7 | --- |
| 8 | The Håstad premise is stated only for functions certified by Lax759944's genuine |
| 9 | finite-Turing polynomial-time predicate. A randomized program fixes constants |
| 10 | and receives exactly uniform bits on an -vertex input. |
| 11 | There is no special constructor for the reduction and no detached step |
| 12 | annotation. For an integer , the high promise is |
| 13 | , the low promise is |
| 14 | , and the acceptance threshold is |
| 15 | . |
| 16 | -/ |
| 17 | |
| 18 | set_option autoImplicit false |
| 19 | |
| 20 | namespace Lax47.Gap |
| 21 | |
| 22 | open 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. -/ |
| 27 | structure 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 . -/ |
| 34 | def 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 -vertex graph. -/ |
| 38 | abbrev GapProgram.Seed {q : ℕ} (program : GapProgram q) (n : ℕ) := |
| 39 | RandomSeed (program.randomBitCount n) |
| 40 | |
| 41 | /-- Boolean answer returned by the program's certified Turing computation. -/ |
| 42 | def 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. -/ |
| 47 | def 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. -/ |
| 52 | def 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 | /-- |
| 59 | A bounded-error finite-Turing polynomial-time solver for Håstad's rational |
| 60 | promise gap. The uniform random-tape length is the fixed monomial stored in |
| 61 | the gap program. |
| 62 | -/ |
| 63 | structure 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 | |
| 75 | end Lax47.Gap |
| 76 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments