The model chain, part 5: the simultaneous contract in a model

The model counterpart of the repository's MIPRE/Background/LIDT/Simultaneous.lean (blueprint thm:lidt-cl-soundness, through lem:lidt-ldc and lem:lidt-ldc-error; not a vendored file: its matrix statement MIPRE.LIDT.Simul.clSoundness serves the tensor instance soundIn_tensor and stays), in the port of planning/c6b-plan.md (milestone M14, unit M14-5). It closes the model chain: in any bipartite model M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ with the instance set of MIPRE.LIDT.Simul.SoundIn, the canonical-line theorem in M implies the simultaneous contract in M (soundIn_of_soundLidtIn : SoundLidtIn M → SoundIn M).

The proof is that of clSoundness, step for step. A strategy for the seeded test with r codewords in m variables is played as one with a single codeword in K + m variables (padded, Co/Chain/Padding.lean), failing at most 9 (K + 1) times as often; the single-codeword theorem clSoundness_ldc_one_deltaCL (Co/Chain/Reduction.lean) applies to it, from SoundLidtIn M; and extracted_conclusions (Co/Chain/Extraction.lean) reads r-tuples of polynomials in the original variables off its measurements (clSoundness_padded). With K + m = padM m r the error is absorbed into δ_sim by the classical deltaCL_padded_le; when m + r > q there is no room to pad, δ_sim ≥ 1 (one_le_deltaSim), and the one-outcome measurements constPM do, since every inconsistency at a unit state is at most one (inconsistency_le_one).

Reused by import. The classical part of Simultaneous.lean (the choice of M, the error δ_sim and its bounds) is named through an explicit open MIPRE.LIDT.Simul (…) list: padM, le_padM, padM_le_mul, padM_dvd, deltaSim, deltaCL_padded_le, one_le_deltaSim, sum_uniform_one, and SoundIn, tuplePOVMAIn, tuplePOVMBIn, evalTuplePOVMIn of ModelSoundness.lean.

Not ported

clSoundness_padded, constPM and inconsistency_le_one are declared here under their names, for POVMs in the algebras of M; clSoundness_padded takes SoundLidtIn M, and its measurements are POVMIns with IsPVMIn carried beside them. Of the rest of Simultaneous.lean:

• clSoundness: replaced by soundIn_of_soundLidtIn, whose conclusion is SoundIn M, the statement of clSoundness read in M.
• padM, le_padM, padM_le, padM_le_mul, padM_dvd, simA, deltaSim, forty_le_simA, clA_add_one_le_simA, rpow_le_rpow_simA, deltaCL_padded_le, one_le_deltaSim: classical, imported.

New here

• constPM_isPVMIn: the one-outcome measurement is projective (the matrix constPM is a ProjectiveMeasurement, so its projectivity is a field there).
• soundIn_of_soundLidtIn: above.

The padded chain

theorem MIPRE.LIDT.Co.Chain.clSoundness_padded {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type} [Field F] [Fintype F] [DecidableEq F] {K m d r : ℕ} [NeZero m] (h : SoundLidtIn 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 : M.ProjStrat (CL.clGame hm)) (ε : ℝ) (hε : 0 ≤ ε) (hS : 1 - ε ≤ S.value) : ∃ (GA : POVMIn (Fin r → LowIndDegPoly) 𝒜) (GB : POVMIn (Fin r → LowIndDegPoly) ℬ), IsPVMIn GA.op ∧ IsPVMIn GB.op ∧ M.inconsistency (uniform (Point F m)) (Simul.tuplePOVMAIn hm S) (Simul.evalTuplePOVMIn GB) ≤ deltaCL (Fintype.card F) (K + m) d (9 * (↑K + 1) * ε) + (↑K + ↑m) * ↑d / ↑(Fintype.card F) ∧ M.inconsistency (uniform (Point F m)) (Simul.evalTuplePOVMIn GA) (Simul.tuplePOVMBIn hm S) ≤ deltaCL (Fintype.card F) (K + m) d (9 * (↑K + 1) * ε) + (↑K + ↑m) * ↑d / ↑(Fintype.card F) ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => GA) fun (x : Unit) => GB) ≤ deltaCL (Fintype.card F) (K + m) d (9 * (↑K + 1) * ε)

The simultaneous contract in the model M, at a padding K ≥ r (the model form of MIPRE.LIDT.Simul.clSoundness_padded): if the canonical-line theorem holds in M, a projective strategy for the seeded test with r codewords passing with probability at least 1 - ε admits projective measurements of r-tuples of polynomials, with error δ_CL(9 (K + 1) ε, q, K + m, d) plus (K + m) d / q on the two point conclusions.

The trivial regime

def MIPRE.LIDT.Co.Chain.constPM {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {A : Type u_5} [Fintype A] [DecidableEq A] (a₀ : A) : POVMIn A R

A measurement with a single outcome a₀: the identity at a₀, zero elsewhere.

Equations

• MIPRE.LIDT.Co.Chain.constPM a₀ = { mats := fun (a : A) => ⟨if a = a₀ then 1 else 0, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

theorem MIPRE.LIDT.Co.Chain.constPM_isPVMIn {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {A : Type u_5} [Fintype A] [DecidableEq A] (a₀ : A) : IsPVMIn (constPM a₀).op

The one-outcome measurement is projective.

theorem MIPRE.LIDT.Co.Chain.inconsistency_le_one {𝒞 : 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_6} {Λ : Type u_7} [Fintype X] [Nonempty X] [Fintype Λ] [DecidableEq Λ] (hψ : ‖M.ψ‖ = 1) (P : X → POVMIn Λ 𝒜) (Q : X → POVMIn Λ ℬ) : M.inconsistency (uniform X) P Q ≤ 1

At a unit state, the inconsistency of two families of POVMs on a uniform index is at most one (the model form of MIPRE.LIDT.Simul.inconsistency_le_one).

The theorem

theorem MIPRE.LIDT.Co.Chain.soundIn_of_soundLidtIn {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : SoundLidtIn M) : Simul.SoundIn M

The canonical-line theorem in a model implies the simultaneous contract in it (the model form of MIPRE.LIDT.Simul.clSoundness, blueprint thm:lidt-cl-soundness through lem:lidt-ldc): if SoundLidtIn M, then SoundIn M. For m + r ≤ q the strategy is padded to K + m = padM m r variables and the error of clSoundness_padded absorbed into δ_sim by deltaCL_padded_le; otherwise δ_sim ≥ 1 and the one-outcome measurements constPM do.