Documentation

MIPRE.Tailored.Sofic.Significance

The significance of the generators of the associated test #

Proposition I:2283, for assocTest g. The words of the challenge at (x, y) use only J and the variables X(x, i), i < ℓ(x), and X(y, i), i < ℓ(y) (wordOK_words); there are at most 2 + 2(ℓ(x) + ℓ(y)) + ℓ(x)² + ℓ(y)² + 2(ℓ^R(x) + ℓ^R(y)) + 2^{ℓ(x) + ℓ(y) + 1} + 1 of them, the constraint words being deduplicated, each of length at most ℓ(x) + ℓ(y) + 4. Hence, with L = Λ = g.ansLen, every generator has significance at most sigBound g = (2L + 4)(3 + 8L + 2L² + 2·4^L) (sig_le), and the variable X(x, i) at most sigBound g · m(x) / W, where m(x) = Σ_y (w(x, y) + w(y, x)) is the weight of the question pairs at x and W the total weight (sig_genX_le).

The paper's count is finer (4 · 2^{2Λ}); the coarser one suffices for the perturbation bound.

Bit lists #

theorem MIPRE.Tailored.Sofic.length_allBits (n : ℕ) :

(allBits n).length = 2 ^ n

theorem MIPRE.Tailored.Sofic.mem_allBits (n : ℕ) (l : List Bool) :

l.length = n → l ∈ allBits n

theorem MIPRE.Tailored.Sofic.length_consWord_le (g : TailoredGameValue.TailoredGameData) (x y : ℕ) (c : List Bool) :

List.length (consWord g x y c) ≤ g.lenAt x + g.lenAt y + 1

theorem MIPRE.Tailored.Sofic.length_consWords_le (g : TailoredGameValue.TailoredGameData) (x y : ℕ) :

(consWords g x y).length ≤ 2 ^ (g.lenAt x + g.lenAt y + 1) + 1

The generators of a challenge #

def MIPRE.Tailored.Sofic.GenOK (g : TailoredGameValue.TailoredGameData) (x y k : ℕ) :

The generators that may occur in the challenge at (x, y).

Equations

MIPRE.Tailored.Sofic.GenOK g x y k = (k = MIPRE.Tailored.Sofic.genJ ∨ (∃ i < g.lenAt x, k = MIPRE.Tailored.Sofic.genX g x i) ∨ ∃ i < g.lenAt y, k = MIPRE.Tailored.Sofic.genX g y i)

Instances For

def MIPRE.Tailored.Sofic.WordOK (g : TailoredGameValue.TailoredGameData) (x y : ℕ) (w : SubgroupTestValue.Word) :

Every letter of w is a generator of the challenge at (x, y).

Equations

MIPRE.Tailored.Sofic.WordOK g x y w = ∀ l ∈ w, MIPRE.Tailored.Sofic.GenOK g x y l.1

Instances For

theorem MIPRE.Tailored.Sofic.wordOK_append {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {u v : SubgroupTestValue.Word} (hu : WordOK g x y u) (hv : WordOK g x y v) :

WordOK g x y (u ++ v)

theorem MIPRE.Tailored.Sofic.wordOK_invW {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {u : SubgroupTestValue.Word} (hu : WordOK g x y u) :

WordOK g x y (invW u)

theorem MIPRE.Tailored.Sofic.wordOK_commW {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {u v : SubgroupTestValue.Word} (hu : WordOK g x y u) (hv : WordOK g x y v) :

WordOK g x y (commW u v)

theorem MIPRE.Tailored.Sofic.wordOK_wJ {g : TailoredGameValue.TailoredGameData} {x y : ℕ} :

WordOK g x y wJ

theorem MIPRE.Tailored.Sofic.wordOK_nil {g : TailoredGameValue.TailoredGameData} {x y : ℕ} :

WordOK g x y []

theorem MIPRE.Tailored.Sofic.wordOK_wX_x {g : TailoredGameValue.TailoredGameData} {x y i : ℕ} (hi : i < g.lenAt x) :

WordOK g x y (wX g x i)

theorem MIPRE.Tailored.Sofic.wordOK_wX_y {g : TailoredGameValue.TailoredGameData} {x y i : ℕ} (hi : i < g.lenAt y) :

WordOK g x y (wX g y i)

theorem MIPRE.Tailored.Sofic.wordOK_varsAt_x {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {X : SubgroupTestValue.Word} (h : X ∈ varsAt g x) :

WordOK g x y X

theorem MIPRE.Tailored.Sofic.wordOK_varsAt_y {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {X : SubgroupTestValue.Word} (h : X ∈ varsAt g y) :

WordOK g x y X

theorem MIPRE.Tailored.Sofic.wordOK_flatMap_x {g : TailoredGameValue.TailoredGameData} {x y : ℕ} (L : List ℕ) (hL : ∀ i ∈ L, i < g.lenAt x) :

WordOK g x y (List.flatMap (wX g x) L)

theorem MIPRE.Tailored.Sofic.wordOK_flatMap_y {g : TailoredGameValue.TailoredGameData} {x y : ℕ} (L : List ℕ) (hL : ∀ i ∈ L, i < g.lenAt y) :

WordOK g x y (List.flatMap (wX g y) L)

theorem MIPRE.Tailored.Sofic.wordOK_words {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {w : SubgroupTestValue.Word} (hw : w ∈ words g x y) :

WordOK g x y w

Lengths #

theorem MIPRE.Tailored.Sofic.length_words_le {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {w : SubgroupTestValue.Word} (hw : w ∈ words g x y) :

List.length w ≤ g.lenAt x + g.lenAt y + 4

theorem MIPRE.Tailored.Sofic.length_fixedLits {g : TailoredGameValue.TailoredGameData} {x y : ℕ} :

(fixedLits g x y).length = 2 + 2 * (g.lenAt x + g.lenAt y) + g.lenAt x ^ 2 + g.lenAt y ^ 2

theorem MIPRE.Tailored.Sofic.length_readWords {g : TailoredGameValue.TailoredGameData} {x y : ℕ} :

(readWords g x y).length = 2 * (g.lenRAt x + g.lenRAt y)

theorem MIPRE.Tailored.Sofic.lenRAt_le_lenAt {g : TailoredGameValue.TailoredGameData} (z : ℕ) :

g.lenRAt z ≤ g.lenAt z

theorem MIPRE.Tailored.Sofic.lenAt_le_ansLen {g : TailoredGameValue.TailoredGameData} {z : ℕ} (hz : z < g.nV + 1) :

g.lenAt z ≤ g.ansLen

Significance #

def MIPRE.Tailored.Sofic.sigBound (g : TailoredGameValue.TailoredGameData) :

The bound on the significance of every generator.

Equations

MIPRE.Tailored.Sofic.sigBound g = (2 * g.ansLen + 4) * (3 + 8 * g.ansLen + 2 * g.ansLen ^ 2 + 2 * 4 ^ g.ansLen)

Instances For

theorem MIPRE.Tailored.Sofic.count_words_le {g : TailoredGameValue.TailoredGameData} {x y : ℕ} (hx : x < g.nV + 1) (hy : y < g.nV + 1) (k : ℕ) :

(List.map (fun (w : SubgroupTestValue.Word) => ↑(wordCount k w)) (words g x y)).sum ≤ if GenOK g x y k then ↑(sigBound g) else 0

The occurrences of any generator in the words of a challenge number at most sigBound g, and none unless the generator belongs to the challenge.

theorem MIPRE.Tailored.Sofic.sig_le {g : TailoredGameValue.TailoredGameData} (k : ℕ) :

sig (assocTest g) k ≤ ↑(sigBound g)

def MIPRE.Tailored.Sofic.mdeg (g : TailoredGameValue.TailoredGameData) (x : ℕ) :

The weight of the question pairs at the vertex x, m(x) = Σ_y (w(x, y) + w(y, x)).

Equations

MIPRE.Tailored.Sofic.mdeg g x = ∑ y ∈ Finset.range (g.nV + 1), (MIPRE.Tailored.Sofic.qw g x y + MIPRE.Tailored.Sofic.qw g y x)

Instances For

theorem MIPRE.Tailored.Sofic.sum_mdeg (g : TailoredGameValue.TailoredGameData) :

∑ x ∈ Finset.range (g.nV + 1), mdeg g x = 2 * qwTot g

theorem MIPRE.Tailored.Sofic.genX_inj {g : TailoredGameValue.TailoredGameData} {x x' i i' : ℕ} (hi : i < g.ansLen) (hi' : i' < g.ansLen) (h : genX g x i = genX g x' i') :

x = x'

The generators X(x, i) and X(x', i'), i, i' < Λ, coincide only when x = x'.

theorem MIPRE.Tailored.Sofic.genX_ne_genJ {g : TailoredGameValue.TailoredGameData} (x i : ℕ) :

genX g x i ≠ genJ

theorem MIPRE.Tailored.Sofic.sig_genX_le {g : TailoredGameValue.TailoredGameData} {x i : ℕ} (hx : x < g.nV + 1) (hi : i < g.lenAt x) :

sig (assocTest g) (genX g x i) ≤ ↑(sigBound g) * ↑(mdeg g x) / ↑(qwTot g)

Significance of a variable (Proposition I:2283): X(x, i) has significance at most sigBound g · m(x) / W.