Section 12 pasting: switcheroo expansion

Expansion identities and the left-front contraction bound: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooCompletion/Expansion.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 contraction witness switcherooAggregateLeftFront_contraction places operators by leftTensor (ι₂ := ι) without a state in the vendored file; here it takes the model as an explicit first argument (switcherooAggregateLeftFront_contraction S params family M q), as the witnesses of Co/Pasting/SwitcherooContraction/Split.lean do. It computes the sum in the local algebra 𝔓, where it is ∑_g X_g with switcherooAggregateFourthTermX, and pushes the bound switcherooAggregateFourthTerm_middle_sum_le_one 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. The two pointwise normalizations unfold the ordered and reversed product families by change and merge the placements by S.leftTensor_conjTranspose and S.leftTensor_mul_leftTensor; the averaged expansion is switcherooAggregate_qSDDOp_expand followed by avgOver_add and avgOver_sub, the four averages being the four terms by definitional equality.

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.switcherooAggregateLeftFront_contraction {𝔓 : 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) : ∑ go : MIPStarRE.LDT.Polynomial params × Outcome, star (∑ _u : Unit, S.L ((family.meas q.1).outcome go.1 * (M q.2).outcome go.2)) * ∑ _u : Unit, S.L ((family.meas q.1).outcome go.1 * (M q.2).outcome go.2) ≤ 1

Contraction witness for the final sqrt chi left-front overlap step.

theorem MIPRE.LIDT.Co.Pasting.switcherooPointProductLeft_self_eq_firstSplit_point {𝔓 : 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 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) (go : MIPStarRE.LDT.Polynomial params × Outcome) : S.ev (star ((switcherooPointProductLeft S params family M q).outcome go) * (switcherooPointProductLeft S params family M q).outcome go) = S.ev (S.L ((M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2))

Normalize the pointwise self-product in the final switcheroo left-front step to the split-by-g scalar.

theorem MIPRE.LIDT.Co.Pasting.switcherooPointProductRightLeft_eq_leftFront_point {𝔓 : 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 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) (go : MIPStarRE.LDT.Polynomial params × Outcome) : S.ev (star ((switcherooPointProductRight S params family M q).outcome go) * (switcherooPointProductLeft S params family M q).outcome go) = S.ev (S.L ((family.meas q.1).outcome go.1 * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2))

Normalize the pointwise mixed product in the final switcheroo left-front step into the left-front scalar form.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregate_qSDDOp_expand_avg {𝔓 : 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) => S.qSDDOp (switcherooAggregateLeft S params family M q) (switcherooAggregateRight S params family M q)) = switcherooAggregateFirstTerm params S family M + switcherooAggregateSecondTerm params S family M - switcherooAggregateThirdTerm params S family M - switcherooAggregateFourthTerm params S family M

Average the single-question four-term qSDDOp expansion over the slice-pair distribution.