Section 12 pasting: half-sandwich move chain

The recursive sequence of operator families which moves a completed-slice factor through the half-product, and its adjacent edges, each supplied by the self-consistency estimate for the completed-slice family: 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 chain 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_moveChainFamily S params family r i. The lemmas take S second, after params: commuteGHalfSandwich_moveChainFamily_zero params S family, commuteGHalfSandwich_moveChainFamily_last params S family, whose vendored versions have no state, gain it there, and commuteGHalfSandwich_moveChain_step params S family zeta hsc takes it where the vendored ψbi was. No vendored lemma here has a swap, density or normalization hypothesis.

The recursion unfolds by dite_eq_left and dite_eq_right, and the outcome identities hold by S.leftTensor_mul_leftTensor and association up to definitional equality, where the vendored proofs unfold by simp.

Not ported

Every declaration of the vendored file has a counterpart here.

References

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

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

Move chain: recursive family, step lemma

noncomputable def MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveChainFamily {𝔓 : 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) (MIPStarRE.LDT.Pasting.MoveO params r) (K →L[ℂ] K)

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.
• MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveChainFamily S params family 0 x_2 = MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveSourceFamily S params family 0

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveChainFamily_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 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params r) (ogs : MIPStarRE.LDT.Pasting.MoveO params r) : (commuteGHalfSandwich_moveChainFamily S params family r 0 q).outcome ogs = (commuteGHalfSandwich_moveSourceFamily S params family r q).outcome ogs

The first family of the move chain is the move source.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveChainFamily_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 𝔓) (r : ℕ) (q : MIPStarRE.LDT.Pasting.MoveQ params r) (ogs : MIPStarRE.LDT.Pasting.MoveO params r) : (commuteGHalfSandwich_moveChainFamily S params family r (Fin.last r) q).outcome ogs = (commuteGHalfSandwich_moveFamily S params family r q).outcome ogs

The last family of the move chain is the move family.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_moveChain_step {𝔓 : 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 : ℝ) (hsc : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (gHatSelfConsistencyLeftFamily S params family) (gHatSelfConsistencyRightFamily S params family) (MIPStarRE.LDT.Pasting.gHatSelfConsistencyError zeta)) (r : ℕ) (i : Fin r) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.MoveQ params r)) (commuteGHalfSandwich_moveChainFamily S params family r i.castSucc) (commuteGHalfSandwich_moveChainFamily S params family r i.succ) (MIPStarRE.LDT.Pasting.gHatSelfConsistencyError zeta)

Adjacent families of the move chain are at the self-consistency error.