Section 12 pasting: commute G half-sandwich setup — definitions

Tuple equivalences, operator definitions, and family constructions for the half-sandwich commutation chain. This module contains all def/noncomputable def declarations and small helper lemmas used by the sum-bound and step-commutation submodules.

References

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

Sandwich-chain comparison lemmas

These lemmas capture the infrastructure needed for the lem:commute-g-half-sandwich through cor:h-a-consistency chain in ld-pasting.tex §9.3.

The n-step SDDOpRel composition lemma (sddOpRel_chain) lives in MIPStarRE.LDT.Preliminaries.CompletionTransfer alongside sddOpRel_triangle, since it is a general-purpose result used by multiple chapters.

def MIPStarRE.LDT.Pasting.pointTupleConsEquiv (params : Parameters) (k : ℕ) : PointTuple params (k + 1) ≃ SliceQuestion params × PointTuple params k

Split a nonempty tuple of slice questions into its first coordinate and the remaining tail.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.gHatReverseHalfProductOutcomeOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) : PointTuple params k → GHatTupleOutcome params k → Quantum.Op ι

Reverse-ordered half-product of completed-slice outcome operators.

Equations

• One or more equations did not get rendered due to their size.
• MIPStarRE.LDT.Pasting.gHatReverseHalfProductOutcomeOperator params family 0 _xs _gs = 1

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

Ordered head-tail family with the head completed-slice operator followed by the remaining half-product on the left tensor register.

Equations

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

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

Rotated head-tail family with the tail half-product placed before the head completed-slice operator.

Equations

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

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

Move-family endpoint with two distinguished left-register factors and the reverse half-product on the right register.

Equations

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

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

Commuted endpoint obtained by interchanging the two distinguished left-register completed-slice factors.

Equations

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

theorem MIPStarRE.LDT.Pasting.gHatHalfSandwichLeft_split_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) (xs : PointTuple params (k + 1)) (gs : GHatTupleOutcome params (k + 1)) : (gHatHalfSandwichLeft params family (k + 1) xs).outcome gs = (headTailOrderedFamily params family k ((pointTupleConsEquiv params k) xs)).outcome ((gHatTupleOutcomeConsEquiv' params k) gs)

theorem MIPStarRE.LDT.Pasting.gHatHalfSandwichLeft_split_total {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) (xs : PointTuple params (k + 1)) : (gHatHalfSandwichLeft params family (k + 1) xs).total = (headTailOrderedFamily params family k ((pointTupleConsEquiv params k) xs)).total

theorem MIPStarRE.LDT.Pasting.gHatHalfSandwichRight_split_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) (xs : PointTuple params (k + 1)) (gs : GHatTupleOutcome params (k + 1)) : (gHatHalfSandwichRight params family (k + 1) xs).outcome gs = (headTailRotatedFamily params family k ((pointTupleConsEquiv params k) xs)).outcome ((gHatTupleOutcomeConsEquiv' params k) gs)

theorem MIPStarRE.LDT.Pasting.gHatHalfSandwichRight_split_total {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) (xs : PointTuple params (k + 1)) : (gHatHalfSandwichRight params family (k + 1) xs).total = (headTailRotatedFamily params family k ((pointTupleConsEquiv params k) xs)).total

theorem MIPStarRE.LDT.Pasting.sddOpRel_uniform_equiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} {Outcome : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [Fintype Outcome] (e : α ≃ β) (ψ : QuantumState (ι × ι)) (A B : IdxOpFamily α Outcome (ι × ι)) (δ : Error) : SDDOpRel ψ (uniformDistribution α) A B δ ↔ SDDOpRel ψ (uniformDistribution β) (fun (b : β) => A (e.symm b)) (fun (b : β) => B (e.symm b)) δ

Base cases and consistency lifts

theorem MIPStarRE.LDT.Pasting.gHatSelfConsistency_sddOpRel {ι : 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)) : SDDOpRel ψbi (uniformDistribution (SliceQuestion params)) (gHatSelfConsistencyLeftFamily params family).toIdxOpFamily (gHatSelfConsistencyRightFamily params family).toIdxOpFamily (gHatSelfConsistencyError zeta)

theorem MIPStarRE.LDT.Pasting.sddOpRel_uniform_fst {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} {Outcome : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (A B : IdxOpFamily α Outcome (ι × ι)) (δ : Error) : SDDOpRel ψ (uniformDistribution α) A B δ → SDDOpRel ψ (uniformDistribution (α × β)) (fun (ab : α × β) => A ab.1) (fun (ab : α × β) => B ab.1) δ

theorem MIPStarRE.LDT.Pasting.gHatPairProduct_sddOpRel_triple {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) (r : ℕ) (hcom : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (gHatPairProductLeft params family) (gHatPairProductRight params family) (gHatCommutationError params gamma zeta)) : SDDOpRel ψbi (uniformDistribution (SliceQuestion params × SliceQuestion params × PointTuple params r)) (fun (q : SliceQuestion params × SliceQuestion params × PointTuple params r) => gHatPairProductLeft params family (q.1, q.2.1)) (fun (q : SliceQuestion params × SliceQuestion params × PointTuple params r) => gHatPairProductRight params family (q.1, q.2.1)) (gHatCommutationError params gamma zeta)

Slice-front equivalences

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

Move the third distinguished slice coordinate to the front while preserving the other two distinguished coordinates and the tail.

Equations

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

Question/outcome equivalences

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

Reassociate a head-tail slice question together with one additional slice question as a move-chain question.

Equations

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

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

Outcome analogue of splitQuestionEquiv, with the additional completed-slice outcome placed in the second distinguished position.

Equations

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

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

Reassociate a pair of distinguished completed-slice outcomes and an outcome tail as a move-chain outcome.

Equations

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

Split-successor and move-tail equivalences

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

Expose the first coordinate of a successor point tuple as the second distinguished slice question.

Equations

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

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

Outcome analogue of splitSuccQuestionEquiv.

Equations

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

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

Expose the first coordinate of the tail in a successor move question.

Equations

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

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

Outcome analogue of moveTailQuestionEquiv.

Equations

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

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

Move a new leading slice coordinate from the product suffix to the front of the exposed move-tail question.

Equations

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

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

Outcome analogue of firstSliceBackQuestionEquiv.

Equations

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

Move-step and source families

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

Source family for a single move step: three distinguished completed-slice operators and the tail half-product all lie on the left tensor register.

Equations

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

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

Target family for a single move step: the exposed tail coordinate and the reverse tail half-product have been moved to the right tensor register.

Equations

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

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

Intermediate family for a move step, after the third distinguished completed-slice operator but before that operator is moved to the right.

Equations

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

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

Source endpoint of the move chain before the first tail coordinate has been exposed.

Equations

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

Move-source splitting lemmas

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_moveSource_eq_split {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) (q : SliceQuestion params × SliceQuestion params × PointTuple params r) (ogs : GHatOutcome params × GHatOutcome params × GHatTupleOutcome params r) : (commuteGHalfSandwich_moveSourceFamily params family r q).outcome ogs = (headTailOrderedFamily params family (r + 1) (q.1, Fin.cons q.2.1 q.2.2)).outcome (ogs.1, Fin.cons ogs.2.1 ogs.2.2)

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_move_recursive_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) : SDDOpRel ψbi (uniformDistribution (SliceQuestion params × SliceQuestion params × PointTuple params 0)) (commuteGHalfSandwich_moveSourceFamily params family 0) (commuteGHalfSandwich_moveFamily params family 0) 0

One-element tuple equivalences

def MIPStarRE.LDT.Pasting.pointTupleOneEquiv (params : Parameters) : PointTuple params 1 ≃ SliceQuestion params

Identify a one-element point tuple with its unique slice question.

Equations

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

def MIPStarRE.LDT.Pasting.gHatTupleOutcomeOneEquiv (params : Parameters) [FieldModel params.q] : GHatTupleOutcome params 1 ≃ GHatOutcome params

Identify a one-element completed-slice outcome tuple with its unique outcome.

Equations

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

def MIPStarRE.LDT.Pasting.splitQuestionEquivOne (params : Parameters) : SliceQuestion params × PointTuple params 1 ≃ SlicePairQuestion params

Specialization of splitQuestionEquiv for a one-element tuple.

Equations

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

def MIPStarRE.LDT.Pasting.splitOutcomeEquivOne (params : Parameters) [FieldModel params.q] : GHatOutcome params × GHatTupleOutcome params 1 ≃ GHatOutcome params × GHatOutcome params

Outcome specialization matching splitQuestionEquivOne.

Equations

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

Outcome slice-front equivalences

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

Outcome analogue of thirdSliceFrontEquiv.

Equations

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