Section 12 pasting: switcheroo commuted contraction #
The once-commuted contraction steps and the split-by-g rewrite.
theorem
MIPStarRE.LDT.Pasting.switcherooAggregateFourthTerm_once_commuted_contraction_right
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
(q : SlicePairQuestion params)
:
∑ g : Polynomial params,
(∑ o : Outcome,
leftTensor
((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o)).conjTranspose * ∑ o : Outcome,
leftTensor
((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
MIPStarRE.LDT.Pasting.switcherooAggregateFirstTerm_eq_split_by_g
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
:
(avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) =>
∑ go : Polynomial params × Outcome,
ev ψbi (leftTensor ((M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2))) = switcherooAggregateFirstTerm params ψbi family M
Collapse the split-by-g raw expression back to the first positive
switcheroo term.