Section 12 pasting: commuting-with-G incomplete part

Incomplete-part commuting-with-G bounds, cor:commuting-with-G-incomplete: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/CommutingWithG/Incomplete.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 𝔓.

Both bounds compare outcome differences: with T = G^y the complete part, the commutator of G^x_g with 1 - T is minus its commutator with T, and the commutator of 1 - G^x with 1 - G^y is the commutator of G^x with G^y. The vendored proofs check these identities entrywise on Kronecker products; here they are identities in 𝔓, by noncomm_ring, placed by S.L (S.leftTensor_sub).

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.commutingWithGIncomplete_ofComplete {𝔓 : 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 𝔓) (gamma zeta : ℝ) (hcomm : CommutingWithGCompleteStatement params S family gamma zeta) : CommutingWithGIncompleteStatement params S family gamma zeta

Internal form of cor:commuting-with-G-incomplete after applying cor:commuting-with-G-complete.

Source: The proof in references/ldt-paper/ld-pasting.tex:775-816 uses cor:commuting-with-G-complete internally. The paper-facing theorem commutingWithGIncomplete below derives that complete-part commutation statement from the source hypotheses rather than exposing it as a public hypothesis.

theorem MIPRE.LIDT.Co.Pasting.commutingWithGIncomplete {𝔓 : 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) : CommutingWithGIncompleteStatement params strategy.state family gamma zeta

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