Section 12 pasting: half-sandwich lifting constructions

The lifted operator families that transport an r-step half-sandwich move comparison to the corresponding (r + 1)-step comparison: the counterpart of the vendored file of the same path under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The question and outcome equivalences are classical and imported from the vendored file. The placed families take the symmetric model S : SymModel 𝔓 K as their first explicit argument, as those of Setup/Definitions do: commuteGHalfSandwich_prefixSecondSliceLeftFamily S params family r F, commuteGHalfSandwich_secondSliceLiftFamily S params family r F and commuteGHalfSandwich_moveChainLiftFamily S params family r F. The reindexed family commuteGHalfSandwich_splitSuccLiftFamily params r F places nothing and is generic over the operator type. The lemmas take S second, after params, where the vendored ψbi was; the three outcome identities, whose vendored versions have no state (commuteGHalfSandwich_prefixSecondSliceLeft_splitSuccLift_eq_secondSliceLift, commuteGHalfSandwich_moveFamily_eq_moveStepTarget and commuteGHalfSandwich_moveChainLift_moveFamily_eq_moveStepMid), gain it there. No vendored lemma here has a swap, density or normalization hypothesis.

The two lifts by a left completed-slice factor are the vendored route: the sandwich Preliminaries.cabApproxDelta_raw by the placed slice, whose contraction bound is CommutativityPoints.liftLeft_sum_adjoint_mul_le_one, then sddOpRel_reindex along the vendored outcome equivalence and sddOpRel_congr_outcome, the outcomes agreeing by definitional equality where the vendored proofs unfold by simp. Of the outcome identities, the first holds by rfl, the second by S.rightTensor_mul_rightTensor and one association, the third by two associations, through Fin.cons and pointTupleTail up to definitional equality.

Not ported

• swappedFrontQuestionEquiv: classical, imported.
• swappedFrontOutcomeEquiv: classical, imported.
• moveTailSwappedFrontQuestionEquiv: classical, imported.
• moveTailSwappedFrontOutcomeEquiv: classical, imported.
• commuteGHalfSandwich_moveChainLiftQuestionEquiv: classical, imported.
• commuteGHalfSandwich_moveChainLiftOutcomeEquiv: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

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

Lifting families for the half-sandwich chain

def MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_splitSuccLiftFamily {R : Type u_3} (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (r : ℕ) (F : IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params r) (MIPStarRE.LDT.Pasting.MoveO params r) R) : IdxOpFamily (MIPStarRE.LDT.Pasting.SliceQuestion params × MIPStarRE.LDT.PointTuple params (r + 1)) (MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatTupleOutcome params (r + 1)) R

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 MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_prefixSecondSliceLeftFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (r : ℕ) (F : IdxOpFamily (MIPStarRE.LDT.Pasting.SliceQuestion params × MIPStarRE.LDT.PointTuple params r) (MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatTupleOutcome params r) (K →L[ℂ] K)) : IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params r) (MIPStarRE.LDT.Pasting.MoveO params r) (K →L[ℂ] K)

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 MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_prefixSecondSliceLeftLift {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (A B : IdxOpFamily (MIPStarRE.LDT.Pasting.SliceQuestion params × MIPStarRE.LDT.PointTuple params r) (MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatTupleOutcome params r) (K →L[ℂ] K)) (δ : ℝ) (hAB : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params × MIPStarRE.LDT.PointTuple params r)) A B δ) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.MoveQ params r)) (commuteGHalfSandwich_prefixSecondSliceLeftFamily S params family r A) (commuteGHalfSandwich_prefixSecondSliceLeftFamily S params family r B) δ

A comparison of head-tail families persists after left multiplication by the completed slice at a new second distinguished coordinate.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_splitSuccLift {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (r : ℕ) (A B : IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params r) (MIPStarRE.LDT.Pasting.MoveO params r) (K →L[ℂ] K)) (δ : ℝ) (hAB : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.MoveQ params r)) A B δ) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params × MIPStarRE.LDT.PointTuple params (r + 1))) (commuteGHalfSandwich_splitSuccLiftFamily params r A) (commuteGHalfSandwich_splitSuccLiftFamily params r B) δ

A comparison of r-move families persists after reindexing both along the split-successor equivalences.

noncomputable def MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_secondSliceLiftFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (r : ℕ) (F : IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params r) (MIPStarRE.LDT.Pasting.MoveO params r) (K →L[ℂ] K)) : IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params (r + 1)) (MIPStarRE.LDT.Pasting.MoveO params (r + 1)) (K →L[ℂ] K)

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 MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_prefixSecondSliceLeft_splitSuccLift_eq_secondSliceLift {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (F : IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params r) (MIPStarRE.LDT.Pasting.MoveO params r) (K →L[ℂ] K)) (q : MIPStarRE.LDT.Pasting.MoveQ params (r + 1)) (ogs : MIPStarRE.LDT.Pasting.MoveO params (r + 1)) : (commuteGHalfSandwich_prefixSecondSliceLeftFamily S params family (r + 1) (commuteGHalfSandwich_splitSuccLiftFamily params r F) q).outcome ogs = (commuteGHalfSandwich_secondSliceLiftFamily S params family r F q).outcome ogs

Prefixing the second slice to the split-successor reindexing is the second-slice lift.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveFamily_eq_moveStepTarget {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params (r + 1)) (ogs : MIPStarRE.LDT.Pasting.MoveO params (r + 1)) : (commuteGHalfSandwich_moveFamily S params family (r + 1) q).outcome ogs = (commuteGHalfSandwich_moveStepTargetFamily S params family r ((MIPStarRE.LDT.Pasting.moveTailQuestionEquiv params r) q)).outcome ((MIPStarRE.LDT.Pasting.moveTailOutcomeEquiv params r) ogs)

The (r + 1)-move family is the move-step target family, after exposing the first tail coordinate.

noncomputable def MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveChainLiftFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (r : ℕ) (F : IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params r) (MIPStarRE.LDT.Pasting.MoveO params r) (K →L[ℂ] K)) : IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params (r + 1)) (MIPStarRE.LDT.Pasting.MoveO params (r + 1)) (K →L[ℂ] K)

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 MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveChainLift {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (A B : IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params r) (MIPStarRE.LDT.Pasting.MoveO params r) (K →L[ℂ] K)) (δ : ℝ) (hAB : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.MoveQ params r)) A B δ) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.MoveQ params (r + 1))) (commuteGHalfSandwich_moveChainLiftFamily S params family r A) (commuteGHalfSandwich_moveChainLiftFamily S params family r B) δ

A comparison of r-move families persists after the move-chain lift by a new leading completed-slice factor.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveChainLift_moveFamily_eq_moveStepMid {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params (r + 1)) (ogs : MIPStarRE.LDT.Pasting.MoveO params (r + 1)) : (commuteGHalfSandwich_moveChainLiftFamily S params family r (commuteGHalfSandwich_moveFamily S params family r) q).outcome ogs = (commuteGHalfSandwich_moveStepMidFamily S params family r ((MIPStarRE.LDT.Pasting.moveTailQuestionEquiv params r) q)).outcome ((MIPStarRE.LDT.Pasting.moveTailOutcomeEquiv params r) ogs)

The move-chain lift of the r-move family is the move-step middle family, after exposing the first tail coordinate.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveChainLift_moveFamily_last {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) (r : ℕ) (hsc : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (gHatSelfConsistencyLeftFamily S params family) (gHatSelfConsistencyRightFamily S params family) (MIPStarRE.LDT.Pasting.gHatSelfConsistencyError zeta)) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.MoveQ params (r + 1))) (commuteGHalfSandwich_moveChainLiftFamily S params family r (commuteGHalfSandwich_moveFamily S params family r)) (commuteGHalfSandwich_moveFamily S params family (r + 1)) (MIPStarRE.LDT.Pasting.gHatSelfConsistencyError zeta)

The last edge of the move chain: the move-chain lift of the r-move family is close to the (r + 1)-move family, at the self-consistency error.