Documentation

MIPRE.Background.LIDT.Co.Pasting.SwitcherooCompletion.SecondTerm

Section 12 pasting: switcheroo second term #

Complete-part self-consistency and the second switcheroo term: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooCompletion/SecondTerm.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 switcheroo_second_aggregate_term_close is dropped, normalization being a theorem of the model (section "Swap symmetry is a theorem"): callers pass params S family M zeta hselfG.

completePartProjFamily_selfConsistency_generic is qSDD_completePart_le_slice averaged, the placed families agreeing by definition. switcheroo_second_aggregate_term_close reads the second term as an iterated average by avgOver_uniform_prod_swap (in place of the vendored avgOver_uniform_equiv along Prod.swap followed by avgOver_uniform_prod) and merges the placements by S.leftTensor_mul_leftTensor, the switch sandwich doing the rest. The two opTensor forms of the centres reduce to S.L A * S.R B, which is S.opTensor A B by definition, after pulling the outcome sum through S.R by S.rightTensor_finset_sum.

Not ported #

Nothing: every declaration of the vendored file is ported here.

References #

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

source
theorem MIPRE.LIDT.Co.Pasting.completePartProjFamily_selfConsistency_generic {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) (hself : GCompleteSelfConsistencyStatement params S family zeta) :
S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (switcherooSelfConsistencyLeft S params (completePartProjFamily params family)) (switcherooSelfConsistencyRight S params (completePartProjFamily params family)) zeta

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

source
theorem MIPRE.LIDT.Co.Pasting.switcheroo_second_aggregate_term_close {𝔓 : 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) :
have secondTerm := switcherooAggregateSecondTerm params S family M; have commonTerm := MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) fun (y : MIPStarRE.LDT.Pasting.SliceQuestion params) => Preliminaries.middleSandwichExpectation S (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.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.

source
theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateMGCenterComplete_eq_opTensor_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.SliceQuestion params)) fun (y : MIPStarRE.LDT.Pasting.SliceQuestion params) => Preliminaries.middleSandwichExpectation S (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (completePartProjFamily params family) (M y).total) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => S.ev (S.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.

source
theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateTarget_eq_opTensor_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 𝔓) :
switcherooAggregateTarget params S family M = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => S.ev (S.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.