Lax Lean Archive

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

Repetition of local proof tests

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

    Repeat a verifier kk times against the same global proof and accept only when every run accepts. Accepting local views are unions of compatible base views. The acceptance probability of each fixed proof is raised to the kkth power, and AA base accepting views give at most AkA^k repeated views per random choice. Perfect completeness is preserved.

    This is repetition of a one-oracle PCP verifier. It is distinct from the two-prover parallel-repetition theorem, whose strategies may depend on entire question tuples.

    Concept map
    12 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

    1 acceptance_probability proven

    2 free_bits proven

    3 passes_iff proven

    4 perfect_completeness proven

    5 soundness proven

    Lean source view on GitHub

    1import Lax253009.TestSampling
    2
    3/-!
    4---
    5title: Repetition of local proof tests
    6type: theorem
    7---
    8Repeat a verifier kk times against the same global proof and accept only
    9when every run accepts. Accepting local views are unions of compatible
    10base views. The acceptance probability of each fixed proof is raised to
    11the kkth power, and AA base accepting views give at most AkA^k repeated
    12views per random choice. Perfect completeness is preserved.
    13
    14This is repetition of a one-oracle PCP verifier. It is distinct from the
    15two-prover parallel-repetition theorem, whose strategies may depend on
    16entire question tuples.
    17-/
    18
    19namespace Lax253009.TestRepetition
    20
    21open LocalTests TestSampling FiniteProbability
    22
    23def Coherent {m k : ℕ} (a : Fin k → View m) : Prop :=
    24 ∀ i j, Compatible (a i) (a j)
    25
    26def merge {m : ℕ} : {k : ℕ} → (Fin k → View m) → View m
    27 | 0, _ => fun _ ↦ none
    28 | k + 1, a => fun i ↦ (a 0 i).or (merge (fun j : Fin k ↦ a j.succ) i)
    29
    30noncomputable def seedEquiv (r k : ℕ) : (Fin k → Fin r) ≃ Fin (r ^ k) :=
    31 Fintype.equivFinOfCardEq (by simp)
    32
    33noncomputable def repeated {r m : ℕ} (C : System r m) (k : ℕ) : System (r ^ k) m := by
    34 classical
    35 exact ⟨fun z ↦ ((Fintype.piFinset (fun i : Fin k ↦ C.accepting ((seedEquiv r k).symm z i))).filter
    36 Coherent).image merge⟩
    37
    38axiom passes_iff {r m : ℕ} (C : System r m) (k : ℕ) (π : Oracle m) (z : Fin (r ^ k)) :
    39 Passes (repeated C k) π z ↔ ∀ i, Passes C π ((seedEquiv r k).symm z i)
    40
    41axiom acceptance_probability {r m : ℕ} (C : System r m) (k : ℕ) (π : Oracle m) :
    42 probability (Passes (repeated C k) π) = probability (Passes C π) ^ k
    43
    44axiom free_bits {r m : ℕ} (C : System r m) (k A : ℕ)
    45 (hA : ∀ z, (C.accepting z).card ≤ A) :
    46 ∀ z, ((repeated C k).accepting z).card ≤ A ^ k
    47
    48axiom perfect_completeness {r m : ℕ} (C : System r m) (k : ℕ) (hC : Complete C) :
    49 Complete (repeated C k)
    50
    51axiom soundness {r m : ℕ} (C : System r m) (k : ℕ) (p : ℝ) (hp : 0 ≤ p)
    52 (hC : Sound C p) : Sound (repeated C k) (p ^ k)
    53
    54end Lax253009.TestRepetition
    55
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…