The model chain, part 2: extracting exactly linear combined codewords

The model counterpart of the operator half of the repository's MIPRE/Background/LIDT/Extraction.lean (blueprint lem:lidt-ldc-extraction; not a vendored file: its matrix statements serve the tensor instance soundIn_tensor and stay), in the port of planning/c6b-plan.md (milestone M14, unit M14-3). It is the paper's Step 4 of the proof of lem:ld-soundness for general ldc (ldt.tex, Claims 4 and 5), read in any bipartite model M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ whose two algebras are star-ordered ⋆-rings (the instance set of MIPRE.LIDT.Simul.SoundIn), at a unit state ‖M.ψ‖ = 1.

The simultaneous test with r codewords is reduced to the single-codeword test in K + m variables by combining: a point (x, y) ∈ F^K × F^m is answered by ∑_{j < r} x_j b_j, where b ∈ F^r is the original point answer at y (combPOVM). The single-codeword theorem returns a measurement R of polynomials in the K + m variables, consistent with the combined answers; extractPM turns it back into a measurement of r-tuples of polynomials in the m original variables, read at a point by MIPRE.LIDT.Simul.evalTuplePOVMIn (ModelSoundness.lean), and extracted_conclusions transfers the three conclusions, at the price (K + m) d / q on the two point conclusions. Every statement is in the vocabulary of M.inconsistency and M.bornProb; the original point measurements A, B are any families (in the chain, the tuple readings MIPRE.LIDT.Simul.tuplePOVMAIn, tuplePOVMBIn of a strategy for the seeded test).

The proofs are those of the matrix file, with the matrix Born rule replaced by the model's: the estimate is the classical MIPRE.LIDT.Simul.sum_agreeX_le, applied to the weights β y b g = M.bornProb (A_y)_b R_g, which are nonnegative because the two players' positive operators commute (BipartiteModel.bornProb_nonneg), and whose sum over b is the weight of g alone (BipartiteModel.bornProb_one_left). Nothing is dimension-dependent.

Reused by import. The classical half of Extraction.lean (the partial evaluation, the linear forms, the extraction itself, Schwartz--Zippel at a fixed y and the weighted bound) is imported and named through an explicit open MIPRE.LIDT.Simul (…) list: extract, extEval, linPoly, padB, agreeX, sum_agreeX_le, xOf, yOf, sum_uniform_pad, sum_uniform_agree, sum_uniform_one, and evalTuplePOVMIn of ModelSoundness.lean.

Not ported

The declarations of the operator section of Extraction.lean are redeclared here, under their names, for POVMs in the algebras of M: inconsistency_eq_one_sub, sum_bornProb_map_right, sum_bornProb_map_left, inconsistency_extract_right_le, inconsistency_extract_left_le, inconsistency_map_le, extractPM, combPOVM and extracted_conclusions. Of the rest:

• isPVM_pm: the matrix projective measurement as an IsPVM family; the model's measurements are POVMIns with IsPVMIn carried beside them, so there is nothing to convert.
• extractPM_toPOVM: extractPM is the coarse-graining R.map (extract hd hr) by definition here.
• evalTuplePOVM: replaced by MIPRE.LIDT.Simul.evalTuplePOVMIn, its existing model form; its lemma evalTuplePOVM_extractPM is evalTuplePOVMIn_extractPM here.
• the classical declarations, above: classical, imported.

inconsistency_map_le drops the hypothesis ∑ x, μ x = 1 of the matrix statement, which its model proof (through BipartiteModel.dis_map_le) does not use, and extracted_conclusions takes RA, RB as POVMs, projectivity being the separate extractPM_isPVMIn.

New here

• extractPM_isPVMIn: the extraction of a projective measurement is projective (POVMIn.isPVMIn_map).
• evalTuplePOVMIn_extractPM: above.

The operator form

theorem MIPRE.LIDT.Co.Chain.inconsistency_eq_one_sub {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {X : Type u_5} {Λ : Type u_6} [Fintype X] [Fintype Λ] [DecidableEq Λ] {μ : X → ℝ} (hμ1 : ∑ x : X, μ x = 1) (hψ : ‖M.ψ‖ = 1) (P : X → POVMIn Λ 𝒜) (Q : X → POVMIn Λ ℬ) : M.inconsistency μ P Q = 1 - ∑ x : X, μ x * ∑ a : Λ, M.bornProb ((P x).op a) ((Q x).op a)

inconsistency is one minus the average agreement, for POVMs at a unit state and a probability distribution on the questions.

theorem MIPRE.LIDT.Co.Chain.sum_bornProb_map_right {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_5} {C : Type u_6} [Fintype A] [Fintype C] [DecidableEq C] (P : C → 𝒜) (N : POVMIn A ℬ) (f : A → C) : ∑ c : C, M.bornProb (P c) ((POVMIn.map f N).op c) = ∑ a : A, M.bornProb (P (f a)) (N.op a)

Relabelling the second family: ∑_c ⟨P_c, (N.map f)_c⟩ = ∑_a ⟨P_{f a}, N_a⟩.

theorem MIPRE.LIDT.Co.Chain.sum_bornProb_map_left {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (M : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_5} {C : Type u_6} [Fintype A] [Fintype C] [DecidableEq C] (N : POVMIn A 𝒜) (Q : C → ℬ) (f : A → C) : ∑ c : C, M.bornProb ((POVMIn.map f N).op c) (Q c) = ∑ a : A, M.bornProb (N.op a) (Q (f a))

Relabelling the first family.

theorem MIPRE.LIDT.Co.Chain.inconsistency_extract_right_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hd : 1 ≤ d) (hr : r ≤ K) (hψ : ‖M.ψ‖ = 1) (A : Point F m → POVMIn (Fin r → F) 𝒜) (R : POVMIn LowIndDegPoly ℬ) : (M.inconsistency (uniform (Point F m)) A fun (y : Point F m) => POVMIn.map (fun (g : LowIndDegPoly) => Simul.extEval hd hr g y) R) ≤ (M.inconsistency (uniform (Point F (K + m))) (fun (u : Point F (K + m)) => POVMIn.map (fun (b : Fin r → F) => (Simul.linPoly hd (Simul.padB b)).eval (Simul.xOf u)) (A (Simul.yOf u))) fun (u : Point F (K + m)) => POVMIn.map (fun (g : LowIndDegPoly) => g.eval u) R) + (↑K + ↑m) * ↑d / ↑(Fintype.card F)

The extraction bound, the extracted measurement on the second party.

theorem MIPRE.LIDT.Co.Chain.inconsistency_extract_left_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hd : 1 ≤ d) (hr : r ≤ K) (hψ : ‖M.ψ‖ = 1) (R : POVMIn LowIndDegPoly 𝒜) (B : Point F m → POVMIn (Fin r → F) ℬ) : M.inconsistency (uniform (Point F m)) (fun (y : Point F m) => POVMIn.map (fun (g : LowIndDegPoly) => Simul.extEval hd hr g y) R) B ≤ (M.inconsistency (uniform (Point F (K + m))) (fun (u : Point F (K + m)) => POVMIn.map (fun (g : LowIndDegPoly) => g.eval u) R) fun (u : Point F (K + m)) => POVMIn.map (fun (b : Fin r → F) => (Simul.linPoly hd (Simul.padB b)).eval (Simul.xOf u)) (B (Simul.yOf u))) + (↑K + ↑m) * ↑d / ↑(Fintype.card F)

The extraction bound, the extracted measurement on the first party.

The extracted measurements, and the three conclusions

theorem MIPRE.LIDT.Co.Chain.inconsistency_map_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {X : Type u_5} {Λ : Type u_6} {C : Type u_7} [Fintype X] [Fintype Λ] [DecidableEq Λ] [Fintype C] [DecidableEq C] {μ : X → ℝ} (hμ0 : ∀ (x : X), 0 ≤ μ x) (hψ : ‖M.ψ‖ = 1) (P : X → POVMIn Λ 𝒜) (Q : X → POVMIn Λ ℬ) (f : Λ → C) : (M.inconsistency μ (fun (x : X) => POVMIn.map f (P x)) fun (x : X) => POVMIn.map f (Q x)) ≤ M.inconsistency μ P Q

Data processing for inconsistency: relabelling both families' outcomes the same way can only decrease the disagreement.

noncomputable def MIPRE.LIDT.Co.Chain.extractPM {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (hd : 1 ≤ d) (hr : r ≤ K) (G : POVMIn LowIndDegPoly R) : POVMIn (Fin r → LowIndDegPoly) R

The extracted measurement: R coarse-grained by extract, a measurement of r-tuples of polynomials in the m original variables.

Equations

• MIPRE.LIDT.Co.Chain.extractPM hd hr G = MIPRE.POVMIn.map (MIPRE.LIDT.Simul.extract hd hr) G

theorem MIPRE.LIDT.Co.Chain.extractPM_isPVMIn {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (hd : 1 ≤ d) (hr : r ≤ K) {G : POVMIn LowIndDegPoly R} (hG : IsPVMIn G.op) : IsPVMIn (extractPM hd hr G).op

The extracted measurement of a projective measurement is projective.

theorem MIPRE.LIDT.Co.Chain.evalTuplePOVMIn_extractPM {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (hd : 1 ≤ d) (hr : r ≤ K) (G : POVMIn LowIndDegPoly R) (y : Point F m) : Simul.evalTuplePOVMIn (extractPM hd hr G) y = POVMIn.map (fun (g : LowIndDegPoly) => Simul.extEval hd hr g y) G

The extracted measurement read at y is R relabelled by the extracted tuple at y.

def MIPRE.LIDT.Co.Chain.combPOVM {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (hd : 1 ≤ d) (A : Point F m → POVMIn (Fin r → F) R) (u : Point F (K + m)) : POVMIn F R

The combined point measurement: at the padded point (x, y), measure the original point measurement at y and answer ∑_{j < r} x_j b_j.

Equations

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

theorem MIPRE.LIDT.Co.Chain.extracted_conclusions {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hd : 1 ≤ d) (hr : r ≤ K) (hψ : ‖M.ψ‖ = 1) (A : Point F m → POVMIn (Fin r → F) 𝒜) (B : Point F m → POVMIn (Fin r → F) ℬ) (RA : POVMIn LowIndDegPoly 𝒜) (RB : POVMIn LowIndDegPoly ℬ) {δ : ℝ} (h1 : M.inconsistency (uniform (Point F (K + m))) (combPOVM hd A) (evalPOVMIn RB) ≤ δ) (h2 : M.inconsistency (uniform (Point F (K + m))) (evalPOVMIn RA) (combPOVM hd B) ≤ δ) (h3 : (M.inconsistency (uniform Unit) (fun (x : Unit) => RA) fun (x : Unit) => RB) ≤ δ) : M.inconsistency (uniform (Point F m)) A (Simul.evalTuplePOVMIn (extractPM hd hr RB)) ≤ δ + (↑K + ↑m) * ↑d / ↑(Fintype.card F) ∧ M.inconsistency (uniform (Point F m)) (Simul.evalTuplePOVMIn (extractPM hd hr RA)) B ≤ δ + (↑K + ↑m) * ↑d / ↑(Fintype.card F) ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => extractPM hd hr RA) fun (x : Unit) => extractPM hd hr RB) ≤ δ

From the single-codeword conclusions to the simultaneous ones (the paper's Step 4), in the model M at a unit state. If the two players' measurements RA, RB of polynomials in the K + m variables satisfy the three conclusions of the single-codeword theorem against the combined point measurements, with error δ, then their extractions satisfy the three conclusions of the simultaneous theorem against the original point measurements A, B, with error δ + (K + m) d / q for the two point conclusions and δ for the full-tuple one.