Lax Lean Archive

Free bits of the complete nonadaptive test

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

    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 Lax323828.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 Lax323828.LongCodePatterns
    22
    23open scoped Classical
    24
    25open LongCode
    26
    27/-- A partial Boolean answer table; `none` marks an unqueried coordinate. -/
    28abbrev Pattern (w : ℕ) := Coordinate w → Option Bool
    29
    30/-- Record the table answers on the queried coordinates and leave the others unspecified. -/
    31noncomputable def restrict {w : ℕ} (Q : Coordinate w → Prop) (A : Table w) :
    32 Pattern w :=
    33 fun g ↦ if Q g then some (A g) else none
    34
    35/-- All queried answer patterns arising from accepting tables. -/
    36noncomputable def patterns {w s : ℕ} (f : Fin s → Coordinate w) : Finset (Pattern w) :=
    37 (Finset.univ.filter (fun A : Table w ↦ Accepts A f)).image (restrict (Queried f))
    38
    39/-- A coordinate queried by the test or forced by agreement on the side condition. -/
    40def SideQueried {w s : ℕ} (f : Fin s → Coordinate w) (h g' : Coordinate w) : Prop :=
    41 ∃ g, Queried f g ∧ AgreesOn h g g'
    42
    43/-- All queried answer patterns arising from tables accepted with the side condition. -/
    44noncomputable def sidePatterns {w s : ℕ} (f : Fin s → Coordinate w)
    45 (h : Coordinate w) : Finset (Pattern w) :=
    46 (Finset.univ.filter (fun A : Table w ↦ AcceptsWithCondition A f h)).image
    47 (restrict (SideQueried f h))
    48
    49axiom free_bits {w s : ℕ} (f : Fin s → Coordinate w) :
    50 (patterns f).card ≤ 2 ^ s
    51
    52axiom side_free_bits {w s : ℕ} (f : Fin s → Coordinate w) (h : Coordinate w) :
    53 (sidePatterns f h).card ≤ 2 ^ s
    54
    55end Lax323828.LongCodePatterns
    56
    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…