Lax Lean Archive

The averaged table preserves the answers of an accepting side-condition test

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

    Let UU be the words satisfying the side condition hh. If the extended CNA test accepts a table AA, then averaging its sign-valued version over coordinates outside UU preserves every base query answer of that run. Indeed, step (3) requires the table to have the same answer on every function agreeing with the query on UU.

    This links the actual test definition to the averaged function in equation (17) and to its Fourier projection formula, Lemma 4.18.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax323828.LongCode
    2import Lax323828.FourierProjection
    3
    4/-!
    5---
    6title: The averaged table preserves the answers of an accepting side-condition test
    7type: theorem
    8---
    9Let UU be the words satisfying the side condition hh. If the extended
    10CNA test accepts a table AA, then averaging its sign-valued version over
    11coordinates outside UU preserves every base query answer of that run.
    12Indeed, step (3) requires the table to have the same answer on every
    13function agreeing with the query on UU.
    14
    15This links the actual test definition to the averaged function in equation
    16(17) and to its Fourier projection formula, Lemma 4.18.
    17-/
    18
    19namespace Lax323828.SideConditionAveraging
    20
    21open LongCode BooleanFourier FourierProjection
    22
    23def satisfying {w : ℕ} (h : Coordinate w) : Finset (Word w) :=
    24 Finset.univ.filter fun x ↦ h x = true
    25
    26axiom query_preserved {w s : ℕ} (A : Table w) (f : Fin s → Coordinate w)
    27 (h : Coordinate w) (hpass : AcceptsWithCondition A f h)
    28 (g : Coordinate w) (hg : Queried f g) :
    29 project (fun q ↦ sign (A q)) (satisfying h) g = sign (A g)
    30
    31end Lax323828.SideConditionAveraging
    32
    Show 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…