Lax Lean Archive

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

Normalizing a long-code table to an odd table

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

    The Fourier analysis assumes A(−g)=−A(g)A(-g)=-A(g). This loses no accepting transcripts: repair every inconsistent pair of complementary coordinates by using evaluation at a fixed word. An accepting CNA transcript only queries consistent pairs, so all its answers are preserved. Acceptance and its side-condition extension are preserved as well.

    This justifies the normalization in footnote (4) preceding equation (2), including the strengthened test used for Theorem 4.17. Boolean negation represents sign negation.

    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 odd proven

    2 preserves_acceptance proven

    3 preserves_side_acceptance proven

    4 same_queries proven

    Lean source view on GitHub

    1import Lax253009.LongCode
    2
    3/-!
    4---
    5title: Normalizing a long-code table to an odd table
    6type: theorem
    7---
    8The Fourier analysis assumes A(−g)=−A(g)A(-g)=-A(g). This loses no accepting
    9transcripts: repair every inconsistent pair of complementary coordinates
    10by using evaluation at a fixed word. An accepting CNA transcript only
    11queries consistent pairs, so all its answers are preserved. Acceptance
    12and its side-condition extension are preserved as well.
    13
    14This justifies the normalization in footnote (4) preceding equation (2),
    15including the strengthened test used for Theorem 4.17. Boolean negation
    16represents sign negation.
    17-/
    18
    19namespace Lax253009.OddNormalization
    20
    21open LongCode
    22
    23def negate {w : ℕ} (g : Coordinate w) : Coordinate w := fun x ↦ !(g x)
    24
    25def oddify {w : ℕ} (x₀ : Word w) (A : Table w) : Table w :=
    26 fun g ↦ if A (negate g) = !(A g) then A g else g x₀
    27
    28axiom odd {w : ℕ} (x₀ : Word w) (A : Table w) (g : Coordinate w) :
    29 oddify x₀ A (negate g) = !(oddify x₀ A g)
    30
    31axiom same_queries {w s : ℕ} (x₀ : Word w) (A : Table w)
    32 (f : Fin s → Coordinate w) (hA : Accepts A f)
    33 (g : Coordinate w) (hg : Queried f g) : oddify x₀ A g = A g
    34
    35axiom preserves_acceptance {w s : ℕ} (x₀ : Word w) (A : Table w)
    36 (f : Fin s → Coordinate w) (hA : Accepts A f) :
    37 Accepts (oddify x₀ A) f
    38
    39axiom preserves_side_acceptance {w s : ℕ} (x₀ : Word w) (A : Table w)
    40 (f : Fin s → Coordinate w) (h : Coordinate w) (hA : AcceptsWithCondition A f h) :
    41 AcceptsWithCondition (oddify x₀ A) f h
    42
    43end Lax253009.OddNormalization
    44
    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…