Section 12 pasting: half-sandwich move chain

This module defines the recursive sequence of operator families which moves a completed-slice factor through the half-product. The adjacent edges in this sequence are supplied by the self-consistency estimate for the completed-slice family.

References

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

Move chain: recursive family, step lemma, and aggregate

The recursive moveChainFamily indexed over Fin (r+1), with the step lemma moveChain_step and the aggregate lemma move_chain that composes the r self-consistency edges.

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

The finite sequence of operator families which moves the distinguished completed-slice factor across an r-tuple tail.

Equations

• One or more equations did not get rendered due to their size.
• MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveChainFamily params family 0 x_2 = MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveSourceFamily params family 0

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveChainFamily_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) (q : MoveQ params r) (ogs : MoveO params r) : (commuteGHalfSandwich_moveChainFamily params family r 0 q).outcome ogs = (commuteGHalfSandwich_moveSourceFamily params family r q).outcome ogs

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveChainFamily_last {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) (q : MoveQ params r) (ogs : MoveO params r) : (commuteGHalfSandwich_moveChainFamily params family r (Fin.last r) q).outcome ogs = (commuteGHalfSandwich_moveFamily params family r q).outcome ogs

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveChain_step {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) (hsc : SDDRel ψbi (uniformDistribution (SliceQuestion params)) (gHatSelfConsistencyLeftFamily params family) (gHatSelfConsistencyRightFamily params family) (gHatSelfConsistencyError zeta)) (r : ℕ) (i : Fin r) : SDDOpRel ψbi (uniformDistribution (MoveQ params r)) (commuteGHalfSandwich_moveChainFamily params family r i.castSucc) (commuteGHalfSandwich_moveChainFamily params family r i.succ) (gHatSelfConsistencyError zeta)