Section 12 pasting: half-sandwich move-chain base

The first recursive target family of the finite commutation chain in lem:commute-g-half-sandwich, and the equivalence between the split-successor comparison and the first move-chain 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 types MoveQ, MoveO, MoveTailQ and MoveTailO are classical and imported from the vendored file. The recursive target family takes the symmetric model S : SymModel 𝔓 K as its first explicit argument, as the placed families of Setup/Definitions do; callers write commuteGHalfSandwich_recursiveTargetFamily strategy.state params family r. The lemmas take S second, after params: commuteGHalfSandwich_recursiveTarget_eq_split params S family r q ogs, whose vendored version has no state, gains it there, as commuteGHalfSandwich_moveSource_eq_split does, and commuteGHalfSandwich_split_succ_iff params S family r δ takes it where the vendored ψbi was. No vendored lemma here has a swap, density or normalization hypothesis.

commuteGHalfSandwich_recursiveTarget_eq_split holds by S.leftTensor_mul_leftTensor up to definitional equality, where the vendored proof unfolds by simp; split_succ_iff rewrites with sddOpRel_uniform_equiv and applies the Co sddOpRel_reindex and sddOpRel_congr_outcome in each direction, as commuteGHalfSandwich_split_iff does.

Not ported

• MoveQ: classical, imported.
• MoveO: classical, imported.
• MoveTailQ: classical, imported.
• MoveTailO: 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

Recursive target family and the split-succ equivalence

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

The recursive target family obtained after one distinguished factor has been moved into the rotated half-product.

Equations

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

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_recursiveTarget_eq_split {𝔓 : 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_recursiveTargetFamily S params family r q).outcome ogs = (headTailRotatedFamily S 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)

The recursive target family is the rotated head-tail family of length r + 1, with the second distinguished coordinate consed onto the tail.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_split_succ_iff {𝔓 : 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 : ℕ) (δ : ℝ) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params × MIPStarRE.LDT.PointTuple params (r + 1))) (headTailOrderedFamily S params family (r + 1)) (headTailRotatedFamily S params family (r + 1)) δ ↔ S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.MoveQ params r)) (commuteGHalfSandwich_moveSourceFamily S params family r) (commuteGHalfSandwich_recursiveTargetFamily S params family r) δ

The head-tail commutation relation on (r + 1)-tuples is equivalent to the first move-chain comparison, between the move source and the recursive target.