Section 12 pasting: commuting-with-G incomplete part

Incomplete-part commuting-with-G bounds.

theorem MIPStarRE.LDT.Pasting.commutingWithGIncomplete_ofComplete {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hcomm : CommutingWithGCompleteStatement params ψbi family gamma zeta) : CommutingWithGIncompleteStatement params ψbi 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 MIPStarRE.LDT.Pasting.commutingWithGIncomplete {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (eps delta gamma zeta : Error) (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.