Lax Lean Archive

Repetition of local proof tests

Lax323828.TestRepetition · concepts/Lax323828/TestRepetition.lean · lax-323828

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

    Discussion

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

    Loading discussion…