Section 12 pasting: commute G half-sandwich

Public statement for lem:commute-g-half-sandwich.

References

• references/ldt-paper/ld-pasting.tex
• blueprint/src/chapter/ch09_pasting.tex

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_ofGHatFacts {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) (k : ℕ) (hk : 2 ≤ k) (hzeta_le : zeta ≤ 1) (hfacts : GHatFactsStatement params ψbi family gamma zeta) : CommuteGHalfSandwichStatement params ψbi family gamma zeta k

Internal form of lem:commute-g-half-sandwich after applying cor:G-hat-facts.

Source: The proof in references/ldt-paper/ld-pasting.tex:871-910 uses the completed-measurement self-consistency and commutation estimates from cor:G-hat-facts. The paper-facing theorem commuteGHalfSandwich below derives those estimates from the source hypotheses.

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich {ι : 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_le : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le : zeta ≤ 1) (hdq_le : 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) (k : ℕ) (hk : 2 ≤ k) : CommuteGHalfSandwichStatement params strategy.state family gamma zeta k

lem:commute-g-half-sandwich, source-facing form.