Section 12 pasting: switcheroo split contraction

The split-form contraction and the first mixed-term transfer: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooContraction/Split.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 vendored hypothesis hnorm : ψbi.IsNormalized of switcherooAggregateFourthTerm_split_close_once_commuted and switcherooAggregateFourthTerm_once_commuted_close_mixed is dropped, normalization being a theorem of the model (section "Swap symmetry is a theorem"): callers pass params S family M chi hcomm and params S family M zeta hselfG.

The two contraction witnesses place operators by leftTensor (ι₂ := ι) without a state in the vendored file; here they take the model as an explicit first argument (switcherooAggregateFourthTerm_split_contraction S params family M q, and the same for switcherooAggregateFourthTerm_once_commuted_contraction_left), as M3's and M7's placement lemmas do. Both are 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; the Hermitian facts come from IsSelfAdjoint.of_nonneg rather than Matrix.PosSemidef.

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

Shared switcheroo contraction helper definitions

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTermX {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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) : MIPStarRE.LDT.Polynomial params → 𝔓

The g-indexed sandwich family used in the once-commuted contraction bounds.

Equations

• MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTermX params family M q g = ∑ o : Outcome, (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o

theorem MIPRE.LIDT.Co.Pasting.switcherooCompletePartTotal_hermitian {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) : star (completePartSubMeas params family q.1).total = (completePartSubMeas params family q.1).total

The complete-part total operator is Hermitian.

theorem MIPRE.LIDT.Co.Pasting.switcherooCompletePartTotal_sq {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) : (completePartSubMeas params family q.1).total * (completePartSubMeas params family q.1).total = (completePartSubMeas params family q.1).total

The complete-part total operator is idempotent.

theorem MIPRE.LIDT.Co.Pasting.switcherooCompletePartTotal_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) : (completePartSubMeas params family q.1).total ≤ 1

The complete-part total operator is bounded by the identity.

theorem MIPRE.LIDT.Co.Pasting.switcherooMeasuredOutcome_hermitian {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) (o : Outcome) : star ((M q.2).outcome o) = (M q.2).outcome o

Every outcome of the external projective family is Hermitian.

theorem MIPRE.LIDT.Co.Pasting.switcherooSliceOutcome_hermitian {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) (g : MIPStarRE.LDT.Polynomial params) : star ((family.meas q.1).outcome g) = (family.meas q.1).outcome g

Every slice outcome of the completed family is Hermitian.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTermX_hermitian {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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 (switcherooAggregateFourthTermX params family M q g) = switcherooAggregateFourthTermX params family M q g

The shared X_g sandwich family is Hermitian pointwise.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTermX_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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) : 0 ≤ switcherooAggregateFourthTermX params family M q g

The shared X_g sandwich family is positive pointwise.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTermX_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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) : switcherooAggregateFourthTermX params family M q g ≤ 1

The shared X_g sandwich family is bounded by the identity pointwise.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTermX_sq_le {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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) : switcherooAggregateFourthTermX params family M q g * switcherooAggregateFourthTermX params family M q g ≤ switcherooAggregateFourthTermX params family M q g

The shared X_g sandwich family satisfies X_g^2 ≤ X_g.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTermX_sum {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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, switcherooAggregateFourthTermX params family M q g = ∑ o : Outcome, (M q.2).outcome o * (completePartSubMeas params family q.1).total * (M q.2).outcome o

Summing the shared X_g family collapses to the middle sandwich term.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm_middle_sum_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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) : ∑ o : Outcome, (M q.2).outcome o * (completePartSubMeas params family q.1).total * (M q.2).outcome o ≤ 1

The middle sandwich sum used in the contraction bounds is a contraction.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm_split_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, S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1) * star (S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1)) ≤ 1

Contraction witness for the first sqrt chi switcheroo transfer.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm_split_close_once_commuted {𝔓 : 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 𝔓) (chi : ℝ) (hcomm : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (switcherooPointProductLeft S params family M) (switcherooPointProductRight S params family M) chi) : |switcherooAggregateFourthTerm params S family M - 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 ((completePartSubMeas params family q.1).total * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1))| ≤ √chi

The first sqrt chi step in the fourth-term switcheroo chain.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm_once_commuted_contraction_left {𝔓 : 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, (∑ 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)) * 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)) ≤ 1

Left-action contraction witness for the first sqrt zeta transfer.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm_once_commuted_close_mixed {𝔓 : 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 𝔓) (zeta : ℝ) (hselfG : GCompleteSelfConsistencyStatement params S family zeta) : |(MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => ∑ g : MIPStarRE.LDT.Polynomial params, ∑ o : Outcome, S.ev (S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o * (family.meas q.1).outcome g))) - MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => ∑ g : MIPStarRE.LDT.Polynomial params, ∑ o : Outcome, S.ev (S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o) * S.R ((family.meas q.1).outcome g))| ≤ √zeta

The first sqrt zeta step in the fourth-term switcheroo chain.