Section 12 pasting: half-sandwich lifting constructions

This module contains the reindexing equivalences and lifted operator families which transport an r-step half-sandwich move comparison to the corresponding r+1-step comparison.

References

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

Lifting families for the half-sandwich chain

Lifting constructions: swapped-front equivalences, splitSuccLiftFamily, prefixSecondSliceLeftFamily, secondSliceLiftFamily, and the moveChainLift construction that lifts an r-step chain to r+1.

def MIPStarRE.LDT.Pasting.swappedFrontQuestionEquiv (params : Parameters) (r : ℕ) : MoveTailQ params r ≃ SliceQuestion params × SliceQuestion params × SliceQuestion params × PointTuple params r

Swap the first two distinguished slice coordinates after exposing the tail coordinate of a move-chain question.

Equations

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

def MIPStarRE.LDT.Pasting.swappedFrontOutcomeEquiv (params : Parameters) [FieldModel params.q] (r : ℕ) : MoveTailO params r ≃ GHatOutcome params × GHatOutcome params × GHatOutcome params × GHatTupleOutcome params r

Outcome analogue of swappedFrontQuestionEquiv.

Equations

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

def MIPStarRE.LDT.Pasting.moveTailSwappedFrontQuestionEquiv (params : Parameters) (r : ℕ) : MoveQ params (r + 1) ≃ MoveTailQ params r

Expose the tail coordinate of an (r+1)-move question and put the first two distinguished slice coordinates in swapped-front order.

Equations

• MIPStarRE.LDT.Pasting.moveTailSwappedFrontQuestionEquiv params r = (MIPStarRE.LDT.Pasting.moveTailQuestionEquiv params r).trans (MIPStarRE.LDT.Pasting.swappedFrontQuestionEquiv params r)

def MIPStarRE.LDT.Pasting.moveTailSwappedFrontOutcomeEquiv (params : Parameters) [FieldModel params.q] (r : ℕ) : MoveO params (r + 1) ≃ MoveTailO params r

Outcome analogue of moveTailSwappedFrontQuestionEquiv.

Equations

• MIPStarRE.LDT.Pasting.moveTailSwappedFrontOutcomeEquiv params r = (MIPStarRE.LDT.Pasting.moveTailOutcomeEquiv params r).trans (MIPStarRE.LDT.Pasting.swappedFrontOutcomeEquiv params r)

noncomputable def MIPStarRE.LDT.Pasting.commuteGHalfSandwich_splitSuccLiftFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (r : ℕ) (F : IdxOpFamily (MoveQ params r) (MoveO params r) (ι × ι)) : IdxOpFamily (SliceQuestion params × PointTuple params (r + 1)) (GHatOutcome params × GHatTupleOutcome params (r + 1)) (ι × ι)

Reindex an r-move operator family along the split-successor equivalences.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.commuteGHalfSandwich_prefixSecondSliceLeftFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) (F : IdxOpFamily (SliceQuestion params × PointTuple params r) (GHatOutcome params × GHatTupleOutcome params r) (ι × ι)) : IdxOpFamily (MoveQ params r) (MoveO params r) (ι × ι)

Add a completed-slice factor on the left of an operator family, with the new slice coordinate placed in the second distinguished position.

Equations

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

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_prefixSecondSliceLeftLift {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (r : ℕ) (A B : IdxOpFamily (SliceQuestion params × PointTuple params r) (GHatOutcome params × GHatTupleOutcome params r) (ι × ι)) (δ : Error) (hAB : SDDOpRel ψbi (uniformDistribution (SliceQuestion params × PointTuple params r)) A B δ) : SDDOpRel ψbi (uniformDistribution (MoveQ params r)) (commuteGHalfSandwich_prefixSecondSliceLeftFamily params family r A) (commuteGHalfSandwich_prefixSecondSliceLeftFamily params family r B) δ

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_splitSuccLift {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (r : ℕ) (A B : IdxOpFamily (MoveQ params r) (MoveO params r) (ι × ι)) (δ : Error) (hAB : SDDOpRel ψbi (uniformDistribution (MoveQ params r)) A B δ) : SDDOpRel ψbi (uniformDistribution (SliceQuestion params × PointTuple params (r + 1))) (commuteGHalfSandwich_splitSuccLiftFamily params r A) (commuteGHalfSandwich_splitSuccLiftFamily params r B) δ

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

Lift an r-move operator family to the (r+1)-move questions by inserting the new second distinguished slice factor.

Equations

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

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_prefixSecondSliceLeft_splitSuccLift_eq_secondSliceLift {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) (F : IdxOpFamily (MoveQ params r) (MoveO params r) (ι × ι)) (q : MoveQ params (r + 1)) (ogs : MoveO params (r + 1)) : (commuteGHalfSandwich_prefixSecondSliceLeftFamily params family (r + 1) (commuteGHalfSandwich_splitSuccLiftFamily params r F) q).outcome ogs = (commuteGHalfSandwich_secondSliceLiftFamily params family r F q).outcome ogs

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveFamily_eq_moveStepTarget {ι : 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_moveFamily params family (r + 1) q).outcome ogs = (commuteGHalfSandwich_moveStepTargetFamily params family r ((moveTailQuestionEquiv params r) q)).outcome ((moveTailOutcomeEquiv params r) ogs)

def MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveChainLiftQuestionEquiv (params : Parameters) (r : ℕ) : MoveQ params r × SliceQuestion params ≃ MoveQ params (r + 1)

Reindex a question pair consisting of an r-move state and a new leading slice coordinate as an (r+1)-move state.

Equations

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

def MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveChainLiftOutcomeEquiv (params : Parameters) [FieldModel params.q] (r : ℕ) : MoveO params r × GHatOutcome params ≃ MoveO params (r + 1)

Outcome analogue of commuteGHalfSandwich_moveChainLiftQuestionEquiv.

Equations

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

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

Lift an r-move chain family by adjoining a new leading completed-slice factor on the left tensor register.

Equations

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

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveChainLift {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (r : ℕ) (A B : IdxOpFamily (MoveQ params r) (MoveO params r) (ι × ι)) (δ : Error) (hAB : SDDOpRel ψbi (uniformDistribution (MoveQ params r)) A B δ) : SDDOpRel ψbi (uniformDistribution (MoveQ params (r + 1))) (commuteGHalfSandwich_moveChainLiftFamily params family r A) (commuteGHalfSandwich_moveChainLiftFamily params family r B) δ

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveChainLift_moveFamily_eq_moveStepMid {ι : 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_moveChainLiftFamily params family r (commuteGHalfSandwich_moveFamily params family r) q).outcome ogs = (commuteGHalfSandwich_moveStepMidFamily params family r ((moveTailQuestionEquiv params r) q)).outcome ((moveTailOutcomeEquiv params r) ogs)

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveChainLift_moveFamily_last {ι : 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_moveChainLiftFamily params family r (commuteGHalfSandwich_moveFamily params family r)) (commuteGHalfSandwich_moveFamily params family (r + 1)) (gHatSelfConsistencyError zeta)