Lax Lean Archive

Perfect completeness and local decoding of the long-code test

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

    Every genuine long code passes the complete nonadaptive test. Conversely, whenever the test accepts, all its answers agree with evaluation at one word. This is Lemma 4.1 of Håstad's paper; it concerns a fixed run and does not assert global closeness of the table to a long code.

    A genuine code also passes the extended test whenever its encoded word satisfies the side condition. Any accepting extended run has a compatible evaluation point satisfying the condition. The latter is a local statement, distinct from the probabilistic bound and the fixed small decoding set in Theorem 4.17.

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

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

    1 local_decoding proven

    2 perfect_completeness proven

    3 side_condition_completeness proven

    4 side_condition_decoding proven

    Lean source view on GitHub

    1import Lax323828.LongCode
    2
    3/-!
    4---
    5title: Perfect completeness and local decoding of the long-code test
    6type: theorem
    7---
    8Every genuine long code passes the complete nonadaptive test. Conversely,
    9whenever the test accepts, all its answers agree with evaluation at one
    10word. This is Lemma 4.1 of Håstad's paper; it concerns a fixed run and does
    11not assert global closeness of the table to a long code.
    12
    13A genuine code also passes the extended test whenever its encoded word
    14satisfies the side condition. Any accepting extended run has a compatible
    15evaluation point satisfying the condition. The latter is a local statement,
    16distinct from the probabilistic bound and the fixed small decoding set in
    17Theorem 4.17.
    18-/
    19
    20namespace Lax323828.LongCodeCorrectness
    21
    22open LongCode
    23
    24axiom perfect_completeness {w s : ℕ} (x : Word w) (f : Fin s → Coordinate w) :
    25 Accepts (evaluation x) f
    26
    27axiom local_decoding {w s : ℕ} (A : Table w) (f : Fin s → Coordinate w)
    28 (h : Accepts A f) :
    29 ∃ x : Word w, LooksLike A f x
    30
    31axiom side_condition_completeness {w s : ℕ} (x : Word w) (f : Fin s → Coordinate w)
    32 (h : Coordinate w) (hx : h x = true) :
    33 AcceptsWithCondition (evaluation x) f h
    34
    35axiom side_condition_decoding {w s : ℕ} (A : Table w) (f : Fin s → Coordinate w)
    36 (h : Coordinate w) (haccept : AcceptsWithCondition A f h) :
    37 ∃ x : Word w, h x = true ∧ LooksLike A f x
    38
    39end Lax323828.LongCodeCorrectness
    40
    Show ProofShow 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…