Documentation

MIPRE.Background.LIDT.Co.Pasting.ComparisonLemmas.CommuteGHalfSandwich.MoveChain.BackChain

Section 12 pasting: half-sandwich move-back chain #

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. 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 move-back family takes the symmetric model S : SymModel 𝔓 K as its first explicit argument, as the placed families of Setup/Definitions and MoveChain/Lifting do: commuteGHalfSandwich_moveBackChainFamily S params family r i. The lemmas take S second, after params: commuteGHalfSandwich_commute_to_moveBackChainFamily_zero params S family zeta hsc where the vendored ψbi was, and the three outcome identities, whose vendored versions have no state, gain it there. No vendored lemma here has a swap, density or normalization hypothesis. The swapped-front equivalences are classical and imported from the vendored MoveChain/Lifting.

The outcome identities hold by association and S.rightTensor_mul_rightTensor up to definitional equality through the swapped-front equivalences, Fin.cons and pointTupleTail, where the vendored proofs unfold by simp; at index 0 the move-back family is the second-slice lift of the last move-chain family by definitional equality (r - 0 = r), so commuteGHalfSandwich_moveChainFamily_last applies directly. The identity commuteGHalfSandwich_moveBackChainFamily_zero_eq_secondSliceLift_moveFamily is declared before commuteGHalfSandwich_commute_to_moveBackChainFamily_zero, the reverse of the vendored order, so that the latter cites it rather than repeating its proof, as the vendored proof does.

Not ported #

Every declaration of the vendored file has a counterpart here.

References #

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

Move-back chain #

source
noncomputable def MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveBackChainFamily {𝔓 : 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 : ℕ) :
Fin (r + 1) → IdxOpFamily (MIPStarRE.LDT.Pasting.MoveQ params (r + 1)) (MIPStarRE.LDT.Pasting.MoveO params (r + 1)) (K →L[ℂ] K)

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.
Instances For
    source
    theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_secondSliceLift_moveFamily_eq_swappedFrontMoveStepMid {𝔓 : 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_secondSliceLiftFamily S params family r (commuteGHalfSandwich_moveFamily S params family r) q).outcome ogs = (commuteGHalfSandwich_moveStepMidFamily S params family r ((MIPStarRE.LDT.Pasting.moveTailSwappedFrontQuestionEquiv params r) q)).outcome ((MIPStarRE.LDT.Pasting.moveTailSwappedFrontOutcomeEquiv params r) ogs)

    The second-slice lift of the r-move family is the move-step middle family, after exposing the first tail coordinate and swapping the two distinguished slices.

    source
    theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_commute_eq_swappedFrontMoveStepTarget {𝔓 : 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_commuteFamily S params family (r + 1) q).outcome ogs = (commuteGHalfSandwich_moveStepTargetFamily S params family r ((MIPStarRE.LDT.Pasting.moveTailSwappedFrontQuestionEquiv params r) q)).outcome ((MIPStarRE.LDT.Pasting.moveTailSwappedFrontOutcomeEquiv params r) ogs)

    The (r + 1)-move commuted endpoint is the move-step target family, after exposing the first tail coordinate and swapping the two distinguished slices.

    source
    theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveBackChainFamily_zero_eq_secondSliceLift_moveFamily {𝔓 : 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_moveBackChainFamily S params family r 0 q).outcome ogs = (commuteGHalfSandwich_secondSliceLiftFamily S params family r (commuteGHalfSandwich_moveFamily S params family r) q).outcome ogs

    The first family of the move-back chain is the second-slice lift of the r-move family.

    source
    theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_commute_to_moveBackChainFamily_zero {𝔓 : 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_commuteFamily S params family (r + 1)) (commuteGHalfSandwich_moveBackChainFamily S params family r 0) (MIPStarRE.LDT.Pasting.gHatSelfConsistencyError zeta)

    The commuted endpoint is close to the first family of the move-back chain, at the self-consistency error.