Section 12 pasting: switcheroo split contraction

The split-form contraction and first mixed-term transfer.

Shared switcheroo contraction helper definitions

noncomputable def MIPStarRE.LDT.Pasting.switcherooAggregateFourthTermX {ι : 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) : Polynomial params → Quantum.Op ι

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

Equations

• MIPStarRE.LDT.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 MIPStarRE.LDT.Pasting.switcherooCompletePartTotal_hermitian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (q : SlicePairQuestion params) : Matrix.conjTranspose (completePartSubMeas params family q.1).total = (completePartSubMeas params family q.1).total

The complete-part total operator is Hermitian.

theorem MIPStarRE.LDT.Pasting.switcherooCompletePartTotal_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (q : 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 MIPStarRE.LDT.Pasting.switcherooCompletePartTotal_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (q : SlicePairQuestion params) : (completePartSubMeas params family q.1).total ≤ 1

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

theorem MIPStarRE.LDT.Pasting.switcherooMeasuredOutcome_hermitian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (M : IdxProjSubMeas (Fq params) Outcome ι) (q : SlicePairQuestion params) (o : Outcome) : Matrix.conjTranspose ((M q.2).outcome o) = (M q.2).outcome o

Every outcome of the external projective family is Hermitian.

theorem MIPStarRE.LDT.Pasting.switcherooSliceOutcome_hermitian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (q : SlicePairQuestion params) (g : Polynomial params) : Matrix.conjTranspose ((family.meas q.1).outcome g) = (family.meas q.1).outcome g

Every slice outcome of the completed family is Hermitian.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateFourthTermX_hermitian {ι : 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) : Matrix.conjTranspose (switcherooAggregateFourthTermX params family M q g) = switcherooAggregateFourthTermX params family M q g

The shared X_g sandwich family is Hermitian pointwise.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateFourthTermX_nonneg {ι : 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) : 0 ≤ switcherooAggregateFourthTermX params family M q g

The shared X_g sandwich family is positive semidefinite pointwise.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateFourthTermX_le_one {ι : 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) : switcherooAggregateFourthTermX params family M q g ≤ 1

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

theorem MIPStarRE.LDT.Pasting.switcherooAggregateFourthTermX_sq_le {ι : 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) : 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 MIPStarRE.LDT.Pasting.switcherooAggregateFourthTermX_sum {ι : 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, 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 MIPStarRE.LDT.Pasting.switcherooAggregateFourthTerm_middle_sum_le_one {ι : 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) : ∑ 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 MIPStarRE.LDT.Pasting.switcherooAggregateFourthTerm_split_close_once_commuted {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (chi : Error) (hcomm : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (switcherooPointProductLeft params family M) (switcherooPointProductRight params family M) chi) : |switcherooAggregateFourthTerm params ψbi family M - avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) => ∑ go : Polynomial params × Outcome, ev ψbi (leftTensor ((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 MIPStarRE.LDT.Pasting.switcherooAggregateFourthTerm_once_commuted_contraction_left {ι : 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)) * (∑ 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 ≤ 1

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

theorem MIPStarRE.LDT.Pasting.switcherooAggregateFourthTerm_once_commuted_close_mixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (zeta : Error) (hselfG : GCompleteSelfConsistencyStatement params ψbi family zeta) : |(avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) => ∑ g : Polynomial params, ∑ o : Outcome, ev ψbi (leftTensor ((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))) - avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) => ∑ g : Polynomial params, ∑ o : Outcome, ev ψbi (leftTensor ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o) * rightTensor ((family.meas q.1).outcome g))| ≤ √zeta

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