Full-slice qSDDOp averaging identity

Averaging identities expanding the full-slice qSDDOp and proving the scalar commutation identity fullSliceCommutation_qSDDOp_avg_eq: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Transport/FullSlice/Bridges/QSDD.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions"). This scalar expansion is used by the full-slice transport theorems that compare the quartic scalar averages appearing in commutativity-G.tex.

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, as in EvaluatedSliceCommutation/Averages.lean.

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.fullSliceCommutation_qSDDOp_avg_expand_full {𝔓 : 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.FullSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.FullSliceQuestion params) => strategy.state.qSDDOp (fullSliceProductLeft params strategy family q) (fullSliceProductRight params strategy family q)) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.FullSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.FullSliceQuestion params) => ∑ gh : MIPStarRE.LDT.Commutativity.FullSliceOutcome params, (fullSliceBABTerm params strategy family q gh + fullSliceABATerm params strategy family q gh - fullSliceBABATerm params strategy family q gh - fullSliceABABTerm params strategy family q gh)

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

theorem MIPRE.LIDT.Co.Commutativity.fullSliceCommutation_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)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => fullSliceProductLeft params strategy family (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => fullSliceProductRight params strategy family (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) = 2 * (fullSliceABAAvg params strategy family - fullSliceABABAvg params strategy family)

Paper eq:gcomterms (commutativity-G.tex lines 286-290).

Full-slice analog of evaluatedSliceCommutation_qSDDOp_avg_eq: the pulled-back sddErrorOp on the full-slice product equals 2·(ABAAvg − ABABAvg) after using projectivity and the (x,g) ↔ (y,h) symmetry to collapse BAB + ABA − BABA − ABAB into the two surviving scalar quartic terms.