Lax Lean Archive

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

Extracting prover strategies from decoded sets

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

    A question uu for the second prover and a random extension ω\omega determine the first prover's question. Each first question has a set of at most BB decoded answers. Call a second question common when some answer is compatible with one of the decoded answers with probability at least pp over extensions.

    There are deterministic prover strategies whose success probability is at least Pr⁡[common]p/(B+1)\Pr[\mathrm{common}]p/(B+1). The first strategy depends only on its own question, even when several extensions produce the same question. An explicit failure answer handles empty decoding sets. This is the rounding step in Lemma 5.5, with a harmless extra unit in the denominator.

    Concept map
    2 concepts; 11 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax253009.FiniteProbability
    2import Mathlib.Data.Fintype.Pi
    3import Mathlib.Data.Fintype.Option
    4
    5/-!
    6---
    7title: Extracting prover strategies from decoded sets
    8type: theorem
    9---
    10A question uu for the second prover and a random extension ω\omega
    11determine the first prover's question. Each first question has a set of
    12at most BB decoded answers. Call a second question common when some
    13answer is compatible with one of the decoded answers with probability
    14at least pp over extensions.
    15
    16There are deterministic prover strategies whose success probability is at
    17least Pr⁡[common]p/(B+1)\Pr[\mathrm{common}]p/(B+1). The first strategy depends only on its
    18own question, even when several extensions produce the same question.
    19An explicit failure answer handles empty decoding sets. This is the
    20rounding step in Lemma 5.5, with a harmless extra unit in the denominator.
    21-/
    22
    23namespace Lax253009.DecodedStrategies
    24
    25open FiniteProbability
    26
    27def Common {U Ω W X Y : Type} [Fintype Ω]
    28 (question : U → Ω → W) (V : U → Ω → Y → X → Prop)
    29 (D : W → Finset Y) (p : ℝ) (u : U) : Prop :=
    30 ∃ x, p ≤ probability (fun ω ↦ ∃ y ∈ D (question u ω), V u ω y x)
    31
    32def Wins {U Ω W X Y : Type}
    33 (question : U → Ω → W) (V : U → Ω → Y → X → Prop)
    34 (P : W → Option Y) (Q : U → Option X) (z : U × Ω) : Prop :=
    35 ∃ y x, P (question z.1 z.2) = some y ∧ Q z.1 = some x ∧ V z.1 z.2 y x
    36
    37axiom extract_strategies {U Ω W X Y : Type}
    38 [Fintype U] [Nonempty U] [Fintype Ω] [Nonempty Ω]
    39 [Fintype W] [DecidableEq W] [Fintype X] [Fintype Y]
    40 (question : U → Ω → W) (V : U → Ω → Y → X → Prop)
    41 (D : W → Finset Y) (B : ℕ) (hB : ∀ w, (D w).card ≤ B)
    42 (p : ℝ) (hp : 0 ≤ p) :
    43 ∃ P : W → Option Y, ∃ Q : U → Option X,
    44 probability (Common question V D p) * p / (B + 1) ≤ probability (Wins question V P Q)
    45
    46end Lax253009.DecodedStrategies
    47
    Show 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…