Section 11 commutativity: the phase-1 evaluated-slice insertion bound

Closeness-of-inner-product side conditions for inserting Bob's measurement into the first evaluated-slice step of the paper proof, and the phase-1 insertion estimate itself: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/EvaluatedSliceBounds/PhaseOneThree.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The left placement of the vendored leftTensor (ι₂ := ι) is the model's S.L, so leftTensor_normalizationConditionSquare_le_one takes the symmetric model S as an explicit first argument, as M3's placement lemmas do (planning/c6b-plan.md, "Departures in M3 and M5"). evaluatedSlice_phaseOne_insert_bound drops the vendored hypothesis hnorm : strategy.state.IsNormalized, a theorem of the model, and its hcombined_snd is stated with evaluatedPointFamilyLeft strategy.state and Preliminaries.totalSandwichFamily strategy.state, which take the model explicitly in the port.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPRE.LIDT.Co.Commutativity.leftTensor_normalizationConditionSquare_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {OutcomeA : Type u_3} {OutcomeB : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) : ∑ a : OutcomeA, (∑ b : OutcomeB, S.L (Q.outcome b * P.outcome a * Q.outcome b)) * star (∑ b : OutcomeB, S.L (Q.outcome b * P.outcome a * Q.outcome b)) ≤ 1

The left placement of the sandwiched totals ∑_b Q_b P_a Q_b satisfies the normalization condition ∑_a (∑_b L(Q_b P_a Q_b)) (∑_b L(Q_b P_a Q_b))^* ≤ 1 of closenessOfIP.

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSlicePointMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) : IdxMeas (MIPStarRE.LDT.Point params.next) (MIPStarRE.LDT.Fq params) 𝔓

View the params.next point measurement with the outcome type rewritten as Fq params.

Equations

• MIPRE.LIDT.Co.Commutativity.evaluatedSlicePointMeas params strategy u = (strategy.pointMeasurement u).toMeasurement

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSlice_phaseOne_insert_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (zeta : ℝ) (family : IdxPolyFamily params 𝔓) (hcombined_snd : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft strategy.state params family q.2) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => Preliminaries.totalSandwichFamily strategy.state (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.2) (4 * zeta)) : have 𝒟 := MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params); have inserted := fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ b : MIPStarRE.LDT.Fq params, ∑ a : MIPStarRE.LDT.Fq params, strategy.state.ev (strategy.state.L ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).outcome a) * (Preliminaries.totalSandwichFamily strategy.state (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.2).outcome b); |(MIPStarRE.LDT.avgOver 𝒟 fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, evaluatedSliceABABTerm params strategy family q ab) - MIPStarRE.LDT.avgOver 𝒟 inserted| ≤ 2 * √zeta

Phase-1 insertion step for evaluatedSlice_scalar_chain_bound.

This is the eq:gcom8 -> eq:apply-add-an-a-once comparison: transport the pointwise consSubMeas control to the second coordinate of an evaluated-slice question, then apply closenessOfIP with the left-sandwich family G_a^{u,x} G_b^{v,y} G_a^{u,x}. The inserted term is kept in the explicit G^y \otimes A_b^{v,y} form coming from totalSandwichFamily.