Section 12 pasting: switcheroo commuted contraction

The once-commuted contraction step and the split-by-g rewrite: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooContraction/Commuted.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 𝔓 and the auxiliary family M an IdxProjSubMeas (Fq params) Outcome 𝔓.

The right-action contraction witness places operators by leftTensor (ι₂ := ι) without a state in the vendored file; here it takes the model as an explicit first argument (switcherooAggregateFourthTerm_once_commuted_contraction_right S params family M q), as the witnesses of Co/Pasting/SwitcherooContraction/Split.lean do. It is proved in the local algebra 𝔓 and pushed through S.L by S.leftTensor_le_one, in place of the vendored conjTranspose_opTensor and opTensor_mono_left with the identity on the second factor. switcherooAggregateFirstTerm_eq_split_by_g inserts G = ∑_g G_g in the local algebra and pulls the sum out through S.leftTensor_finset_sum and S.ev_sum, as switcherooAggregateFourthTerm_eq_split does.

Not ported

Nothing: every declaration of the vendored file is ported here.

References

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

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

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm_once_commuted_contraction_right {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) : ∑ g : MIPStarRE.LDT.Polynomial params, star (∑ o : Outcome, S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o)) * ∑ o : Outcome, S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o) ≤ 1

Right-action contraction witness for the second sqrt zeta transfer.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFirstTerm_eq_split_by_g {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => ∑ go : MIPStarRE.LDT.Polynomial params × Outcome, S.ev (S.L ((M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2))) = switcherooAggregateFirstTerm params S family M

Collapse the split-by-g raw expression back to the first positive switcheroo term.