Lax Lean Archive

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

The complete finite game-to-clique construction

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

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 any positive approximation exponent, choose fixed FAF and sampling parameters before the game question spaces or the input instance. The FAF composition, local-view construction, repetition, and randomized sparsification then yield a clique decision rule with perfect completeness. Explicit sampling from a fixed vector of fair bits gives false-positive probability at most 1/31/3 on sufficiently sound games.

    The sampled graph has polynomially many vertices in the proof length, with explicit degree and constant. Its base proof length is linear in the game question counts for fixed answer widths. This completes the finite mathematical transfer from a small-value projection game. Constructing that game from the registered NP machine model and proving polynomial-time implementations are still required for Håstad's theorem. The finite regular 3-SAT gap and soundness amplification are proved in the companion concepts.

    Concept map
    26 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax253009.FAFLocalTests
    2import Lax253009.RandomizedReduction
    3
    4/-!
    5---
    6title: The complete finite game-to-clique construction
    7type: theorem
    8---
    9For any positive approximation exponent, choose fixed FAF and sampling
    10parameters before the game question spaces or the input instance. The
    11FAF composition, local-view construction, repetition, and randomized
    12sparsification then yield a clique decision rule with perfect completeness.
    13Explicit sampling from a fixed vector of fair bits gives false-positive
    14probability at most 1/31/3 on sufficiently sound games.
    15
    16The sampled graph has polynomially many vertices in the proof length, with
    17explicit degree and constant. Its base proof length is linear in the game
    18question counts for fixed answer widths. This completes the finite
    19mathematical transfer from a small-value projection game. Constructing that
    20game from the registered NP machine model and proving polynomial-time
    21implementations are still required for Håstad's theorem. The finite regular
    223-SAT gap and soundness amplification are proved in the companion concepts.
    23-/
    24
    25namespace Lax253009.GameToClique
    26
    27open LocalTests ConsistencyGraph TestSampling SamplingParameters FiniteProbability
    28open Lax434930.PolynomialTime
    29
    30axiom reduction (ε : ℝ) (hε : 0 < ε) (happrox : Approximation.Approximable ε) :
    31 ∃ estimate : Word → ℕ,
    32 Nonempty (Turing.TM2ComputableInPolyTime id Computability.encodeNat estimate) ∧
    33 ∃ l s c w₀ : ℕ, 0 < l ∧ 0 < s ∧ 0 < c ∧
    34 ∀ w : ℕ, w₀ ≤ w →
    35 ∀ {U Ω W : Type} [Fintype U] [Nonempty U] [Fintype Ω] [Nonempty Ω]
    36 [Fintype W] [DecidableEq W],
    37 ∀ u : ℕ, ∀ (question : U → Ω → W)
    38 (ρ : U → Ω → LongCode.Word w → LongCode.Word u) (valid : U → Ω → LongCode.Coordinate w),
    39 let C := FAFLocalTests.system (n := 10 * l) (s := s) (q := 10 * l * s) question ρ valid
    40 let m := Fintype.card (FAFLocalTests.Index U W u w)
    41 let k := repetitions c m
    42 (∀ (P : W → LongCode.Word w) (Q : U → LongCode.Word u),
    43 (∀ v ω, valid v ω (P (question v ω)) = true) →
    44 (∀ v ω, ρ v ω (P (question v ω)) = Q v) →
    45 ∀ coins, RandomizedReduction.CoinAccept estimate C (by exact Fintype.card_pos)
    46 (20 * l * l * s) k coins) ∧
    47 ((∀ (P : W → Option (LongCode.Word w)) (Q : U → Option (LongCode.Word u)),
    48 probability (DecodedStrategies.Wins question (FAFStrategyExtraction.Relation ρ valid) P Q) <
    49 FAFComposition.gameThreshold l s) →
    50 probability (RandomizedReduction.CoinAccept estimate C (by exact Fintype.card_pos)
    51 (20 * l * l * s) k) ≤ 1 / 3) ∧
    52 (∀ z, Fintype.card (Vertex (RandomizedReduction.tests C (20 * l * l * s) k z)) ≤
    53 16 ^ ((20 * l * l * s + 20 * l * s) * c) *
    54 (m + 2) ^ ((20 * l * l * s + 20 * l * s) * c + 1))
    55
    56end Lax253009.GameToClique
    57
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…