Section 12 pasting: half-sandwich flat chain #
This module defines the post-move and combined flat chains used after the distinguished completed-slice factor has been moved to the right tensor register. The chain alternates between pairwise commutation and self-consistency steps, with an explicit error sequence for the final composition.
References #
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
Post-move flat chain and flat-chain definitions #
The post-move flat chain (postMoveFlatFamily, postMoveFlatError) and the
combined flat chain (flatChainFamily, flatChainError) together with their
endpoint and summation lemmas.
Length of the post-move part of the flat chain.
Equations
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatFamily
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
:
Fin (commuteGHalfSandwich_postMoveFlatLength r + 1) → IdxOpFamily (MoveQ params r) (MoveO params r) (ι × ι)
Operator-family sequence for the post-move part of the flat chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatError
(params : Parameters)
[FieldModel params.q]
(gamma zeta : Error)
(r : ℕ)
:
Error sequence for the post-move flat chain.
Equations
- One or more equations did not get rendered due to their size.
- MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatError params gamma zeta 0 x_2 = MIPStarRE.LDT.Pasting.gHatCommutationError params gamma zeta
Instances For
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatError_sum
(params : Parameters)
[FieldModel params.q]
(gamma zeta : Error)
(r : ℕ)
:
∑ i : Fin (commuteGHalfSandwich_postMoveFlatLength r), commuteGHalfSandwich_postMoveFlatError params gamma zeta r i = 2 * ↑r * zeta + ↑(r + 1) * gHatCommutationError params gamma zeta
Length of the combined move and post-move flat chain.
Equations
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainFamily
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
:
Fin (commuteGHalfSandwich_flatChainLength r + 1) → IdxOpFamily (MoveQ params r) (MoveO params r) (ι × ι)
Operator-family sequence obtained by concatenating the move chain and the post-move flat chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainError
(params : Parameters)
[FieldModel params.q]
(gamma zeta : Error)
(r : ℕ)
:
Error sequence for the combined flat chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_commuteFamily_zero_eq_recursiveTarget
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(q : SliceQuestion params × SliceQuestion params × PointTuple params 0)
(ogs : GHatOutcome params × GHatOutcome params × GHatTupleOutcome params 0)
:
(commuteGHalfSandwich_commuteFamily params family 0 q).outcome ogs = (commuteGHalfSandwich_recursiveTargetFamily params family 0 q).outcome ogs
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_secondSliceLift_recursiveTarget
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
(q : MoveQ params (r + 1))
(ogs : MoveO params (r + 1))
:
(commuteGHalfSandwich_secondSliceLiftFamily params family r (commuteGHalfSandwich_recursiveTargetFamily params family r)
q).outcome
ogs = (commuteGHalfSandwich_recursiveTargetFamily params family (r + 1) q).outcome ogs
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatFamily_zero_active
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
(q : MoveQ params r)
(ogs : MoveO params r)
:
(commuteGHalfSandwich_postMoveFlatFamily params family r 0 q).outcome ogs = (commuteGHalfSandwich_moveFamily params family r q).outcome ogs
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatFamily_one_active
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
(q : MoveQ params (r + 1))
(ogs : MoveO params (r + 1))
:
(commuteGHalfSandwich_postMoveFlatFamily params family (r + 1) ⟨1, ⋯⟩ q).outcome ogs = (commuteGHalfSandwich_commuteFamily params family (r + 1) q).outcome ogs
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_postMoveFlatFamily_last_active
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
(q : MoveQ params r)
(ogs : MoveO params r)
:
(commuteGHalfSandwich_postMoveFlatFamily params family r (Fin.last (commuteGHalfSandwich_postMoveFlatLength r))
q).outcome
ogs = (commuteGHalfSandwich_recursiveTargetFamily params family r q).outcome ogs
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainFamily_zero
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
(q : MoveQ params r)
(ogs : MoveO params r)
:
(commuteGHalfSandwich_flatChainFamily params family r 0 q).outcome ogs = (commuteGHalfSandwich_moveSourceFamily params family r q).outcome ogs
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainError_sum
(params : Parameters)
[FieldModel params.q]
(gamma zeta : Error)
(r : ℕ)
:
∑ i : Fin (commuteGHalfSandwich_flatChainLength r), commuteGHalfSandwich_flatChainError params gamma zeta r i = 4 * ↑r * zeta + ↑(r + 1) * gHatCommutationError params gamma zeta
theorem
MIPStarRE.LDT.Pasting.commuteGHalfSandwich_flatChainFamily_last
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(family : IdxPolyFamily params ι)
(r : ℕ)
(q : MoveQ params r)
(ogs : MoveO params r)
:
(commuteGHalfSandwich_flatChainFamily params family r (Fin.last (commuteGHalfSandwich_flatChainLength r)) q).outcome
ogs = (commuteGHalfSandwich_recursiveTargetFamily params family r q).outcome ogs