Section 12 pasting: half-sandwich move-back chain

This module contains the reverse part of the finite commutation chain used in lem:commute-g-half-sandwich. After the initial move chain and the flat post-move comparison, these families bring the leading completed-slice measurement back to the position required by the rotated half-sandwich endpoint.

References

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

Move-back chain

The moveBackChainFamily and its endpoint lemmas reverse the commutation to bring the leading Ĝ back into position.

noncomputable def MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveBackChainFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) : Fin (r + 1) → IdxOpFamily (MoveQ params (r + 1)) (MoveO params (r + 1)) (ι × ι)

Reverse the move-chain indexing so that the leading completed-slice factor is moved back through the product.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_secondSliceLift_moveFamily_eq_swappedFrontMoveStepMid {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) (q : MoveQ params (r + 1)) (ogs : MoveO params (r + 1)) : (commuteGHalfSandwich_secondSliceLiftFamily params family r (commuteGHalfSandwich_moveFamily params family r) q).outcome ogs = (commuteGHalfSandwich_moveStepMidFamily params family r ((moveTailSwappedFrontQuestionEquiv params r) q)).outcome ((moveTailSwappedFrontOutcomeEquiv params r) ogs)

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_commute_eq_swappedFrontMoveStepTarget {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) (q : MoveQ params (r + 1)) (ogs : MoveO params (r + 1)) : (commuteGHalfSandwich_commuteFamily params family (r + 1) q).outcome ogs = (commuteGHalfSandwich_moveStepTargetFamily params family r ((moveTailSwappedFrontQuestionEquiv params r) q)).outcome ((moveTailSwappedFrontOutcomeEquiv params r) ogs)

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_commute_to_moveBackChainFamily_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) {r : ℕ} (hsc : SDDRel ψbi (uniformDistribution (SliceQuestion params)) (gHatSelfConsistencyLeftFamily params family) (gHatSelfConsistencyRightFamily params family) (gHatSelfConsistencyError zeta)) : SDDOpRel ψbi (uniformDistribution (MoveQ params (r + 1))) (commuteGHalfSandwich_commuteFamily params family (r + 1)) (commuteGHalfSandwich_moveBackChainFamily params family r 0) (gHatSelfConsistencyError zeta)

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveBackChainFamily_zero_eq_secondSliceLift_moveFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) (q : MoveQ params (r + 1)) (ogs : MoveO params (r + 1)) : (commuteGHalfSandwich_moveBackChainFamily params family r 0 q).outcome ogs = (commuteGHalfSandwich_secondSliceLiftFamily params family r (commuteGHalfSandwich_moveFamily params family r) q).outcome ogs