Quantum soundness of the seeded CL test with several codewords

Blueprint thm:lidt-cl-soundness, through lem:lidt-ldc and lem:lidt-ldc-error: the simultaneous contract for r codewords, from the single-codeword theorem MIPRE.LIDT.Adapter.clSoundness_ldc_one_deltaCL.

The chain is three steps. A strategy for the test with r codewords in m variables is played as one for the test with one codeword in M = K + m variables (MIPRE/Background/LIDT/Padding), failing at most 9 (K + 1) times as often; the single-codeword theorem applies to it; and the extraction of MIPRE/Background/LIDT/Extraction reads r-tuples of polynomials in the original m variables off its measurements, at an additive cost M d / q on the two point conclusions. clSoundness_padded is the three steps at any K ≥ r.

Choosing M, and the error

M is the least power of two at least m + r, so that M ∣ q when q is a power of two and m + r ≤ q, and M ≤ 2 (m + r) ≤ 4 m r. The error is then absorbed into δ_sim = a (d m r)^a (ε^b + q^{-b} + 2^{-b m d}) with b the single-codeword exponent and a a (large, explicit) constant: M ≤ 4 m r controls the polynomial factor, x^b ≤ x for x ≥ 1 the failure blow-up, and M ≥ m the exponential term. When m + r > q there is no room to pad, and the bound is at least one, so any measurements do (clSoundness).

The padded chain

theorem MIPRE.LIDT.Simul.clSoundness_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) (hK : 1 ≤ K) (hd : 1 ≤ d) (S : TensorProductStrategy (CL.clGame hm)) (ε : ℝ) (hε : 0 ≤ ε) (hS : 1 - ε ≤ S.value) : ∃ (GA : ProjectiveMeasurement Unit (Fin r → LowIndDegPoly) (Matrix (Fin S.dA) (Fin S.dA) ℂ)) (GB : ProjectiveMeasurement Unit (Fin r → LowIndDegPoly) (Matrix (Fin S.dB) (Fin S.dB) ℂ)), inconsistency (uniform (Point F m)) S.ψ (tuplePOVMA hm S) (evalTuplePOVM GB) ≤ deltaCL (Fintype.card F) (K + m) d (9 * (↑K + 1) * ε) + (↑K + ↑m) * ↑d / ↑(Fintype.card F) ∧ inconsistency (uniform (Point F m)) S.ψ (evalTuplePOVM GA) (tuplePOVMB hm S) ≤ deltaCL (Fintype.card F) (K + m) d (9 * (↑K + 1) * ε) + (↑K + ↑m) * ↑d / ↑(Fintype.card F) ∧ (inconsistency (uniform Unit) S.ψ (fun (x : Unit) => GA.toPOVM ()) fun (x : Unit) => GB.toPOVM ()) ≤ deltaCL (Fintype.card F) (K + m) d (9 * (↑K + 1) * ε)

The simultaneous contract, at a padding K ≥ r.

The choice of M

def MIPRE.LIDT.Simul.padM (m r : ℕ) : ℕ

The least power of two at least m + r.

Equations

• MIPRE.LIDT.Simul.padM m r = 2 ^ Nat.clog 2 (m + r)

theorem MIPRE.LIDT.Simul.le_padM (m r : ℕ) : m + r ≤ padM m r

theorem MIPRE.LIDT.Simul.padM_le {m r : ℕ} (hm1 : 1 ≤ m) (hr : 1 ≤ r) : padM m r ≤ 2 * (m + r)

theorem MIPRE.LIDT.Simul.padM_le_mul {m r : ℕ} (hm1 : 1 ≤ m) (hr : 1 ≤ r) : padM m r ≤ 4 * (m * r)

theorem MIPRE.LIDT.Simul.padM_dvd {m r k : ℕ} (hmr : m + r ≤ 2 ^ k) : padM m r ∣ 2 ^ k

The error

noncomputable def MIPRE.LIDT.Simul.simA : ℝ

The constant of δ_sim.

Equations

• MIPRE.LIDT.Simul.simA = 40 * MIPRE.LIDT.clA * 4 ^ MIPRE.LIDT.clA

noncomputable def MIPRE.LIDT.Simul.deltaSim (q m d r : ℕ) (ε : ℝ) : ℝ

δ_sim, the error of the simultaneous contract (blueprint thm:lidt-cl-soundness).

Equations

• MIPRE.LIDT.Simul.deltaSim q m d r ε = MIPRE.LIDT.Simul.simA * ↑(d * m * r) ^ MIPRE.LIDT.Simul.simA * (ε ^ MIPRE.LIDT.clB + ↑q ^ (-MIPRE.LIDT.clB) + 2 ^ (-(MIPRE.LIDT.clB * ↑m * ↑d)))

theorem MIPRE.LIDT.Simul.forty_le_simA : 40 ≤ simA

theorem MIPRE.LIDT.Simul.clA_add_one_le_simA : clA + 1 ≤ simA

theorem MIPRE.LIDT.Simul.rpow_le_rpow_simA {N : ℝ} (hN : 1 ≤ N) : N ^ (clA + 1) ≤ N ^ simA

The polynomial factor dominates: N^{clA + 1} ≤ N^{simA} for N ≥ 1.

theorem MIPRE.LIDT.Simul.deltaCL_padded_le {m d r : ℕ} (hm1 : 1 ≤ m) (hd : 1 ≤ d) (hr : 1 ≤ r) {q M : ℕ} (hq : 1 ≤ q) (hmM : m ≤ M) (hMr : M ≤ 4 * (m * r)) {K : ℕ} (hKM : K + 1 ≤ M) {ε : ℝ} (hε : 0 ≤ ε) : deltaCL q M d (9 * (↑K + 1) * ε) + ↑M * ↑d / ↑q ≤ deltaSim q m d r ε

Absorbing the padded chain's error (blueprint lem:lidt-ldc-error).

theorem MIPRE.LIDT.Simul.one_le_deltaSim {m d r : ℕ} (hm1 : 1 ≤ m) (hd : 1 ≤ d) (hr : 1 ≤ r) {q : ℕ} (hq : 1 ≤ q) (hqmr : q < m + r) {ε : ℝ} (hε : 0 ≤ ε) : 1 ≤ deltaSim q m d r ε

In the trivial regime the error is at least one.

The theorem

def MIPRE.LIDT.Simul.constPM {A : Type u_2} [Fintype A] [DecidableEq A] {n : Type u_3} [Fintype n] [DecidableEq n] (a₀ : A) : ProjectiveMeasurement Unit A (Matrix n n ℂ)

A measurement with a single outcome.

Equations

• MIPRE.LIDT.Simul.constPM a₀ = { M := fun (x : Unit) (a : A) => if a = a₀ then 1 else 0, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

theorem MIPRE.LIDT.Simul.inconsistency_le_one {X : Type u_2} {A : Type u_3} [Fintype X] [Nonempty X] [Fintype A] [DecidableEq A] {dA : Type u_4} {dB : Type u_5} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ψ : dA × dB → ℂ} (hψ : star ψ ⬝ᵥ ψ = 1) (M : X → POVM A dA) (N : X → POVM A dB) : inconsistency (uniform X) ψ M N ≤ 1

theorem MIPRE.LIDT.Simul.clSoundness {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} [NeZero m] {k : ℕ} (hq : Fintype.card F = 2 ^ k) (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) (hr : 1 ≤ r) (S : TensorProductStrategy (CL.clGame hm)) (ε : ℝ) (hε : 0 ≤ ε) (hS : 1 - ε ≤ S.value) : ∃ (GA : ProjectiveMeasurement Unit (Fin r → LowIndDegPoly) (Matrix (Fin S.dA) (Fin S.dA) ℂ)) (GB : ProjectiveMeasurement Unit (Fin r → LowIndDegPoly) (Matrix (Fin S.dB) (Fin S.dB) ℂ)), inconsistency (uniform (Point F m)) S.ψ (tuplePOVMA hm S) (evalTuplePOVM GB) ≤ deltaSim (Fintype.card F) m d r ε ∧ inconsistency (uniform (Point F m)) S.ψ (evalTuplePOVM GA) (tuplePOVMB hm S) ≤ deltaSim (Fintype.card F) m d r ε ∧ (inconsistency (uniform Unit) S.ψ (fun (x : Unit) => GA.toPOVM ()) fun (x : Unit) => GB.toPOVM ()) ≤ deltaSim (Fintype.card F) m d r ε

Quantum soundness of the seeded CL test (blueprint thm:lidt-cl-soundness, through lem:lidt-ldc): for q a power of two, m ∣ q and m, d, r ≥ 1, every strategy passing the seeded test with r codewords with probability at least 1 - ε admits projective measurements of complete r-tuples of polynomials on the two players' spaces, each evaluated at a uniform point consistent with the other player's point measurement, and consistent with each other, all with error δ_sim(ε, q, m, d, r).