Lax Lean Archive

Free bits of the FAF test

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

    The accepting transcripts of the FAF test use at most q+nsq+ns free bits: qq reference answers, followed by at most ss free bits in each of the nn CNA tests. The side-condition queries are determined by the reference answers. Setting n=10ℓn=10\ell and q=10ℓsq=10\ell s gives Lemma 5.4's bound of 20ℓs20\ell s free bits.

    We enumerate a finite superset of accepting transcripts. This allows repeated sampled tables to be treated independently for the upper bound; every transcript produced by an actual accepting oracle is included.

    Concept map
    7 concepts; 3 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 transcript_mem proven

    Lean source view on GitHub

    1import Lax323828.FAFTest
    2import Lax323828.LongCodePatterns
    3
    4/-!
    5---
    6title: Free bits of the FAF test
    7type: theorem
    8---
    9The accepting transcripts of the FAF test use at most q+nsq+ns free bits:
    10qq reference answers, followed by at most ss free bits in each of the
    11nn CNA tests. The side-condition queries are determined by the reference
    12answers. Setting n=10ℓn=10\ell and q=10ℓsq=10\ell s gives Lemma 5.4's bound
    13of 20ℓs20\ell s free bits.
    14
    15We enumerate a finite superset of accepting transcripts. This allows
    16repeated sampled tables to be treated independently for the upper bound;
    17every transcript produced by an actual accepting oracle is included.
    18-/
    19
    20namespace Lax323828.FAFPatterns
    21
    22open scoped Classical
    23
    24open LongCode LongCodePatterns
    25
    26/-- The side condition on a larger-table word: validity and agreement with all reference answers. -/
    27noncomputable def conditionOfAnswers {Ω : Type} {u w q : ℕ}
    28 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    29 (ω : Ω) (g : Fin q → Coordinate u) (b : Word q) : Coordinate w :=
    30 fun y ↦ valid ω y && decide (∀ j, g j (ρ ω y) = b j)
    31
    32/-- All reference answer strings paired with one permissible partial pattern for each sampled larger table. -/
    33noncomputable def patterns {Ω : Type} {u w n s q : ℕ}
    34 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    35 (ω : Fin n → Ω) (g : Fin q → Coordinate u) (f : Fin n → Fin s → Coordinate w) :
    36 Finset (Word q × (Fin n → Pattern w)) :=
    37 Finset.univ.biUnion (fun b : Word q ↦
    38 (Fintype.piFinset (fun i ↦ sidePatterns (f i) (conditionOfAnswers ρ valid (ω i) g b))).image
    39 (fun a ↦ (b, a)))
    40
    41/-- The reference answers and queried larger-table answers supplied by the given tables. -/
    42noncomputable def transcript {Ω : Type} {u w n s q : ℕ}
    43 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w) (R : Table u) (A : Ω → Table w)
    44 (ω : Fin n → Ω) (g : Fin q → Coordinate u) (f : Fin n → Fin s → Coordinate w) :
    45 Word q × (Fin n → Pattern w) :=
    46 (fun j ↦ R (g j), fun i ↦ restrict (SideQueried (f i) (FAFTest.condition ρ valid R (ω i) g)) (A (ω i)))
    47
    48axiom transcript_mem {Ω : Type} {u w n s q : ℕ}
    49 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w) (R : Table u) (A : Ω → Table w)
    50 (ω : Fin n → Ω) (g : Fin q → Coordinate u) (f : Fin n → Fin s → Coordinate w)
    51 (h : FAFTest.Accepts ρ valid R A ω g f) :
    52 transcript ρ valid R A ω g f ∈ patterns ρ valid ω g f
    53
    54axiom free_bits {Ω : Type} {u w n s q : ℕ}
    55 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    56 (ω : Fin n → Ω) (g : Fin q → Coordinate u) (f : Fin n → Fin s → Coordinate w) :
    57 (patterns ρ valid ω g f).card ≤ 2 ^ (q + n * s)
    58
    59end Lax323828.FAFPatterns
    60
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…