Section 12 pasting: switcheroo second term

Complete-part self-consistency and the second switcheroo term.

theorem MIPStarRE.LDT.Pasting.completePartProjFamily_selfConsistency_generic {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) (hself : GCompleteSelfConsistencyStatement params ψbi family zeta) : SDDRel ψbi (uniformDistribution (SliceQuestion params)) (switcherooSelfConsistencyLeft params (completePartProjFamily params family)) (switcherooSelfConsistencyRight params (completePartProjFamily params family)) zeta

The one-outcome complete-part family inherits self-consistency from the slice family.

theorem MIPStarRE.LDT.Pasting.switcheroo_second_aggregate_term_close {ι : 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) : have secondTerm := switcherooAggregateSecondTerm params ψbi family M; have commonTerm := avgOver (uniformDistribution (SliceQuestion params)) fun (y : SliceQuestion params) => Preliminaries.middleSandwichExpectation ψbi (uniformDistribution (SliceQuestion params)) (completePartProjFamily params family) (M y).total; |secondTerm - commonTerm| ≤ 2 * √zeta

The second positive switcheroo term is close to the swapped center coming from the complete-part family.

This aggregate form matches the four-term qSDDOp expansion: the projective family in the sandwich is the one-outcome complete part G^x, not the original slice-outcome family.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateMGCenterComplete_eq_opTensor_avg {ι : 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 (SliceQuestion params)) fun (y : SliceQuestion params) => Preliminaries.middleSandwichExpectation ψbi (uniformDistribution (SliceQuestion params)) (completePartProjFamily params family) (M y).total) = avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) => ev ψbi (opTensor (M q.2).total (completePartSubMeas params family q.1).total)

The complete-part M ⊗ G switcheroo center, expressed as a slice-pair opTensor average over the M-totals and complete-part G-totals.

theorem MIPStarRE.LDT.Pasting.switcherooAggregateTarget_eq_opTensor_avg {ι : 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 ι) : switcherooAggregateTarget params ψbi family M = avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) => ev ψbi (opTensor (completePartSubMeas params family q.1).total (M q.2).total)

The G ⊗ M switcheroo center, expressed as a slice-pair opTensor average over the complete-part G-totals and M-totals.