The low-individual-degree test in a bipartite model

Phase 3 of planning/mipco-track.md. The one fact about the low-individual-degree test that the soundness of answer reduction uses is the quantum soundness of the seeded CL test, LIDT.Simul.clSoundness. LIDT.Simul.SoundIn M is that fact as a hypothesis on a bipartite model M, in the exact shape of clSoundness: a projective strategy in M passing the seeded test with r codewords with probability at least 1 - ε admits projective measurements of r-tuples of polynomials in the two players' algebras, each consistent with the other player's point measurements and with each other, at the error δ_sim.

• Its tensor-product instance (soundIn_tensor) is clSoundness, and through it the vendored mainFormal: a projective strategy in the tensor-product model of a state on Fin a × Fin b is a TensorProductStrategy (BipartiteModel.ProjStrat.toTensor), and the matrix inconsistency is the model's (inconsistency_eq_tensor).
• Its commuting-operator form (SoundCo: the test is sound in the model of every commuting-operator strategy) is the hypothesis MIPRE.mipco_eq_core_of_stages carries for answer reduction, and Phase 6 of the plan.

The measurements the conclusion extracts are single POVMs (POVMIn) rather than families over a one-point index; the third conclusion keeps the one-point index of clSoundness (BipartiteModel.inconsistency_uniform_unit reads it as a disagreement).

The readings of the conclusions

def MIPRE.LIDT.Simul.tuplePOVMAIn {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (S : M.ProjStrat (CL.clGame hm)) (y : Point F m) : POVMIn (Fin r → F) 𝒜

The first player's point measurements of a projective strategy for the seeded test, read as the tuple of values a point answer carries (the model form of tuplePOVMA).

Equations

• MIPRE.LIDT.Simul.tuplePOVMAIn hm S y = MIPRE.POVMIn.map MIPRE.LIDT.Simul.valsOf (S.PA (MIPRE.LIDT.CL.Question.point y))

def MIPRE.LIDT.Simul.tuplePOVMBIn {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (S : M.ProjStrat (CL.clGame hm)) (y : Point F m) : POVMIn (Fin r → F) ℬ

The second player's point measurements, as for tuplePOVMAIn.

Equations

• MIPRE.LIDT.Simul.tuplePOVMBIn hm S y = MIPRE.POVMIn.map MIPRE.LIDT.Simul.valsOf (S.PB (MIPRE.LIDT.CL.Question.point y))

def MIPRE.LIDT.Simul.evalTuplePOVMIn {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (G : POVMIn (Fin r → LowIndDegPoly) R) (y : Point F m) : POVMIn (Fin r → F) R

A measurement of r-tuples of polynomials, evaluated at a point (the model form of evalTuplePOVM).

Equations

• MIPRE.LIDT.Simul.evalTuplePOVMIn G y = MIPRE.POVMIn.map (fun (g : Fin r → MIPRE.LIDT.LowIndDegPoly) (j : Fin r) => (g j).eval y) G

Soundness in a model

def MIPRE.LIDT.Simul.SoundIn {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : Prop

The seeded CL test is sound in the bipartite model M (def:lidt-sound-in), in the shape of clSoundness: for q a power of two, m ∣ q and d, r ≥ 1, a projective strategy in M passing the seeded test with r codewords with probability at least 1 - ε admits projective measurements GA in the first player's algebra and GB in the second's, of r-tuples of polynomials of individual degree d, whose evaluations at a uniform point are consistent with the other player's point measurements, and which are consistent with each other, all with error δ_sim(ε, q, m, d, r).

Equations

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

The tensor-product instance

theorem MIPRE.LIDT.Simul.tuplePOVMA_toTensor {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} {a b : ℕ} {ψ : Fin a × Fin b → ℂ} (S : (BipartiteModel.tensor ψ).ProjStrat (CL.clGame hm)) (y : Point F m) : (tuplePOVMA hm S.toTensor y).toIn = tuplePOVMAIn hm S y

theorem MIPRE.LIDT.Simul.tuplePOVMB_toTensor {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} {a b : ℕ} {ψ : Fin a × Fin b → ℂ} (S : (BipartiteModel.tensor ψ).ProjStrat (CL.clGame hm)) (y : Point F m) : (tuplePOVMB hm S.toTensor y).toIn = tuplePOVMBIn hm S y

theorem MIPRE.LIDT.Simul.evalTuplePOVM_toIn {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} {n : Type u_5} [Fintype n] [DecidableEq n] (G : ProjectiveMeasurement Unit (Fin r → LowIndDegPoly) (Matrix n n ℂ)) (y : Point F m) : (evalTuplePOVM G y).toIn = evalTuplePOVMIn (G.toPOVM ()).toIn y

theorem MIPRE.LIDT.Simul.soundIn_tensor {a b : ℕ} (ψ : Fin a × Fin b → ℂ) : SoundIn (BipartiteModel.tensor ψ)

The seeded CL test is sound in the tensor-product model of every state on Fin a × Fin b: clSoundness, for the tensor-product strategy the projective strategy is.

The commuting-operator model

def MIPRE.LIDT.Simul.SoundCo : Prop

The seeded CL test is sound in the commuting-operator model (def:lidt-sound-in): in the model of every commuting-operator strategy, whose algebras are the commutant of the second player's operators and its commutant. This is Phase 6 of planning/mipco-track.md, and the hypothesis on the low-individual-degree test of MIPRE.mipco_eq_core_of_stages.

Equations

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