Lax Lean Archive

Encoding finite projection-game answers as binary words

Lax323828.ProjectionEncoding · concepts/Lax323828/ProjectionEncoding.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

    Inject finite answer alphabets into fixed-length Boolean words, reject invalid first-prover encodings, and project valid answers through the encoding of the second alphabet. This preserves perfect completeness and cannot increase soundness, including for partial prover strategies. The first answer width can be enlarged arbitrarily without changing either property, as required by the FAF composition's minimum-width condition.

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

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

    1 completeness proven

    2 encoding_exists proven

    3 soundness proven

    Lean source view on GitHub

    1import Lax323828.FAFStrategyExtraction
    2
    3/-!
    4---
    5title: Encoding finite projection-game answers as binary words
    6type: theorem
    7---
    8Inject finite answer alphabets into fixed-length Boolean words, reject
    9invalid first-prover encodings, and project valid answers through the
    10encoding of the second alphabet. This preserves perfect completeness and
    11cannot increase soundness, including for partial prover strategies.
    12The first answer width can be enlarged arbitrarily without changing either
    13property, as required by the FAF composition's minimum-width condition.
    14-/
    15
    16namespace Lax323828.ProjectionEncoding
    17
    18open scoped Classical
    19
    20open LongCode FiniteProbability
    21
    22/-- Recover the unique encoded letter if `b` lies in the image of `e`; otherwise return no letter. -/
    23noncomputable def decode {A B : Type} (e : A ↪ B) (b : B) : Option A :=
    24 if h : ∃ a, e a = b then some h.choose else none
    25
    26/-- Accept precisely the encodings of letters that satisfy the original validity test. -/
    27noncomputable def valid {U Ω Y : Type} {w : ℕ}
    28 (ey : Y ↪ Word w) (v : U → Ω → Y → Bool) (u : U) (ω : Ω) (b : Word w) : Bool :=
    29 match decode ey b with
    30 | some y => v u ω y
    31 | none => false
    32
    33/-- Decode the first answer, apply the projection, and encode the second answer; invalid words map to the zero word. -/
    34noncomputable def project {U Ω X Y : Type} {u w : ℕ}
    35 (ex : X ↪ Word u) (ey : Y ↪ Word w) (ρ : U → Ω → Y → X)
    36 (v : U) (ω : Ω) (b : Word w) : Word u :=
    37 match decode ey b with
    38 | some y => ex (ρ v ω y)
    39 | none => fun _ ↦ false
    40
    41axiom encoding_exists {A : Type} [Fintype A] (w : ℕ) (h : Fintype.card A ≤ w) :
    42 Nonempty (A ↪ Word w)
    43
    44axiom completeness {U Ω W X Y : Type} {u w : ℕ}
    45 (ex : X ↪ Word u) (ey : Y ↪ Word w) (question : U → Ω → W)
    46 (v : U → Ω → Y → Bool) (ρ : U → Ω → Y → X)
    47 (P : W → Y) (Q : U → X)
    48 (hv : ∀ a ω, v a ω (P (question a ω)) = true)
    49 (hρ : ∀ a ω, ρ a ω (P (question a ω)) = Q a) :
    50 (∀ a ω, valid ey v a ω (ey (P (question a ω))) = true) ∧
    51 (∀ a ω, project ex ey ρ a ω (ey (P (question a ω))) = ex (Q a))
    52
    53axiom soundness {U Ω W X Y : Type} [Fintype U] [Fintype Ω]
    54 [Nonempty X] [Nonempty Y] {u w : ℕ}
    55 (ex : X ↪ Word u) (ey : Y ↪ Word w) (question : U → Ω → W)
    56 (v : U → Ω → Y → Bool) (ρ : U → Ω → Y → X) (s : ℝ)
    57 (h : ∀ (P : W → Y) (Q : U → X),
    58 probability (fun z : U × Ω ↦ v z.1 z.2 (P (question z.1 z.2)) = true ∧
    59 ρ z.1 z.2 (P (question z.1 z.2)) = Q z.1) ≤ s)
    60 (P : W → Option (Word w)) (Q : U → Option (Word u)) :
    61 probability (DecodedStrategies.Wins question
    62 (FAFStrategyExtraction.Relation (project ex ey ρ) (valid ey v)) P Q) ≤ s
    63
    64end Lax323828.ProjectionEncoding
    65
    Show ProofShow ProofShow 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…