Lax Lean Archive

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

Encoding finite projection-game answers as binary words

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

    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 Lax253009.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 Lax253009.ProjectionEncoding
    17
    18open LongCode FiniteProbability
    19
    20noncomputable def decode {A B : Type} (e : A ↪ B) (b : B) : Option A := by
    21 classical
    22 exact if h : ∃ a, e a = b then some h.choose else none
    23
    24noncomputable def valid {U Ω Y : Type} {w : ℕ}
    25 (ey : Y ↪ Word w) (v : U → Ω → Y → Bool) (u : U) (ω : Ω) (b : Word w) : Bool :=
    26 match decode ey b with
    27 | some y => v u ω y
    28 | none => false
    29
    30noncomputable def project {U Ω X Y : Type} {u w : ℕ}
    31 (ex : X ↪ Word u) (ey : Y ↪ Word w) (ρ : U → Ω → Y → X)
    32 (v : U) (ω : Ω) (b : Word w) : Word u :=
    33 match decode ey b with
    34 | some y => ex (ρ v ω y)
    35 | none => fun _ ↦ false
    36
    37axiom encoding_exists {A : Type} [Fintype A] (w : ℕ) (h : Fintype.card A ≤ w) :
    38 Nonempty (A ↪ Word w)
    39
    40axiom completeness {U Ω W X Y : Type} {u w : ℕ}
    41 (ex : X ↪ Word u) (ey : Y ↪ Word w) (question : U → Ω → W)
    42 (v : U → Ω → Y → Bool) (ρ : U → Ω → Y → X)
    43 (P : W → Y) (Q : U → X)
    44 (hv : ∀ a ω, v a ω (P (question a ω)) = true)
    45 (hρ : ∀ a ω, ρ a ω (P (question a ω)) = Q a) :
    46 (∀ a ω, valid ey v a ω (ey (P (question a ω))) = true) ∧
    47 (∀ a ω, project ex ey ρ a ω (ey (P (question a ω))) = ex (Q a))
    48
    49axiom soundness {U Ω W X Y : Type} [Fintype U] [Fintype Ω]
    50 [Nonempty X] [Nonempty Y] {u w : ℕ}
    51 (ex : X ↪ Word u) (ey : Y ↪ Word w) (question : U → Ω → W)
    52 (v : U → Ω → Y → Bool) (ρ : U → Ω → Y → X) (s : ℝ)
    53 (h : ∀ (P : W → Y) (Q : U → X),
    54 probability (fun z : U × Ω ↦ v z.1 z.2 (P (question z.1 z.2)) = true ∧
    55 ρ z.1 z.2 (P (question z.1 z.2)) = Q z.1) ≤ s)
    56 (P : W → Option (Word w)) (Q : U → Option (Word u)) :
    57 probability (DecodedStrategies.Wins question
    58 (FAFStrategyExtraction.Relation (project ex ey ρ) (valid ey v)) P Q) ≤ s
    59
    60end Lax253009.ProjectionEncoding
    61
    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…