The seeded-CL adapter, part 6: the reduction

This is the payoff. MIPRE.LIDT.lowIndividualDegree_soundness is soundness of the canonical-line test lidtGame, proved through the vendored MIPStarRE development; the seeded CL test clGame of def:lidt-cl is a different test, and rem:lidt-cl-adapter says that transferring soundness from one to the other needs an explicit strategy adapter. The previous five parts built it; this one runs it.

The shape of the argument:

• a strategy S for clGame with ldc = 1 is turned into one for lidtGame by reindexing the questions along qmapS (a canonical line becomes a seeded description of its reversal) and coarse-graining the answers along amap (the diagonal answer is affinely reparametrized);
• hD_qmap says the adapted strategy is accepted wherever S is, and pushforward_le says the push-forward of the question distribution costs a factor 3m, so exists_one_sub_value_adapt_le produces one member of the averaging family whose adapted strategy has 1 - value ≤ 3m ε;
• lowIndividualDegree_soundness applies to it and returns two low-degree measurements;
• the three consistency conclusions are carried back through the coordinate reversal (inconsistency_congr), which acts on the questions by revPoint --- measure-preserving, uniform being uniform --- and on the outcomes by revPoly, the same reversal of a polynomial's exponent vectors.

clSoundness_ldc_one states the conclusion with the canonical-line error; combining it with Adapter/Parameters.lean's choice of k gives clSoundness_ldc_one_deltaCL, the ldc = 1 case of thm:lidt-cl-soundness with the blueprint's own δ_CL.

What is not here: the ldc > 1 case (lem:lidt-ldc, the paper's Steps 1--5).

Reversing a polynomial

The adapter plays a canonical-line question at the reversed point, so the low-degree polynomial the soundness theorem produces is a polynomial in the reversed variables. Reversing the exponent vectors turns it back, and does so bijectively and degree-preservingly --- the individual degree bound d is symmetric in the variables.

def MIPRE.LIDT.Adapter.revExp {m d : ℕ} : (Fin m → Fin (d + 1)) ≃ (Fin m → Fin (d + 1))

Coordinate reversal on exponent vectors.

Equations

• MIPRE.LIDT.Adapter.revExp = { toFun := fun (e : Fin m → Fin (d + 1)) (i : Fin m) => e i.rev, invFun := fun (e : Fin m → Fin (d + 1)) (i : Fin m) => e i.rev, left_inv := ⋯, right_inv := ⋯ }

def MIPRE.LIDT.Adapter.revPoly {F : Type u_1} {m d : ℕ} (p : LowIndDegPoly) : LowIndDegPoly

Coordinate reversal on polynomials of individual degree at most d.

Equations

• MIPRE.LIDT.Adapter.revPoly p e = p (MIPRE.LIDT.Adapter.revExp e)

theorem MIPRE.LIDT.Adapter.eval_revPoly {F : Type u_1} [Field F] {m d : ℕ} (p : LowIndDegPoly) (u : Point F m) : (revPoly p).eval u = p.eval (revPoint u)

Reversing a polynomial is reversing its argument.

def MIPRE.LIDT.Adapter.revPolyEquiv {F : Type u_1} {m d : ℕ} : LowIndDegPoly ≃ LowIndDegPoly

Polynomial reversal as an equivalence.

Equations

• MIPRE.LIDT.Adapter.revPolyEquiv = { toFun := MIPRE.LIDT.Adapter.revPoly, invFun := MIPRE.LIDT.Adapter.revPoly, left_inv := ⋯, right_inv := ⋯ }

Two computations of measurement operators

theorem MIPRE.LIDT.Adapter.val_mats_map {A : Type u_2} {B : Type u_3} {n : Type u_4} [Fintype A] [Fintype B] [DecidableEq B] [Fintype n] [DecidableEq n] (f : A → B) (M : POVM A n) (b : B) : ↑((POVM.map f M).mats b) = ∑ a : A with f a = b, ↑(M.mats a)

The operators of a coarse-grained POVM, as a sum over the fibre.

theorem MIPRE.LIDT.Adapter.sum_filter_comp {ι : Type u_2} {κ : Type u_3} {ρ : Type u_4} [Fintype ι] [Fintype κ] [DecidableEq κ] [DecidableEq ρ] {M : Type u_5} [AddCommMonoid M] (r : ι → κ) (g : κ → ρ) (h : ι → M) (f : ρ) : ∑ a' : κ with g a' = f, ∑ a : ι with r a = a', h a = ∑ a : ι with g (r a) = f, h a

Composing two coarse-grainings of a sum over fibres.

theorem MIPRE.LIDT.Adapter.toValue_amap_point {F : Type u_1} [Field F] [DecidableEq F] {m d : ℕ} (c : F) (u : Point F m) (a : CL.Answer F m d 1) : (amap c (Question.point u) a).toValue = a.toValue

The adapter reads a point answer exactly as the seeded test does.

The adapted strategy's point measurements

noncomputable def MIPRE.LIDT.Adapter.adapted {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (σc : Seed F m) (S : TensorProductStrategy (CL.clGame hm)) : TensorProductStrategy (lidtGame F m d)

The strategy the adapter builds, for one member of the averaging family.

Equations

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

theorem MIPRE.LIDT.Adapter.val_mats_pointPOVMA_adapted {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (σc : Seed F m) (S : TensorProductStrategy (CL.clGame hm)) (u : Point F m) (f : F) : ↑((CL.pointPOVMA S u).mats f) = ↑((pointPOVMA (adapted σc S) (revPoint u)).mats f)

A's point measurement of the adapted strategy is A's point measurement of the seeded strategy at the reversed point.

theorem MIPRE.LIDT.Adapter.val_mats_pointPOVMB_adapted {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (σc : Seed F m) (S : TensorProductStrategy (CL.clGame hm)) (u : Point F m) (f : F) : ↑((CL.pointPOVMB S u).mats f) = ↑((pointPOVMB (adapted σc S) (revPoint u)).mats f)

B's point measurement, likewise.

Reversing the low-degree measurements

def MIPRE.LIDT.Adapter.revMeas {F : Type u_1} [Fintype F] {m d : ℕ} {n : Type u_2} [Fintype n] [DecidableEq n] (G : ProjectiveMeasurement Unit LowIndDegPoly (Matrix n n ℂ)) : ProjectiveMeasurement Unit LowIndDegPoly (Matrix n n ℂ)

The reversal of a measurement with polynomial outcomes.

Equations

• MIPRE.LIDT.Adapter.revMeas G = G.reindex (fun (x : Unit) => ()) MIPRE.LIDT.Adapter.revPolyEquiv

theorem MIPRE.LIDT.Adapter.val_mats_evalPOVM_revMeas {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {n : Type u_2} [Fintype n] [DecidableEq n] (G : ProjectiveMeasurement Unit LowIndDegPoly (Matrix n n ℂ)) (u : Point F m) (a : F) : ↑((evalPOVM (revMeas G) u).mats a) = ↑((evalPOVM G (revPoint u)).mats a)

Evaluating the reversal is evaluating at the reversed point.

The reduction

theorem MIPRE.LIDT.Adapter.clSoundness_ldc_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (S : TensorProductStrategy (CL.clGame hm)) (ε : ℝ) (hS : 1 - ε ≤ S.value) (k : ℕ) (hk : 400 * m * d ≤ k) (hk0 : 0 < k) : ∃ (GA : ProjectiveMeasurement Unit LowIndDegPoly (Matrix (Fin S.dA) (Fin S.dA) ℂ)) (GB : ProjectiveMeasurement Unit LowIndDegPoly (Matrix (Fin S.dB) (Fin S.dB) ℂ)), inconsistency (uniform (Point F m)) S.ψ (CL.pointPOVMA S) (evalPOVM GB) ≤ lidtError m d (Fintype.card F) k (3 * ↑m * ε) ∧ inconsistency (uniform (Point F m)) S.ψ (evalPOVM GA) (CL.pointPOVMB S) ≤ lidtError m d (Fintype.card F) k (3 * ↑m * ε) ∧ (inconsistency (uniform Unit) S.ψ (fun (x : Unit) => GA.toPOVM ()) fun (x : Unit) => GB.toPOVM ()) ≤ lidtError m d (Fintype.card F) k (3 * ↑m * ε)

Soundness of the seeded CL test at ldc = 1, by reduction to the canonical-line test.

A strategy for clGame passing with probability at least 1 - ε has point measurements consistent, up to lidtError m d q k (3m·ε), with the evaluations of a single measurement with low-individual-degree outcomes --- one per player, the two consistent with each other. The factor 3m is the push-forward cost of the adapter (pushforward_le); the k is free subject to k ≥ 400md, exactly as in the canonical-line theorem.

This is the ldc = 1 case of thm:lidt-cl-soundness with the error in the canonical-line form. Turning lidtError m d q k (3m ε) into the δ_CL the blueprint asks for is a separate arithmetic obligation, and ldc > 1 is lem:lidt-ldc, a separate piece of work on top.

theorem MIPRE.LIDT.Adapter.clSoundness_ldc_one_deltaCL {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (S : TensorProductStrategy (CL.clGame hm)) (ε : ℝ) (hε : 0 ≤ ε) (hS : 1 - ε ≤ S.value) (hm1 : 1 ≤ m) (hd : 1 ≤ d) : ∃ (GA : ProjectiveMeasurement Unit LowIndDegPoly (Matrix (Fin S.dA) (Fin S.dA) ℂ)) (GB : ProjectiveMeasurement Unit LowIndDegPoly (Matrix (Fin S.dB) (Fin S.dB) ℂ)), inconsistency (uniform (Point F m)) S.ψ (CL.pointPOVMA S) (evalPOVM GB) ≤ deltaCL (Fintype.card F) m d ε ∧ inconsistency (uniform (Point F m)) S.ψ (evalPOVM GA) (CL.pointPOVMB S) ≤ deltaCL (Fintype.card F) m d ε ∧ (inconsistency (uniform Unit) S.ψ (fun (x : Unit) => GA.toPOVM ()) fun (x : Unit) => GB.toPOVM ()) ≤ deltaCL (Fintype.card F) m d ε

The ldc = 1 case of thm:lidt-cl-soundness. The same conclusion as clSoundness_ldc_one, with the blueprint's own error δ_CL = a (dm)^a (ε^b + q^{-b} + 2^{-bmd}) in place of the canonical-line one --- the sampling parameter is clK m d = 400 m³ d + 400 m and the constants are a = 2·10^11, b = 1/40000 (lidtError_le_deltaCL).

1 ≤ d is needed and is not cosmetic: at d = 0 the blueprint's δ_CL is identically zero.