The padded game adapter

Blueprint lem:lidt-ldc-adapter, the paper's Steps 1--2 and Claims 1--3 of the general-ldc proof of lem:ld-soundness (ldt.tex). A strategy for the seeded test with r codewords in m variables is played as a strategy for the seeded test with one codeword in K + m variables: a combined point (x, y) is answered by ∑_{j<r} x_j b_j from the original point answer b at y, and a combined line by the matching polynomial built from the original line answer.

The seed choice, and how it differs from the paper's

Each combined question is sent to an original question. The only freedom is the original seed, and the paper draws it independently for each player, diagonal seeds from a law proportional to q^{j-1}; the independence then has to be paid for on the two same-type line subtests, by a chain of three consistency links and a d / q term.

Here both players share one seed offset σ, and the original seed's block is determined by the combined seed's block i as j = max(i - K, 0). Then every simulated question pair is the image of a single original sample: sampleMap sends the combined sample (u, s, v) to the original sample (y-part of u, seedOf j σ, y-part of v), with types collapsed to point where the combined line does not move the original coordinates (qmap_question). Acceptance transfers subtest by subtest --- the same-type line subtests to the original equality subtest --- and the push-forward bound is a count of the fibres of sampleMap.

The decider on a sample

accepts_sample_imp and accepts_sample_of characterize the seeded test's decider on the two questions of one sample: formats, then equality for equal types, nothing for the two cross pairs, and otherwise equality of the two answers' values at the sample's point (valAt). Both games are instances, and the transfer is checked on values.

The decider on the two questions of a sample

noncomputable def MIPRE.LIDT.Simul.valAt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (x : CL.Question F m) (u : Point F m) : CL.Answer F m d ldc → Fin ldc → F

The value of an answer at a point: a point answer itself, a line answer evaluated at the parameter of the point on the question's line. This is what the decider compares in the line-versus-point subtests.

Equations

• MIPRE.LIDT.Simul.valAt hm x u (MIPRE.LIDT.CL.Answer.values a) = a
• MIPRE.LIDT.Simul.valAt hm x u (MIPRE.LIDT.CL.Answer.apolys f) = fun (j : Fin ldc) => (f j).eval (MIPRE.LIDT.CL.lineParam x.base (MIPRE.LIDT.CL.Question.dir hm x) u)
• MIPRE.LIDT.Simul.valAt hm x u (MIPRE.LIDT.CL.Answer.dpolys f) = fun (j : Fin ldc) => (f j).eval (MIPRE.LIDT.CL.lineParam x.base (MIPRE.LIDT.CL.Question.dir hm x) u)

def MIPRE.LIDT.Simul.IsCross : CL.Ty → CL.Ty → Prop

The two cross type pairs, on which the decider checks nothing but the formats.

Equations

• MIPRE.LIDT.Simul.IsCross MIPRE.LIDT.CL.Ty.aline MIPRE.LIDT.CL.Ty.dline = True
• MIPRE.LIDT.Simul.IsCross MIPRE.LIDT.CL.Ty.dline MIPRE.LIDT.CL.Ty.aline = True
• MIPRE.LIDT.Simul.IsCross x✝¹ x✝ = False

@[instance_reducible]

instance MIPRE.LIDT.Simul.instDecidableIsCross (t t' : CL.Ty) : Decidable (IsCross t t')

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.LIDT.Simul.SampleRel {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (sm : CL.Sample F m) (a b : CL.Answer F m d ldc) : Prop

The relation the decider checks on the answers to a sample's two questions, once the formats are right.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Simul.sample_mem_line {F : Type u_1} [Field F] {m : ℕ} (w u : Point F m) : ∃ (t : F), u = CL.rep w u + t • w

The sample's point lies on the line of each of its line questions.

theorem MIPRE.LIDT.Simul.accepts_sample_imp {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (sm : CL.Sample F m) {a b : CL.Answer F m d ldc} (h : CL.accepts hm (CL.Sample.question hm sm sm.tyA) (CL.Sample.question hm sm sm.tyB) a b = true) : (CL.Sample.question hm sm sm.tyA).fmtOk a = true ∧ (CL.Sample.question hm sm sm.tyB).fmtOk b = true ∧ SampleRel hm sm a b

What an accepted pair of answers satisfies, on the two questions of a sample.

theorem MIPRE.LIDT.Simul.accepts_sample_of {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (sm : CL.Sample F m) {a b : CL.Answer F m d ldc} (hfa : (CL.Sample.question hm sm sm.tyA).fmtOk a = true) (hfb : (CL.Sample.question hm sm sm.tyB).fmtOk b = true) (hrel : SampleRel hm sm a b) : CL.accepts hm (CL.Sample.question hm sm sm.tyA) (CL.Sample.question hm sm sm.tyB) a b = true

When a pair of answers is accepted, on the two questions of a sample.

Lines through a sample's point

theorem MIPRE.LIDT.Simul.eq_rep_add_lineParam {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (w u : Point F n) : u = CL.rep w u + CL.lineParam (CL.rep w u) w u • w

A point, its canonical base point and its parameter: u = rep w u + (lineParam …) • w, whether or not w vanishes.

def MIPRE.LIDT.Simul.shiftOf {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (w y : Point F n) : F

The shift from a point to the canonical base point of the line through it.

Equations

• MIPRE.LIDT.Simul.shiftOf w y = if h : ∃ (j : Fin n), w j ≠ 0 then y (Fin.find (fun (j : Fin n) => w j ≠ 0) h) / w (Fin.find (fun (j : Fin n) => w j ≠ 0) h) else 0

theorem MIPRE.LIDT.Simul.eq_rep_add_shiftOf {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} {w : Point F n} (hw : ∃ (j : Fin n), w j ≠ 0) (y : Point F n) : y = CL.rep w y + shiftOf w y • w

theorem MIPRE.LIDT.Simul.lineParam_rep_add {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} {w : Point F n} (hw : ∃ (j : Fin n), w j ≠ 0) (y₀ : Point F n) (t : F) : CL.lineParam (CL.rep w y₀) w (y₀ + t • w) = t + shiftOf w y₀

The parameter of a point on a rebased line. If y = y₀ + t w then the parameter of y on the line through y₀ with base point rep w y₀ is t plus the shift of y₀.

theorem MIPRE.LIDT.Simul.rep_add_smul' {F : Type u_1} [Field F] {n : ℕ} (w y : Point F n) (t : F) : CL.rep w (y + t • w) = CL.rep w y

The base point of a line does not see the point it was built from.

The combining and original blocks

@[simp]

theorem MIPRE.LIDT.Simul.yOf_add {F : Type u_1} [Field F] {K m : ℕ} (u v : Point F (K + m)) : yOf (u + v) = yOf u + yOf v

@[simp]

theorem MIPRE.LIDT.Simul.yOf_smul {F : Type u_1} [Field F] {K m : ℕ} (c : F) (u : Point F (K + m)) : yOf (c • u) = c • yOf u

@[simp]

theorem MIPRE.LIDT.Simul.xOf_add {F : Type u_1} [Field F] {K m : ℕ} (u v : Point F (K + m)) : xOf (u + v) = xOf u + xOf v

@[simp]

theorem MIPRE.LIDT.Simul.xOf_smul {F : Type u_1} [Field F] {K m : ℕ} (c : F) (u : Point F (K + m)) : xOf (c • u) = c • xOf u

@[simp]

theorem MIPRE.LIDT.Simul.yOf_zero {F : Type u_1} [Field F] {K m : ℕ} : yOf 0 = 0

def MIPRE.LIDT.Simul.jIdx {K m : ℕ} [NeZero m] (i : Fin (K + m)) : Fin m

The original block index of a combined index: i - K, or 0 for a combining index.

Equations

• MIPRE.LIDT.Simul.jIdx i = if h : K ≤ ↑i then ⟨↑i - K, ⋯⟩ else ⟨0, ⋯⟩

theorem MIPRE.LIDT.Simul.jIdx_of_le {K m : ℕ} [NeZero m] {i : Fin (K + m)} (h : K ≤ ↑i) : ↑(jIdx i) = ↑i - K

theorem MIPRE.LIDT.Simul.yOf_single_of_le {F : Type u_1} [Field F] {K m : ℕ} [NeZero m] {i : Fin (K + m)} (h : K ≤ ↑i) : yOf (Pi.single i 1) = Pi.single (jIdx i) 1

theorem MIPRE.LIDT.Simul.yOf_single_of_lt {F : Type u_1} [Field F] {K m : ℕ} {i : Fin (K + m)} (h : ↑i < K) : yOf (Pi.single i 1) = 0

theorem MIPRE.LIDT.Simul.xOf_single_of_le {F : Type u_1} [Field F] {K m : ℕ} {i : Fin (K + m)} (h : K ≤ ↑i) : xOf (Pi.single i 1) = 0

theorem MIPRE.LIDT.Simul.yOf_zeroBelow {F : Type u_1} [Field F] {K m : ℕ} [NeZero m] (i : Fin (K + m)) (v : Point F (K + m)) : yOf (CL.zeroBelow i v) = CL.zeroBelow (jIdx i) (yOf v)

theorem MIPRE.LIDT.Simul.yOf_rep_single_of_le {F : Type u_1} [Field F] {K m : ℕ} [NeZero m] [DecidableEq F] {i : Fin (K + m)} (h : K ≤ ↑i) (u : Point F (K + m)) : yOf (CL.rep (Pi.single i 1) u) = yOf u + -u i • Pi.single (jIdx i) 1

theorem MIPRE.LIDT.Simul.yOf_rep_single_of_lt {F : Type u_1} [Field F] {K m : ℕ} [DecidableEq F] {i : Fin (K + m)} (h : ↑i < K) (u : Point F (K + m)) : yOf (CL.rep (Pi.single i 1) u) = yOf u

theorem MIPRE.LIDT.Simul.exists_yOf_rep {F : Type u_1} [Field F] {K m : ℕ} [Fintype F] [DecidableEq F] (w u : Point F (K + m)) : ∃ (t : F), yOf (CL.rep w u) = yOf u + t • yOf w

The question map and the sample map

noncomputable def MIPRE.LIDT.Simul.jOf {F : Type u_1} [Field F] [Fintype F] {K m : ℕ} [NeZero m] [NeZero (K + m)] (hM : K + m ∣ Fintype.card F) (s : F) : Fin m

The original seed block of a combined seed.

Equations

• MIPRE.LIDT.Simul.jOf hM s = MIPRE.LIDT.Simul.jIdx (MIPRE.LIDT.CL.chi hM s)

def MIPRE.LIDT.Simul.tyMap {F : Type u_1} [Field F] [DecidableEq F] {K m : ℕ} (i : Fin (K + m)) (wy : Point F m) : CL.Ty → CL.Ty

The type map: an axis-parallel line along a combining coordinate, and a diagonal line whose original part is constant, become point questions.

Equations

• MIPRE.LIDT.Simul.tyMap i wy MIPRE.LIDT.CL.Ty.point = MIPRE.LIDT.CL.Ty.point
• MIPRE.LIDT.Simul.tyMap i wy MIPRE.LIDT.CL.Ty.aline = if K ≤ ↑i then MIPRE.LIDT.CL.Ty.aline else MIPRE.LIDT.CL.Ty.point
• MIPRE.LIDT.Simul.tyMap i wy MIPRE.LIDT.CL.Ty.dline = if wy = 0 then MIPRE.LIDT.CL.Ty.point else MIPRE.LIDT.CL.Ty.dline

noncomputable def MIPRE.LIDT.Simul.qmap {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (σ : Fin (Fintype.card F / m)) : CL.Question F (K + m) → CL.Question F m

The question map, with the shared seed offset σ.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.Simul.qmap hm hM σ (MIPRE.LIDT.CL.Question.point u) = MIPRE.LIDT.CL.Question.point (MIPRE.LIDT.Simul.yOf u)

noncomputable def MIPRE.LIDT.Simul.wyOf {F : Type u_1} [Field F] [Fintype F] {K m : ℕ} [NeZero (K + m)] (hM : K + m ∣ Fintype.card F) (sm : CL.Sample F (K + m)) : Point F m

The original part of a combined sample's diagonal direction.

Equations

• MIPRE.LIDT.Simul.wyOf hM sm = MIPRE.LIDT.Simul.yOf (MIPRE.LIDT.CL.zeroBelow (MIPRE.LIDT.CL.chi hM sm.s) sm.v)

noncomputable def MIPRE.LIDT.Simul.sampleMap {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (σ : Fin (Fintype.card F / m)) (sm : CL.Sample F (K + m)) : CL.Sample F m

The sample map: one original sample for the whole combined sample.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Simul.qmap_question {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (σ : Fin (Fintype.card F / m)) (sm : CL.Sample F (K + m)) (t : CL.Ty) : qmap hm hM σ (CL.Sample.question hM sm t) = CL.Sample.question hm (sampleMap hm hM σ sm) (tyMap (CL.chi hM sm.s) (wyOf hM sm) t)

Every simulated question is the mapped sample's question.

The answer map

def MIPRE.LIDT.Simul.xr {F : Type u_1} {K r : ℕ} (hr : r ≤ K) (x : Point F K) : Fin r → F

The first r combining coordinates.

Equations

• MIPRE.LIDT.Simul.xr hr x k = x (Fin.castLE hr k)

@[simp]

theorem MIPRE.LIDT.Simul.xr_add {F : Type u_1} [Field F] {K r : ℕ} (hr : r ≤ K) (x x' : Point F K) : xr hr (x + x') = xr hr x + xr hr x'

@[simp]

theorem MIPRE.LIDT.Simul.xr_smul {F : Type u_1} [Field F] {K r : ℕ} (hr : r ≤ K) (c : F) (x : Point F K) : xr hr (c • x) = c • xr hr x

@[simp]

theorem MIPRE.LIDT.Simul.xr_zero {F : Type u_1} [Field F] {K r : ℕ} (hr : r ≤ K) : xr hr 0 = 0

def MIPRE.LIDT.Simul.linEval {F : Type u_1} [Field F] {K r : ℕ} (hr : r ≤ K) (b : Fin r → F) (x : Point F K) : F

The combined point answer ∑_{k<r} x_k b_k.

Equations

• MIPRE.LIDT.Simul.linEval hr b x = ∑ k : Fin r, MIPRE.LIDT.Simul.xr hr x k * b k

theorem MIPRE.LIDT.Simul.eval_linPoly_padB {F : Type u_1} [Field F] {K r d : ℕ} (hd : 1 ≤ d) (hr : r ≤ K) (b : Fin r → F) (x : Point F K) : (linPoly hd (padB b)).eval x = linEval hr b x

noncomputable def MIPRE.LIDT.Simul.affPoly {F : Type u_1} [Field F] {r : ℕ} (α β : Fin r → F) (c : F) (P : Fin r → Polynomial F) : Polynomial F

The affine-in-t combination ∑_k (α_k + β_k t) P_k(t + c).

Equations

• MIPRE.LIDT.Simul.affPoly α β c P = ∑ k : Fin r, (Polynomial.C (α k) + Polynomial.C (β k) * Polynomial.X) * (P k).comp (Polynomial.X + Polynomial.C c)

theorem MIPRE.LIDT.Simul.eval_affPoly {F : Type u_1} [Field F] {r : ℕ} (α β : Fin r → F) (c : F) (P : Fin r → Polynomial F) (t : F) : Polynomial.eval t (affPoly α β c P) = ∑ k : Fin r, (α k + β k * t) * Polynomial.eval (t + c) (P k)

theorem MIPRE.LIDT.Simul.natDegree_affPoly_le {F : Type u_1} [Field F] {r : ℕ} {α β : Fin r → F} {c : F} {P : Fin r → Polynomial F} {D : ℕ} (h : ∀ (k : Fin r), (P k).natDegree ≤ D) : (affPoly α β c P).natDegree ≤ D + 1

theorem MIPRE.LIDT.Simul.natDegree_affPoly_le_of_zero {F : Type u_1} [Field F] {r : ℕ} {α : Fin r → F} {c : F} {P : Fin r → Polynomial F} {D : ℕ} (h : ∀ (k : Fin r), (P k).natDegree ≤ D) : (affPoly α 0 c P).natDegree ≤ D

def MIPRE.LIDT.Simul.valsOf {F : Type u_1} [Field F] {r m d : ℕ} : CL.Answer F m d r → Fin r → F

The coordinates of a point answer; 0 for the wrong format.

Equations

• MIPRE.LIDT.Simul.valsOf (MIPRE.LIDT.CL.Answer.values b) = b
• MIPRE.LIDT.Simul.valsOf x✝ = 0

noncomputable def MIPRE.LIDT.Simul.polysOf {F : Type u_1} [Field F] {r m d : ℕ} : CL.Answer F m d r → Fin r → Polynomial F

The r polynomials an answer carries: constants for a point answer.

Equations

• MIPRE.LIDT.Simul.polysOf (MIPRE.LIDT.CL.Answer.values b) = fun (k : Fin r) => Polynomial.C (b k)
• MIPRE.LIDT.Simul.polysOf (MIPRE.LIDT.CL.Answer.apolys g) = fun (k : Fin r) => MIPRE.LIDT.Adapter.toPoly (g k)
• MIPRE.LIDT.Simul.polysOf (MIPRE.LIDT.CL.Answer.dpolys g) = fun (k : Fin r) => MIPRE.LIDT.Adapter.toPoly (g k)

noncomputable def MIPRE.LIDT.Simul.lineAns {F : Type u_1} [Field F] {K r m d : ℕ} [DecidableEq F] (hr : r ≤ K) (u₀ w : Point F (K + m)) (a : CL.Answer F m d r) : Polynomial F

The combined line answer on the line through u₀ in direction w: at the parameter t, the combined point answer at u₀ + t w.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Simul.rmap {F : Type u_1} [Field F] {K r m d : ℕ} [Fintype F] [DecidableEq F] [NeZero (K + m)] (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) : CL.Question F (K + m) → CL.Answer F m d r → CL.Answer F (K + m) d 1

The answer map.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.Simul.rmap hM hr (MIPRE.LIDT.CL.Question.dline u₀ s w) x✝ = MIPRE.LIDT.CL.Answer.dpolys fun (x : Fin 1) => MIPRE.LIDT.Adapter.ofPoly (MIPRE.LIDT.Simul.lineAns hr u₀ w x✝)

theorem MIPRE.LIDT.Simul.fmtOk_rmap {F : Type u_1} [Field F] {K r m d : ℕ} [Fintype F] [DecidableEq F] [NeZero (K + m)] (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (x : CL.Question F (K + m)) (a : CL.Answer F m d r) : x.fmtOk (rmap hM hr x a) = true

Values transfer

theorem MIPRE.LIDT.Simul.base_add_lineParam {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} {u₀ w u : Point F n} (h : ∃ (t : F), u = u₀ + t • w) : u₀ + CL.lineParam u₀ w u • w = u

A point on a line is the base point moved by its parameter.

theorem MIPRE.LIDT.Simul.eval_lineAns_eq {F : Type u_1} [Field F] [DecidableEq F] {K m d r : ℕ} (hr : r ≤ K) {u₀ w : Point F (K + m)} {a : CL.Answer F m d r} {t : F} {V : Fin r → F} (h : ∀ (k : Fin r), Polynomial.eval (t + shiftOf (yOf w) (yOf u₀)) (polysOf a k) = V k) : Polynomial.eval t (lineAns hr u₀ w a) = linEval hr V (xOf (u₀ + t • w))

theorem MIPRE.LIDT.Simul.valAt_line_aux {F : Type u_1} [Field F] [DecidableEq F] {K m r : ℕ} (hr : r ≤ K) {D : ℕ} {P : Polynomial F} (hP : P.natDegree ≤ D) {u₀ w u : Point F (K + m)} (hu : ∃ (t : F), u = u₀ + t • w) (V : Point F m → Fin r → F) (hPV : ∀ (t : F), Polynomial.eval t P = linEval hr (V (yOf (u₀ + t • w))) (xOf (u₀ + t • w))) : (Adapter.ofPoly P).eval (CL.lineParam u₀ w u) = linEval hr (V (yOf u)) (xOf u)

theorem MIPRE.LIDT.Simul.natDegree_polysOf_values {F : Type u_1} [Field F] {m d r : ℕ} (b : Fin r → F) (k : Fin r) : (polysOf (CL.Answer.values b) k).natDegree ≤ 0

theorem MIPRE.LIDT.Simul.valAt_rmap {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (hd : 1 ≤ d) (hK : 1 ≤ K) (σ : Fin (Fintype.card F / m)) (x : CL.Question F (K + m)) {u : Point F (K + m)} (hu : ∃ (t : F), u = x.base + t • CL.Question.dir hM x) {a : CL.Answer F m d r} (hf : (qmap hm hM σ x).fmtOk a = true) (k : Fin 1) : valAt hM x u (rmap hM hr x a) k = linEval hr (valAt hm (qmap hm hM σ x) (yOf u) a) (xOf u)

The value transfer. On a point u of a combined question's line, the combined answer's value is the combined point answer ∑_{k<r} x_k b_k, with b the original answer's value at the original part of u.

Acceptance transfer

theorem MIPRE.LIDT.Simul.sample_question_mem {F : Type u_1} [Field F] [Fintype F] {n : ℕ} [NeZero n] (hn : n ∣ Fintype.card F) (sm : CL.Sample F n) (t : CL.Ty) : ∃ (τ : F), sm.u = (CL.Sample.question hn sm t).base + τ • CL.Question.dir hn (CL.Sample.question hn sm t)

The sample's point lies on each of its questions' lines.

theorem MIPRE.LIDT.Simul.valAt_eq_of_sampleRel {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {d r n : ℕ} [NeZero n] (hn : n ∣ Fintype.card F) {sm : CL.Sample F n} {a b : CL.Answer F n d r} (h : SampleRel hn sm a b) (hc : ¬IsCross sm.tyA sm.tyB) : valAt hn (CL.Sample.question hn sm sm.tyA) sm.u a = valAt hn (CL.Sample.question hn sm sm.tyB) sm.u b

theorem MIPRE.LIDT.Simul.eq_point_of_not_cross {t t' : CL.Ty} (h1 : t ≠ t') (h2 : ¬IsCross t t') : t = CL.Ty.point ∨ t' = CL.Ty.point

theorem MIPRE.LIDT.Simul.not_isCross_point_left (t : CL.Ty) : ¬IsCross CL.Ty.point t

theorem MIPRE.LIDT.Simul.not_isCross_point_right (t : CL.Ty) : ¬IsCross t CL.Ty.point

theorem MIPRE.LIDT.Simul.accepts_rmap {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (hd : 1 ≤ d) (hK : 1 ≤ K) (σ : Fin (Fintype.card F / m)) (sm : CL.Sample F (K + m)) {a b : CL.Answer F m d r} (h : CL.accepts hm (qmap hm hM σ (CL.Sample.question hM sm sm.tyA)) (qmap hm hM σ (CL.Sample.question hM sm sm.tyB)) a b = true) : CL.accepts hM (CL.Sample.question hM sm sm.tyA) (CL.Sample.question hM sm sm.tyB) (rmap hM hr (CL.Sample.question hM sm sm.tyA) a) (rmap hM hr (CL.Sample.question hM sm sm.tyB) b) = true

Acceptance transfers from the mapped original sample to the combined sample.

theorem MIPRE.LIDT.Simul.clGame_D_rmap {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (hd : 1 ≤ d) (hK : 1 ≤ K) (σ : Fin (Fintype.card F / m)) (x y : CL.Question F (K + m)) (a b : CL.Answer F m d r) (hμ : (CL.clGame hM).μ x y ≠ 0) (h : (CL.clGame hm).D (qmap hm hM σ x) (qmap hm hM σ y) a b = true) : (CL.clGame hM).D x y (rmap hM hr x a) (rmap hM hr y b) = true

The acceptance hypothesis of exists_one_sub_value_adapt_le, for the padded adapter.

The fibre count

def MIPRE.LIDT.Simul.sampleEquiv {F : Type u_1} (n : ℕ) : CL.Sample F n ≃ CL.Ty × CL.Ty × Point F n × F × Point F n

The samples as a product.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Simul.card_ty : Fintype.card CL.Ty = 3

theorem MIPRE.LIDT.Simul.card_sample {F : Type u_1} [Fintype F] (n : ℕ) : Fintype.card (CL.Sample F n) = 9 * (Fintype.card F ^ n * (Fintype.card F * Fintype.card F ^ n))

theorem MIPRE.LIDT.Simul.eq_of_xOf_yOf {F : Type u_1} {K m : ℕ} {u u' : Point F (K + m)} (hx : xOf u = xOf u') (hy : yOf u = yOf u') : u = u'

theorem MIPRE.LIDT.Simul.card_jOf_fiber_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m : ℕ} [NeZero m] [NeZero (K + m)] (hM : K + m ∣ Fintype.card F) (j : Fin m) : {s : F | jOf hM s = j}.card ≤ (K + 1) * (Fintype.card F / (K + m))

A seed block of the original test collects at most K + 1 blocks of the combined test.

theorem MIPRE.LIDT.Simul.card_sampleMap_fiber_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (sm : CL.Sample F m) : {p : Fin (Fintype.card F / m) × CL.Sample F (K + m) | sampleMap hm hM p.1 p.2 = sm}.card ≤ 9 * ((K + 1) * (Fintype.card F / (K + m))) * Fintype.card F ^ K * Fintype.card F ^ K

The fibres of the sample map, over the seed offset and the combined sample, have at most 9 (K + 1) (q / (K + m)) q^{2K} elements: the types have three preimages each, the combining coordinates of the point and the direction are free, the combined seed ranges over K + 1 blocks, and the offset is then determined.

theorem MIPRE.LIDT.Simul.clGame_mu_fibre {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {d n l : ℕ} [NeZero n] (hn : n ∣ Fintype.card F) {X : Type u_2} [DecidableEq X] (qA qB : CL.Question F n → X) (x y : X) : ∑ x' : CL.Question F n with qA x' = x, ∑ y' : CL.Question F n with qB y' = y, (CL.clGame hn).μ x' y' = ∑ sm : CL.Sample F n, (↑(Fintype.card (CL.Sample F n)))⁻¹ * if qA (CL.Sample.question hn sm sm.tyA) = x ∧ qB (CL.Sample.question hn sm sm.tyB) = y then 1 else 0

The mass the seeded test puts on the fibre of a pair of question maps.

theorem MIPRE.LIDT.Simul.sum_mu_qmap_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (x y : CL.Question F m) : ∑ σ : Fin (Fintype.card F / m), ∑ x' : CL.Question F (K + m) with qmap hm hM σ x' = x, ∑ y' : CL.Question F (K + m) with qmap hm hM σ y' = y, (CL.clGame hM).μ x' y' ≤ ↑(Fintype.card (Fin (Fintype.card F / m))) * (9 * (↑K + 1) * (CL.clGame hm).μ x y)

The push-forward bound of the padded adapter, averaged over the seed offset, with C = 9 (K + 1).

The padded strategy

noncomputable def MIPRE.LIDT.Simul.tuplePOVMA {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (S : TensorProductStrategy (CL.clGame hm)) (y : Point F m) : POVM (Fin r → F) (Fin S.dA)

The point measurements of player A in a strategy for the seeded test with r codewords, as POVMs with outcomes in F^r; answers of the wrong format are read as 0.

Equations

• MIPRE.LIDT.Simul.tuplePOVMA hm S y = MIPRE.POVM.map MIPRE.LIDT.Simul.valsOf (S.PA.toPOVM (MIPRE.LIDT.CL.Question.point y))

noncomputable def MIPRE.LIDT.Simul.tuplePOVMB {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (S : TensorProductStrategy (CL.clGame hm)) (y : Point F m) : POVM (Fin r → F) (Fin S.dB)

The point measurements of player B, as for tuplePOVMA.

Equations

• MIPRE.LIDT.Simul.tuplePOVMB hm S y = MIPRE.POVM.map MIPRE.LIDT.Simul.valsOf (S.PB.toPOVM (MIPRE.LIDT.CL.Question.point y))

theorem MIPRE.LIDT.Simul.toPOVM_mergeAt {X : Type u_2} {X' : Type u_3} {A : Type u_4} {A' : Type u_5} [Fintype A] [Fintype A'] [DecidableEq A'] {n : Type u_6} [Fintype n] [DecidableEq n] (P : ProjectiveMeasurement X A (Matrix n n ℂ)) (qX : X' → X) (rX : X' → A → A') (x : X') : (P.mergeAt qX rX).toPOVM x = POVM.map (rX x) (P.toPOVM (qX x))

noncomputable def MIPRE.LIDT.Simul.padded {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (S : TensorProductStrategy (CL.clGame hm)) (σ : Fin (Fintype.card F / m)) : TensorProductStrategy (CL.clGame hM)

The padded strategy for the seeded test with one codeword in K + m variables.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Simul.exists_padded_value {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (hd : 1 ≤ d) (hK : 1 ≤ K) (S : TensorProductStrategy (CL.clGame hm)) : ∃ (σ : Fin (Fintype.card F / m)), 1 - (padded hm hM hr S σ).value ≤ 9 * (↑K + 1) * (1 - S.value)

The padded adapter loses a factor 9 (K + 1) (blueprint lem:lidt-ldc-adapter): some seed offset makes the padded strategy fail at most 9 (K + 1) times as often as S.

theorem MIPRE.LIDT.Simul.pointPOVMA_padded {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (hd : 1 ≤ d) (S : TensorProductStrategy (CL.clGame hm)) (σ : Fin (Fintype.card F / m)) (u : Point F (K + m)) : CL.pointPOVMA (padded hm hM hr S σ) u = combPOVM hd (tuplePOVMA hm S) u

The padded strategy's point measurements are the combined ones: at the padded point (x, y), measure the original point measurement at y and answer ∑_{k<r} x_k b_k.

theorem MIPRE.LIDT.Simul.pointPOVMB_padded {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (hd : 1 ≤ d) (S : TensorProductStrategy (CL.clGame hm)) (σ : Fin (Fintype.card F / m)) (u : Point F (K + m)) : CL.pointPOVMB (padded hm hM hr S σ) u = combPOVM hd (tuplePOVMB hm S) u

The same for player B.