Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Pasting.ComparisonLemmas.CommuteGHalfSandwich.MoveChain.Base

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

This module introduces the question and outcome types used by the finite commutation chain in lem:commute-g-half-sandwich. It also defines the first recursive target family and proves the equivalence between the source split-successor comparison and the first move-chain comparison.

References #

Recursive target family and the split-succ equivalence #

These are the basic building blocks for the half-sandwich commutation chain: type abbreviations, the recursive target family, and the split-succ equivalence (split_succ_iff) plus the prefix-second-slice-left lemma.

source
@[reducible, inline]
abbrev MIPStarRE.LDT.Pasting.MoveQ (params : Parameters) (r : ℕ) :
Type

Questions for the move-chain state with two distinguished slice coordinates and an r-tuple tail.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev MIPStarRE.LDT.Pasting.MoveO (params : Parameters) [FieldModel params.q] (r : ℕ) :
    Type u_2

    Outcomes matching MoveQ: two distinguished completed-slice outcomes and an r-tuple tail.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev MIPStarRE.LDT.Pasting.MoveTailQ (params : Parameters) (r : ℕ) :
      Type

      Questions for the move-chain step after exposing the first tail coordinate.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[reducible, inline]
        abbrev MIPStarRE.LDT.Pasting.MoveTailO (params : Parameters) [FieldModel params.q] (r : ℕ) :
        Type u_2

        Outcomes for MoveTailQ, with three distinguished completed-slice outcomes and an r-tuple tail.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPStarRE.LDT.Pasting.commuteGHalfSandwich_recursiveTargetFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) :
          IdxOpFamily (MoveQ params r) (MoveO params r) (ι × ι)

          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.
          Instances For
            source
            theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_recursiveTarget_eq_split {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (r : ℕ) (q : MoveQ params r) (ogs : MoveO params r) :
            (commuteGHalfSandwich_recursiveTargetFamily params family r q).outcome ogs = (headTailRotatedFamily 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)
            source
            theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwich_split_succ_iff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (r : ℕ) (δ : Error) :
            SDDOpRel ψbi (uniformDistribution (SliceQuestion params × PointTuple params (r + 1))) (headTailOrderedFamily params family (r + 1)) (headTailRotatedFamily params family (r + 1)) δ ↔ SDDOpRel ψbi (uniformDistribution (MoveQ params r)) (commuteGHalfSandwich_moveSourceFamily params family r) (commuteGHalfSandwich_recursiveTargetFamily params family r) δ