Section 12 pasting: line one-point transport — prefix moved lemmas

Internal helper module; part of the file-split for #1127.

References

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

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePointPrefixOriginalFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : IdxSubMeas (SandwichedLineQuestion params k) (Option (Fq params)) ι

The original one-point left family restricted to the prefix through coordinate i.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePointPrefixMovedFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : IdxSubMeas (SandwichedLineQuestion params k) (Option (Fq params)) ι

The prefix family after rotating the selected coordinate to the front.

Equations

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

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointPrefixMoved_eq_endpoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : ldSandwichLineOnePointPrefixMovedFamily params family hi = fun (q : SandwichedLineQuestion params k) => postprocess (evaluateAt params q.1 (family.meas (q.2 ⟨i, hi⟩)).toSubMeas) some

Rotating the selected coordinate to the front reduces the prefix family to ldGbcon.

This is the prefix-completeness collapse and endpoint identification used after references/ldt-paper/ld-pasting.tex:1011--1024: once the selected coordinate is first, summing the remaining prefix sandwich leaves the one-point endpoint measurement.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointLeftFamily_self_eq_prefixOriginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (i : ℕ) : ldSandwichLineOnePointLeftFamily params strategy family (i + 1) i = ldSandwichLineOnePointPrefixOriginalFamily params family ⋯

The global one-point left family at its last prefix index is the prefix family.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointPrefixMoved_consRel_endpoint_of_axis_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta zeta : Error) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (family : IdxPolyFamily params ι) (hcons : family.ConsistentWithPoints strategy zeta) {k i : ℕ} (hi : i < k) : ConsRel strategy.state (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixMovedFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) (zeta + √(8 * ↑params.m * eps + 4 * delta))

Endpoint consistency for the rotated prefix family.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointPrefixMoved_rawCommutation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hcomm : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params ψ family gamma zeta j) {i : ℕ} (hi0 : i ≠ 0) : SDDOpRel ψ (uniformDistribution (PointTuple params (i + 1))) (gHatHalfSandwichLeft params family (i + 1)) (gHatHalfSandwichRight params family (i + 1)) (commuteGHalfSandwichError params gamma zeta (i + 1))

Raw commutation for the nonempty prefix before adding the remaining question tail.

theorem MIPStarRE.LDT.Pasting.gHatHalfProduct_prefix_mul_last {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (i : ℕ) (xs : PointTuple params (i + 2)) (gs : GHatTupleOutcome params (i + 2)) : gHatHalfProductOutcomeOperator params family (i + 2) xs gs = (gHatHalfProductOutcomeOperator params family (i + 1) (fun (j : Fin (i + 1)) => xs ⟨↑j, ⋯⟩) fun (j : Fin (i + 1)) => gs ⟨↑j, ⋯⟩) * (gHatIdxMeas params family (xs ⟨i + 1, ⋯⟩)).outcome (gs ⟨i + 1, ⋯⟩)

Expand a half-product into the prefix product times the last slice operator.

theorem MIPStarRE.LDT.Pasting.gHatHalfProductOutcomeOperator_prefix_last {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (n : ℕ) (xs : PointTuple params (n + 1)) (gs : GHatTupleOutcome params (n + 1)) : gHatHalfProductOutcomeOperator params family (n + 1) xs gs = (gHatHalfProductOutcomeOperator params family n (fun (j : Fin n) => xs ⟨↑j, ⋯⟩) fun (j : Fin n) => gs ⟨↑j, ⋯⟩) * (gHatIdxMeas params family (xs ⟨n, ⋯⟩)).outcome (gs ⟨n, ⋯⟩)

Split the ordered half-product into its first n coordinates and the last slice.

theorem MIPStarRE.LDT.Pasting.gHatSandwich_sum_last_eq_prefix {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (n : ℕ) (xs : PointTuple params (n + 1)) (gsPrefix : GHatTupleOutcome params n) : (∑ g : GHatOutcome params, have half := gHatHalfProductOutcomeOperator params family (n + 1) xs ((gHatTupleOutcomePrefixLastEquiv params n).symm (gsPrefix, g)); half * Matrix.conjTranspose half) = gHatHalfProductOutcomeOperator params family n (fun (j : Fin n) => xs ⟨↑j, ⋯⟩) gsPrefix * Matrix.conjTranspose (gHatHalfProductOutcomeOperator params family n (fun (j : Fin n) => xs ⟨↑j, ⋯⟩) gsPrefix)

Summing the last completed-slice sandwich coordinate deletes that coordinate.

This formalizes the measurement-completeness step in ld-pasting.tex lines 934--941 for a single trailing coordinate.

theorem MIPStarRE.LDT.Pasting.gHatHalfProduct_lastReverse_eq_conjTranspose {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (i : ℕ) (xs : PointTuple params (i + 1)) (gs : GHatTupleOutcome params (i + 1)) : gHatHalfProductOutcomeOperator params family (i + 1) ((pointTupleLastReverseEquiv params i) xs) ((gHatTupleOutcomeLastReverseEquiv params i) gs) = Matrix.conjTranspose (gHatHalfProductOutcomeOperator params family (i + 1) xs gs)

Reversing the prefix after moving the last coordinate to the front gives the adjoint product.

theorem MIPStarRE.LDT.Pasting.gHatRotatedHalfProduct_lastReverse_eq_conjTranspose_lastFront {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (i : ℕ) (xs : PointTuple params (i + 1)) (gs : GHatTupleOutcome params (i + 1)) : gHatRotatedHalfProductOutcomeOperator params family (i + 1) ((pointTupleLastReverseEquiv params i) xs) ((gHatTupleOutcomeLastReverseEquiv params i) gs) = Matrix.conjTranspose (gHatHalfProductOutcomeOperator params family (i + 1) ((pointTupleLastFrontEquiv params i) xs) ((gHatTupleOutcomeLastFrontEquiv params i) gs))

The rotated product on the last-reversed tuple is the adjoint of the last-front product.