Section 11 commutativity: evaluated-slice averaged expansion

Averaged evaluated-slice expansion of qSDDOp into the four projector terms BAB + ABA - BABA - ABAB, used to reduce the commutation to per-projector estimates: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/EvaluatedSliceCommutation/Averages.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The vendored proof of the expansion works with the Kronecker placements leftTensor (ι₂ := ι) A and proves their self-adjointness through Matrix.PosSemidef; here the commutator identity (AB − BA)^*(AB − BA) = BAB + ABA − BABA − ABAB is proved in the local algebra 𝔓 and placed once by strategy.state.L. The two swap identities are one reindexing helper applied twice.

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.evaluatedSliceCommutation_qSDDOp_avg_expand {𝔓 : 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) (family : IdxPolyFamily params 𝔓) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => strategy.state.qSDDOp (evaluatedSliceProductLeft params strategy family q) (evaluatedSliceProductRight params strategy family q)) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, (evaluatedSliceBABTerm params strategy family q ab + evaluatedSliceABATerm params strategy family q ab - evaluatedSliceBABATerm params strategy family q ab - evaluatedSliceABABTerm params strategy family q ab)

Expand the averaged evaluated-slice qSDDOp into the four projector terms BAB + ABA - BABA - ABAB.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSliceCommutation_avg_swap_terms {𝔓 : 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) (family : IdxPolyFamily params 𝔓) : ((MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, evaluatedSliceBABTerm params strategy family q ab) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, evaluatedSliceABATerm params strategy family q ab) ∧ (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, evaluatedSliceBABATerm params strategy family q ab) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, evaluatedSliceABABTerm params strategy family q ab

Swapping the evaluated question and outcome identifies the averaged BAB/ABA terms and the averaged BABA/ABAB terms.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSliceCommutation_qSDDOp_avg_eq {𝔓 : 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) (family : IdxPolyFamily params 𝔓) : strategy.state.sddErrorOp (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (evaluatedSliceProductLeft params strategy family) (evaluatedSliceProductRight params strategy family) = 2 * ((MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, evaluatedSliceABATerm params strategy family q ab) - MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, evaluatedSliceABABTerm params strategy family q ab)

Averaged evaluated-slice qSDDOp collapses to the paper's two scalar terms after swapping the sampled questions and outcomes.