Lax Lean Archive

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

Free bits of the complete nonadaptive test

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

    For fixed random functions, record an accepting table only at queried coordinates, leaving other coordinates unspecified. There are at most 2s2^s distinct such answer patterns. The same bound holds when all the queries imposed by a side condition are included. Thus the CNA test and its extension both use at most ss free bits.

    Patterns are explicitly enumerated as restrictions of accepting tables. The bound counts distinct patterns, not distinct tables: the unqueried entries of a table can be arbitrary.

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

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

    1 free_bits proven

    2 side_free_bits proven

    Lean source view on GitHub

    1import Lax253009.LongCode
    2import Mathlib.Data.Fintype.Option
    3import Mathlib.Data.Finset.Card
    4
    5/-!
    6---
    7title: Free bits of the complete nonadaptive test
    8type: theorem
    9---
    10For fixed random functions, record an accepting table only at queried
    11coordinates, leaving other coordinates unspecified. There are at most
    122s2^s distinct such answer patterns. The same bound holds when all the
    13queries imposed by a side condition are included. Thus the CNA test and
    14its extension both use at most ss free bits.
    15
    16Patterns are explicitly enumerated as restrictions of accepting tables.
    17The bound counts distinct patterns, not distinct tables: the unqueried
    18entries of a table can be arbitrary.
    19-/
    20
    21namespace Lax253009.LongCodePatterns
    22
    23open LongCode
    24
    25abbrev Pattern (w : ℕ) := Coordinate w → Option Bool
    26
    27noncomputable def restrict {w : ℕ} (Q : Coordinate w → Prop) (A : Table w) :
    28 Pattern w := by
    29 classical
    30 exact fun g ↦ if Q g then some (A g) else none
    31
    32noncomputable def patterns {w s : ℕ} (f : Fin s → Coordinate w) : Finset (Pattern w) := by
    33 classical
    34 exact (Finset.univ.filter (fun A : Table w ↦ Accepts A f)).image (restrict (Queried f))
    35
    36def SideQueried {w s : ℕ} (f : Fin s → Coordinate w) (h g' : Coordinate w) : Prop :=
    37 ∃ g, Queried f g ∧ AgreesOn h g g'
    38
    39noncomputable def sidePatterns {w s : ℕ} (f : Fin s → Coordinate w)
    40 (h : Coordinate w) : Finset (Pattern w) := by
    41 classical
    42 exact (Finset.univ.filter (fun A : Table w ↦ AcceptsWithCondition A f h)).image
    43 (restrict (SideQueried f h))
    44
    45axiom free_bits {w s : ℕ} (f : Fin s → Coordinate w) :
    46 (patterns f).card ≤ 2 ^ s
    47
    48axiom side_free_bits {w s : ℕ} (f : Fin s → Coordinate w) (h : Coordinate w) :
    49 (sidePatterns f h).card ≤ 2 ^ s
    50
    51end Lax253009.LongCodePatterns
    52
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…