Section 12 pasting: half-sandwich chain assembly

This module assembles the move chain, the flat post-move chain, and the move-back chain to prove the operator-family estimate used by lem:commute-g-half-sandwich.

References

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

Main theorem: commuteGHalfSandwich_core

The flat-chain construction and the final error envelope.

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_core {ι : 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) (hsc : SDDRel ψbi (uniformDistribution (SliceQuestion params)) (gHatSelfConsistencyLeftFamily params family) (gHatSelfConsistencyRightFamily params family) (gHatSelfConsistencyError zeta)) (hcom : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (gHatPairProductLeft params family) (gHatPairProductRight params family) (gHatCommutationError params gamma zeta)) : SDDOpRel ψbi (uniformDistribution (PointTuple params k)) (gHatHalfSandwichLeft params family k) (gHatHalfSandwichRight params family k) (commuteGHalfSandwichError params gamma zeta k)

The staged move-commute-move chain for commuteGHalfSandwich.

Constructs the sequence of 3k - 4 intermediate bipartite operator families joined by 3k - 5 elementary edges. These edges repeatedly move Ĝ₁ through the product Ĝ₁ · Ĝ₂ · ⋯ · Ĝₖ using self-consistency (move to right tensor, error 2ζ) and pairwise commutation (swap past neighbor, error ν₃), then compose them in one call to sddOpRel_chain, avoiding the exponential loss from recursive macro-chain composition.

Paper reference: lem:commute-g-half-sandwich computation in ld-pasting.tex lines 881–914.