Section 12 pasting: half-sandwich flat-chain steps #
This module proves the adjacent-edge estimates for the post-move and combined
flat chains. These estimates are the local inputs to the final chain
composition in the proof of commuteGHalfSandwich_core.
References #
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
Flat-chain step lemmas #
postMoveFlatStep builds the edges within the post-move phase, and
flatChainStep stitches the move-chain prefix and the post-move suffix
into one combined chain.
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatStep
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(gamma zeta : Error)
(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))
(r : ℕ)
(i : Fin (commuteGHalfSandwich_postMoveFlatLength r))
:
SDDOpRel ψbi (uniformDistribution (MoveQ params r)) (commuteGHalfSandwich_postMoveFlatFamily params family r i.castSucc)
(commuteGHalfSandwich_postMoveFlatFamily params family r i.succ)
(commuteGHalfSandwich_postMoveFlatError params gamma zeta r i)
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainStep
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(gamma zeta : Error)
(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))
(r : ℕ)
(i : Fin (commuteGHalfSandwich_flatChainLength r))
:
SDDOpRel ψbi (uniformDistribution (MoveQ params r)) (commuteGHalfSandwich_flatChainFamily params family r i.castSucc)
(commuteGHalfSandwich_flatChainFamily params family r i.succ)
(commuteGHalfSandwich_flatChainError params gamma zeta r i)