Section 12 pasting: half-sandwich flat-chain steps

The adjacent-edge estimates for the post-move and combined flat chains, the local inputs to the final chain composition in the proof of commuteGHalfSandwich_core: 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").

Both lemmas take the symmetric model S : SymModel 𝔓 K second, after params, where the vendored ψbi was: commuteGHalfSandwich_postMoveFlatStep params S family gamma zeta hsc hcom r i and commuteGHalfSandwich_flatChainStep params S family gamma zeta hsc hcom r i. Neither has a swap, density or normalization hypothesis in the vendored file.

Where the vendored proofs compare outcomes by simp and transport each edge along sddOpRel_congr_outcome, these rewrite the two families of the edge and its error to the families of a step lemma, as equalities of families: the recursions unfold by ite_eq_left, ite_eq_right, dite_eq_left and dite_eq_right, and an index whose value is not definitionally that of the step lemma's index is moved by Fin.ext. Outcome identities remain at the two edges whose families agree only outcome by outcome: the base edge of the post-move chain (commuteGHalfSandwich_commuteFamily_zero_eq_recursiveTarget) and its edge into the move-back chain (commuteGHalfSandwich_postMoveFlatFamily_zero_active, commuteGHalfSandwich_moveBackChainFamily_zero_eq_secondSliceLift_moveFamily). The base edge of the combined chain is the commutation step at r = 0, as the vendored commuteGHalfSandwich_postMoveFlatStep at 0 is, with the move family and the move source identified outcome by outcome.

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

Flat-chain step lemmas

postMoveFlatStep builds the edges within the post-move phase, and flatChainStep stitches the move-chain prefix and the post-move suffix into one combined chain.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_postMoveFlatStep {𝔓 : 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 𝔓) (gamma 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)) (hcom : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (gHatPairProductLeft S params family) (gHatPairProductRight S params family) (MIPStarRE.LDT.Pasting.gHatCommutationError params gamma zeta)) (r : ℕ) (i : Fin (MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatLength r)) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.MoveQ params r)) (commuteGHalfSandwich_postMoveFlatFamily S params family r i.castSucc) (commuteGHalfSandwich_postMoveFlatFamily S params family r i.succ) (MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatError params gamma zeta r i)

Adjacent families of the post-move flat chain are at the error of the post-move error sequence.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_flatChainStep {𝔓 : 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 𝔓) (gamma 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)) (hcom : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (gHatPairProductLeft S params family) (gHatPairProductRight S params family) (MIPStarRE.LDT.Pasting.gHatCommutationError params gamma zeta)) (r : ℕ) (i : Fin (MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainLength r)) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.MoveQ params r)) (commuteGHalfSandwich_flatChainFamily S params family r i.castSucc) (commuteGHalfSandwich_flatChainFamily S params family r i.succ) (MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainError params gamma zeta r i)

Adjacent families of the combined flat chain are at the error of the combined error sequence.