The pulling chain, assembled

MIPRE/Background/QLD/Chain.lean and MIPRE/Background/QLD/ChainPhysical.lean prove the eleven displays of lem:qld-pauli-selfcons's derivation one at a time. This file names the terms they run through and reads the displays as bounds on consecutive deviations, which is the form the chaining inequality consumes.

chainT is the chain, on the physical model: ten terms for nine steps. The four displays eq:qld-pulling-0 to -3 are the first cut's (SimulPair.chainS), and everything from -5 on is the physical model's own. The three terms between -3 and -5 are left out, the chain paying nothing for them (SimulPair.chainS_three_mulVec, MirrorSimul.chainS3b_mulVec).

Three of the nine steps are free --- eq:qld-pulling-2 and -2b, then -3a to -5, then -9a --- and the six that are not cost, in order: item 1 of lem:qld-helper, the game's point--point consistency, item 2 of lem:qld-helper, eq:qld-pulling-10 complete, item 2 of lem:qld-helper again at the second cut, and Schwartz--Zippel. The chain's total is nine times their sum, not two to the ninth power, because a chain's deviation telescopes and Cauchy--Schwarz against the constant one turns the squared norm of a sum of nine terms into nine times the sum of their squares (StateModel.sum_snorm_sq_chain_le).

The last thing this file needs that Chain.lean did not have is the cost of eq:qld-pulling-3: sum_uniform_xSqNorm_pt_le reads the game's point--point consistency on the physical model, which reproduces the strategy's expectations for operators that do not see the registers.

Stated in a bipartite model

Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The chain runs in the physical model phys (Anc F m) F m d M Mi.K of a MirrorSimul. The matrix route ran the first four terms on a regrouping mVec of the first cut's state and carried them to the physical cut by an explicit lift (physLift); the first cut is a reading of the physical model's state model, so here the first four terms are the first cut's terms as they stand, and nothing is lifted. That the physical model reproduces the strategy's expectations (bornProb_mVec_ext, xSqNorm_mVec_ext) is the embedding of the model into its physical model with the registers inert (physInert); the steps that read the second cut go through MirrorSimul.bornProb_physVec_bOp. The constants are the matrix ones.

theorem MIPRE.QLD.SimulPair.bornProb_mVec_ext {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {N : BipartiteModel 𝒞 𝒜 ℬ} {S : N.ProjStrat (qldGame hm)} {K : ℕ} {δ : ℝ} (_P : CutSimul N S K δ) (X : 𝒜) (Y : ℬ) : (phys (Anc F m) F m d N K).bornProb ((physInert (Anc F m) F m d N K).ΦA X) ((physInert (Anc F m) F m d N K).ΦB Y) = N.bornProb X Y

The cut the chain runs on reproduces the strategy's own expectations for operators extended by the identity on every register: the model embeds in its physical model with the registers inert (physInert).

theorem MIPRE.QLD.SimulPair.xSqNorm_mVec_ext {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {N : BipartiteModel 𝒞 𝒜 ℬ} {S : N.ProjStrat (qldGame hm)} {K : ℕ} {δ : ℝ} (_P : CutSimul N S K δ) (X : 𝒜) (Y : ℬ) : (phys (Anc F m) F m d N K).xSqNorm ((physInert (Anc F m) F m d N K).ΦA X) ((physInert (Anc F m) F m d N K).ΦB Y) = N.xSqNorm X Y

And so it reproduces the strategy's cross-party deviations.

theorem MIPRE.QLD.SimulPair.sum_uniform_xSqNorm_pt_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {N : BipartiteModel 𝒞 𝒜 ℬ} {S : N.ProjStrat (qldGame hm)} {K : ℕ} {δ : ℝ} (P : CutSimul N S K δ) {ε : ℝ} (hfail : 1 - S.value ≤ ε) (W : Bas) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ k : F, (phys (Anc F m) F m d N K).xSqNorm (ptA P W u k) (ptB P W u k) ≤ 2 * (86 * ε)

The cost of eq:qld-pulling-3: the point measurements' own cross-party deviation, read on the physical model, is the game's point--point consistency and nothing more.

theorem MIPRE.QLD.snorm_sub_eq_zero_of_mulVec {𝒞 : Type u_2} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {X Y : 𝒞} (h : (M.π X) M.ψ = (M.π Y) M.ψ) : M.snorm (X - Y) = 0

A deviation that vanishes on the state has no state-norm.

noncomputable def MIPRE.QLD.MirrorSimul.chainT {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) : ℕ → F → Matrix (PhysReg (Anc F m) F m d Mi.K × PhysReg (Anc F m) F m d Mi.K) (PhysReg (Anc F m) F m d Mi.K × PhysReg (Anc F m) F m d Mi.K) 𝒞

The chain, on the physical model. Ten terms: the four displays eq:qld-pulling-0 to -3 of the first cut, then -5, -7, -9a, -10, -11 and -12. The three terms between -3 and -5 are left out, the chain paying nothing for them.

Equations

• One or more equations did not get rendered due to their size.
• Mi.chainT W v u 0 = fun (a : F) => MIPRE.QLD.SimulPair.chainS Mi.first W v u 0 a
• Mi.chainT W v u 1 = fun (a : F) => MIPRE.QLD.SimulPair.chainS Mi.first W v u 1 a
• Mi.chainT W v u 2 = fun (a : F) => MIPRE.QLD.SimulPair.chainS Mi.first W v u 2 a
• Mi.chainT W v u 3 = fun (a : F) => MIPRE.QLD.SimulPair.chainS Mi.first W v u 3 a
• Mi.chainT W v u x✝ = fun (a : F) => Mi.endOp W v a

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_zero_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 0 a - Mi.chainT W v u 1 a) ^ 2 ≤ δ

Step 0 to 1 is eq:qld-pulling-1, at item 1 of lem:qld-helper's own constant.

theorem MIPRE.QLD.MirrorSimul.sum_snorm_sq_chainT_one_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) : ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 1 a - Mi.chainT W v u 2 a) ^ 2 = 0

Step 1 to 2 is free, being displays eq:qld-pulling-2 and -2b.

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_two_three {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) {ε : ℝ} (hfail : 1 - S.value ≤ ε) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 2 a - Mi.chainT W v u 3 a) ^ 2 ≤ 2 * (86 * ε)

Step 2 to 3 is eq:qld-pulling-3, the insertion, at the game's point--point consistency.

theorem MIPRE.QLD.MirrorSimul.snorm_chainT_three_four {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) (a : F) : (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 3 a - Mi.chainT W v u 4 a) = 0

Step 3 to 4 is free, being displays eq:qld-pulling-3a, -3b, -4 and -5.

theorem MIPRE.QLD.MirrorSimul.chainT_five_sub_four {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) (a : F) : Mi.chainT W v u 5 a - Mi.chainT W v u 4 a = ∑ t : (LIDT.LowIndDegPoly × Anc F m) × Anc F m with Weyl.dotF (chainLabel t.1.1 t.1.2) v = a, Mi.chainP W t * Mi.chainW W u t

Step 4 to 5 is what eq:qld-pulling-5 to -7 bounds: the gap between Alice's pair measurement with her own point measurement beside it and without.

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_four_five {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) {ε : ℝ} (hfail : 1 - S.value ≤ ε) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 4 a - Mi.chainT W v u 5 a) ^ 2 ≤ 4 * δ + 2 * (172 * ε)

And its cost is display eq:qld-pulling-9, item 2 of lem:qld-helper.

theorem MIPRE.QLD.MirrorSimul.chainT_five_eq_six {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) (a : F) : Mi.chainT W v u 5 a = Mi.chainT W v u 6 a

Step 5 to 6 is free, being display eq:qld-pulling-9a: left-multiplying by Bob's own pair measurement, which is the identity.

theorem MIPRE.QLD.MirrorSimul.chainT_six_sub_seven {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) (a : F) : Mi.chainT W v u 6 a - Mi.chainT W v u 7 a = ∑ q ∈ {q : (LIDT.LowIndDegPoly × Anc F m) × LIDT.LowIndDegPoly × Anc F m | chainQShift u q ≠ q.2.1.eval u} with Weyl.dotF (chainLabel q.1.1 q.1.2) v = a, Mi.chainQ W q * Mi.chainV W u q

Step 6 to 7 is eq:qld-pulling-10: what the chain drops is the pairs whose outcomes disagree at the sampled point.

theorem MIPRE.QLD.MirrorSimul.bornProb_bobSand_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (u : LIDT.Point F m) (c : F) (g : LIDT.LowIndDegPoly) : (phys (Anc F m) F m d M Mi.K).bornProb 1 (compHom (Matrix.diagonal fun (x : Anc F m) => Mi.bobSand W u c g)) = (cut1 (Anc F m) F m d M.swap Mi.K).qform ((cut1 (Anc F m) F m d M.swap Mi.K).πA ((ι₁ (Anc F m) F m d M.swap Mi.K).ΦA (hatMats S.PB W u c)) * (cut1 (Anc F m) F m d M.swap Mi.K).πA ((polyMarg Mi.second.SA W).op g) * (cut1 (Anc F m) F m d M.swap Mi.K).πA ((ι₁ (Anc F m) F m d M.swap Mi.K).ΦA (hatMats S.PB W u c)))

Bob's sandwiched marginal, read on the second cut: the sandwich of the second cut's pair measurement by Bob's hatted point measurement, which is what SimulPair.sum_uniform_qform_ne_le bounds at the second cut.

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_six_seven {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) {ε : ℝ} (hfail : 1 - S.value ≤ ε) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 6 a - Mi.chainT W v u 7 a) ^ 2 ≤ δ + 2 * √(172 * ε)

And its cost, which is display eq:qld-pulling-10 complete, read on the second cut.

theorem MIPRE.QLD.MirrorSimul.bobLift_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) : Mi.bobLift 1 = 1

Bob's lift is unital.

theorem MIPRE.QLD.MirrorSimul.bobLift_sub {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (T T' : Matrix (PadAnc F m d Mi.K × Anc F m) (PadAnc F m d Mi.K × Anc F m) ℬ) : Mi.bobLift (T - T') = Mi.bobLift T - Mi.bobLift T'

And additive.

theorem MIPRE.QLD.MirrorSimul.chainT_eight_sub_seven {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) (a : F) : Mi.chainT W v u 8 a - Mi.chainT W v u 7 a = ∑ q ∈ {q : (LIDT.LowIndDegPoly × Anc F m) × LIDT.LowIndDegPoly × Anc F m | chainQShift u q = q.2.1.eval u} with Weyl.dotF (chainLabel q.1.1 q.1.2) v = a, Mi.chainQ W q * Mi.bobLift (1 - (ι₁ (Anc F m) F m d M.swap Mi.K).ΦA (hatMats S.PB W u (q.2.1.eval u)))

Step 7 to 8 is eq:qld-pulling-11: dropping Bob's point measurement from his side.

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_seven_eight {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) {ε : ℝ} (hfail : 1 - S.value ≤ ε) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 7 a - Mi.chainT W v u 8 a) ^ 2 ≤ 4 * δ + 2 * (172 * ε)

And its cost, which is item 2 of lem:qld-helper at the second cut.

theorem MIPRE.QLD.chainQShift_eq_of_coupled {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (u : LIDT.Point F m) {q : (LIDT.LowIndDegPoly × Anc F m) × LIDT.LowIndDegPoly × Anc F m} (hc : ChainCoupled q.1.1 q.2.1 q.1.2 q.2.2) : chainQShift u q = q.2.1.eval u

Coupled pairs agree at every point. The coupling is an identity of polynomials, so evaluating it at the sampled point gives the chain's agreement condition.

theorem MIPRE.QLD.MirrorSimul.chainT_eight_sub_nine {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) (a : F) : Mi.chainT W v u 8 a - Mi.chainT W v u 9 a = ∑ q ∈ {q : (LIDT.LowIndDegPoly × Anc F m) × LIDT.LowIndDegPoly × Anc F m | chainQShift u q = q.2.1.eval u ∧ ¬ChainCoupled q.1.1 q.2.1 q.1.2 q.2.2} with Weyl.dotF (chainLabel q.1.1 q.1.2) v = a, Mi.chainQ W q

Step 8 to 9 is eq:qld-pulling-12: what the chain drops is the pairs that agree at the sampled point without being coupled.

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_eight_nine {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (hd : 1 ≤ d) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 8 a - Mi.chainT W v u 9 a) ^ 2 ≤ ↑m * ↑d / ↑(Fintype.card F)

And its cost is md/q, by Schwartz--Zippel.

The three free steps, averaged

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_one_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 1 a - Mi.chainT W v u 2 a) ^ 2 = 0

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_three_four {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 3 a - Mi.chainT W v u 4 a) ^ 2 = 0

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_five_six {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 5 a - Mi.chainT W v u 6 a) ^ 2 = 0

theorem MIPRE.QLD.sum_mul_const_mul_sum_range {X : Type u_5} [Fintype X] (μ : X → ℝ) (n : ℕ) (f : ℕ → X → ℝ) (c : ℝ) : ∑ x : X, μ x * (c * ∑ k ∈ Finset.range n, f k x) = c * ∑ k ∈ Finset.range n, ∑ x : X, μ x * f k x

Averaging a constant multiple of a chain's steps: the average goes inside.

theorem MIPRE.QLD.MirrorSimul.chainT_zero_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) (a : F) : Mi.chainT W v u 0 a = (phys (Anc F m) F m d M Mi.K).πA (Mi.aliceMTilde W v a)

The chain starts at Alice's exact Pauli measurement on her physical registers.

theorem MIPRE.QLD.MirrorSimul.chainT_nine_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) (W : Bas) (v : Anc F m) (u : LIDT.Point F m) (a : F) : Mi.chainT W v u 9 a = Mi.endOp W v a

And ends at eq:qld-pulling-12.

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_chainT_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) {ε : ℝ} (hfail : 1 - S.value ≤ ε) (hd : 1 ≤ d) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm (Mi.chainT W v u 0 a - Mi.chainT W v u 9 a) ^ 2 ≤ 9 * (10 * δ + 860 * ε + 2 * √(172 * ε) + ↑m * ↑d / ↑(Fintype.card F))

The pulling chain, assembled. Nine steps, of which three are free; the chain's total deviation is at most nine times the sum of the steps', by Cauchy--Schwarz against the constant one.

theorem MIPRE.QLD.MirrorSimul.sum_uniform_snorm_sq_mTildeAnc_endOp_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {δ : ℝ} (Mi : MirrorSimul M S δ) {ε : ℝ} (hfail : 1 - S.value ≤ ε) (hd : 1 ≤ d) (W : Bas) (v : Anc F m) : ∑ u : LIDT.Point F m, uniform (LIDT.Point F m) u * ∑ a : F, (phys (Anc F m) F m d M Mi.K).snorm ((phys (Anc F m) F m d M Mi.K).πA (Mi.aliceMTilde W v a) - Mi.endOp W v a) ^ 2 ≤ 9 * (10 * δ + 860 * ε + 2 * √(172 * ε) + ↑m * ↑d / ↑(Fintype.card F))

Display eq:qld-pulling-cons for Alice: her exact Pauli measurement on her physical registers is close, in summed squared state distance, to the chain's endpoint.