Lax Lean Archive

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

Free bits of the FAF test

Lax253009.FAFPatterns · concepts/Lax253009/FAFPatterns.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 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 Lax253009.FAFTest
    2import Lax253009.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 Lax253009.FAFPatterns
    21
    22open LongCode LongCodePatterns
    23
    24noncomputable def conditionOfAnswers {Ω : Type} {u w q : ℕ}
    25 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    26 (ω : Ω) (g : Fin q → Coordinate u) (b : Word q) : Coordinate w :=
    27 fun y ↦ valid ω y && decide (∀ j, g j (ρ ω y) = b j)
    28
    29noncomputable def patterns {Ω : Type} {u w n s q : ℕ}
    30 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    31 (ω : Fin n → Ω) (g : Fin q → Coordinate u) (f : Fin n → Fin s → Coordinate w) :
    32 Finset (Word q × (Fin n → Pattern w)) := by
    33 classical
    34 exact Finset.univ.biUnion (fun b : Word q ↦
    35 (Fintype.piFinset (fun i ↦ sidePatterns (f i) (conditionOfAnswers ρ valid (ω i) g b))).image
    36 (fun a ↦ (b, a)))
    37
    38noncomputable def transcript {Ω : Type} {u w n s q : ℕ}
    39 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w) (R : Table u) (A : Ω → Table w)
    40 (ω : Fin n → Ω) (g : Fin q → Coordinate u) (f : Fin n → Fin s → Coordinate w) :
    41 Word q × (Fin n → Pattern w) :=
    42 (fun j ↦ R (g j), fun i ↦ restrict (SideQueried (f i) (FAFTest.condition ρ valid R (ω i) g)) (A (ω i)))
    43
    44axiom transcript_mem {Ω : Type} {u w n s q : ℕ}
    45 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w) (R : Table u) (A : Ω → Table w)
    46 (ω : Fin n → Ω) (g : Fin q → Coordinate u) (f : Fin n → Fin s → Coordinate w)
    47 (h : FAFTest.Accepts ρ valid R A ω g f) :
    48 transcript ρ valid R A ω g f ∈ patterns ρ valid ω g f
    49
    50axiom free_bits {Ω : Type} {u w n s q : ℕ}
    51 (ρ : Ω → Word w → Word u) (valid : Ω → Coordinate w)
    52 (ω : Fin n → Ω) (g : Fin q → Coordinate u) (f : Fin n → Fin s → Coordinate w) :
    53 (patterns ρ valid ω g f).card ≤ 2 ^ (q + n * s)
    54
    55end Lax253009.FAFPatterns
    56
    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…