Section 12 pasting: switcheroo completion bounds

Completion and first-stage switcheroo error bounds, lem:commutativity-switcheroo: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooCompletion.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, and a strategy is a SymStrat params.next 𝔓 K; the slice family is an IdxPolyFamily params 𝔓 and the auxiliary family M an IdxProjSubMeas (Fq params) Outcome 𝔓. The vendored hypotheses hnorm : ψbi.IsNormalized and hfix : swapDensity ψbi.density = ψbi.density are dropped, both being theorems of the model (section "Swap symmetry is a theorem"): callers pass switcherooCompletePartCenter_eq_target params S family M and commutativitySwitcheroo_ofCompleteSelfConsistency params S family M zeta omega chi hselfG hselfM hcomm. commutativitySwitcheroo no longer reads strategy.permInvState, strategy.isNormalized or strategy.densityFixed.

The swap of the two centres is S.ev_opTensor_swap_of_density_fixed, which needs no hypothesis. The assembly compares the four terms of the expansion with the one centre G ⊗ M: the first by the switch sandwich on M, the second by the switch sandwich on the complete part followed by the centre swap, and the third and fourth through the fourth-term chain of Co/Pasting/SwitcherooCompletion/FourthTermChain.lean. The arithmetic is one linarith on the unfolded absolute-value bounds, in place of the vendored nlinarith steps; it proves the displayed 6√ζ + 6√ω + 4√χ from the sharper 6√ζ + 2√ω + 4√χ.

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.switcherooCompletePartCenter_eq_target {𝔓 : 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) = switcherooAggregateTarget params S family M

The complete-part M ⊗ G centre equals the G ⊗ M switcheroo target.

theorem MIPRE.LIDT.Co.Pasting.commutativitySwitcheroo_ofCompleteSelfConsistency {𝔓 : 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 omega chi : ℝ) (hselfG : GCompleteSelfConsistencyStatement params S family zeta) (hselfM : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (switcherooSelfConsistencyLeft S params M) (switcherooSelfConsistencyRight S params M) omega) (hcomm : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (switcherooPointProductLeft S params family M) (switcherooPointProductRight S params family M) chi) : CommutativitySwitcherooStatement params S family M zeta omega chi

Internal form of lem:commutativity-switcheroo after applying lem:g-complete-self-consistency.

Source: The proof in references/ldt-paper/ld-pasting.tex:560-706 uses the complete-part self-consistency conclusion internally. The paper-facing theorem commutativitySwitcheroo below derives it from the source strong self-consistency hypothesis rather than exposing it as a public hypothesis.

theorem MIPRE.LIDT.Co.Pasting.commutativitySwitcheroo {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) (zeta omega chi : ℝ) (hself : family.StronglySelfConsistent strategy.state zeta) (hselfM : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (switcherooSelfConsistencyLeft strategy.state params M) (switcherooSelfConsistencyRight strategy.state params M) omega) (hcomm : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (switcherooPointProductLeft strategy.state params family M) (switcherooPointProductRight strategy.state params family M) chi) : CommutativitySwitcherooStatement params strategy.state family M zeta omega chi

lem:commutativity-switcheroo, source-facing form.