Section 12 pasting: commuting-with-G complete part

Complete-part commuting-with-G bounds, cor:commuting-with-G-complete: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/CommutingWithG/Complete.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K and the slice family an IdxPolyFamily params 𝔓; the placed families take strategy.state as their first explicit argument. The vendored proofs read strategy.isNormalized, strategy.densityFixed and strategy.permInvState only to pass them to commutativitySwitcheroo_ofCompleteSelfConsistency, Commutativity.comMain and gCompleteSelfConsistency, whose ported forms take no such hypothesis (section "Swap symmetry is a theorem"), so the statements here are the vendored ones, translated, and the proofs no longer read those fields.

The two switcheroo applications are as in the vendored proof: the first, on M = G, gives the point-with-complete-part bound after swapping the two questions and the two families (sddOpRel_swap_questions, Preliminaries.sddOpRel_symm); the second, on the complete-part family, gives the total-product bound. The comparisons with thm:com-main and between the placed families hold by definition, where the vendored proof unfolds them under simpa.

The scalar bound secondSwitcherooError_le_commutingWithGCompleteError mentions no state, operator or measurement, so it is classical: this file imports the vendored file for it, and dependants name it through an explicit open MIPStarRE.LDT.Pasting (…) list.

Not ported

References

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

• references/ldt-paper/ld-pasting.tex

theorem MIPRE.LIDT.Co.Pasting.secondSwitcherooError_le_commutingWithGCompleteError (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hzeta : zeta ≤ 1) (hd_le_q : params.d ≤ params.q) : MIPStarRE.LDT.Pasting.commutativitySwitcherooError zeta zeta (MIPStarRE.LDT.Pasting.commutativitySwitcherooError zeta zeta (MIPStarRE.LDT.Commutativity.comMainError params gamma zeta)) ≤ MIPStarRE.LDT.Pasting.commutingWithGCompleteError params gamma zeta

Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.

The paper's scalar inequality 12·√ζ + 4·√θ₁ ≤ ν₂, where θ₁ = θ(ζ, ζ, comMainError) is the first switcheroo error. The proof uses firstSwitcherooError_le_eighth_stage to bound θ₁ by 36m · eighthSum, then a sqrt/rpow chain to land on ν₂ = commutingWithGCompleteError.

theorem MIPRE.LIDT.Co.Pasting.commutingWithGComplete_ofComMainAndSelfConsistency {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hgamma : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta : zeta ≤ 1) (hd_le_q : params.d ≤ params.q) (hcom : Commutativity.ComMainConclusion params strategy family gamma zeta) (hself : GCompleteSelfConsistencyStatement params strategy.state family zeta) : CommutingWithGCompleteStatement params strategy.state family gamma zeta

Internal form of cor:commuting-with-G-complete after applying thm:com-main and lem:g-complete-self-consistency.

Source: The proof in references/ldt-paper/ld-pasting.tex:721-774 uses thm:com-main, lem:commutativity-switcheroo, and lem:g-complete-self-consistency internally. The paper-facing theorem commutingWithGComplete below derives the first and third inputs from the source hypotheses rather than exposing them as public hypotheses.

theorem MIPRE.LIDT.Co.Pasting.commutingWithGComplete {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (eps delta gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hgamma : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta : zeta ≤ 1) (hd_le_q : params.d ≤ params.q) (hgood : strategy.IsGood eps delta gamma) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) : CommutingWithGCompleteStatement params strategy.state family gamma zeta

cor:commuting-with-G-complete, source-facing form.