Section 12 pasting: complete-part reductions

Complete-part aggregate commutation and scalar error bounds: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooCompletion/CompletePart.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The vendored second bipartite state ψbi : QuantumState (ι × ι) is the symmetric model S : SymModel 𝔓 K, in the vendored argument position; the slice family is an IdxPolyFamily params 𝔓. completePartAggregateCommutation_as_total applies CommutativityPoints.sddOpRel_congr_outcome to S.toVecState, the outcomes agreeing after completePartSubMeas_outcome_unit on both sides.

The two scalar bounds of the vendored file mention no state, operator or measurement, so they are classical: this file imports the vendored file for them, and dependants name them through an explicit open MIPStarRE.LDT.Pasting (…) list.

Not ported

• firstSwitcherooError_le_eighth_stage: classical, imported.
• firstSwitcherooError_le_commutingWithGCompleteError: classical, imported.

References

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

• references/ldt-paper/ld-pasting.tex

theorem MIPRE.LIDT.Co.Pasting.completePartAggregateCommutation_as_total {𝔓 : 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] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma : ℝ) (hcomm : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (switcherooAggregateLeft S params family (completePartProjFamily params family)) (switcherooAggregateRight S params family (completePartProjFamily params family)) gamma) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (completePartTotalProductLeft S params family) (completePartTotalProductRight S params family) gamma

When the left/right aggregate families are re-expressed using the completed one-outcome form, the aggregate commutation bound translates to the complete-part total-product commutation bound.