Lax Lean Archive

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

Small-value projection games for every registered NP language

Lax253009.SmallValueNP · concepts/Lax253009/SmallValueNP.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

    Every language in the registered certificate definition of NP has a polynomial-size reduction to projection games of arbitrarily small positive value. The answer alphabets depend only on the target value. The polynomial bound can depend on the language. Completeness is perfect.

    The proof connects the registered stack-machine verifiers to Cook–Levin, then applies the proved finite gap and fortification construction. This statement records semantic correctness and size; the machine implementation of the complete game transformation is a separate obligation.

    Concept map
    13 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.SmallValueSatisfiability
    2import Lax434930.NondeterministicPolynomialTime
    3
    4/-!
    5---
    6title: Small-value projection games for every registered NP language
    7type: theorem
    8---
    9Every language in the registered certificate definition of NP has a
    10polynomial-size reduction to projection games of arbitrarily small positive
    11value. The answer alphabets depend only on the target value. The polynomial
    12bound can depend on the language. Completeness is perfect.
    13
    14The proof connects the registered stack-machine verifiers to Cook–Levin,
    15then applies the proved finite gap and fortification construction. This
    16statement records semantic correctness and size; the machine implementation
    17of the complete game transformation is a separate obligation.
    18-/
    19
    20namespace Lax253009.SmallValueNP
    21
    22open CenteredProjection
    23
    24axiom reduction (δ : ℝ) (hδ : 0 < δ) :
    25 ∃ x y : ℕ, 0 < x ∧ 0 < y ∧
    26 ∀ L ∈ Lax434930.NondeterministicPolynomialTime.NP, ∃ K e : ℕ,
    27 ∀ z : List Bool,
    28 ∃ u o w : ℕ, 0 < u ∧ 0 < o ∧ 0 < w ∧ u + o + w ≤ K * (z.length + 1) ^ e ∧
    29 ∃ G : System (Fin u) (Fin o) (Fin w) (Fin x) (Fin y),
    30 (z ∈ L → G.Complete) ∧ (z ∉ L → G.Sound δ)
    31
    32end Lax253009.SmallValueNP
    33
    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…