Section 12 pasting: line one-point transport — outcome lemmas

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

References

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

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointRightFamily_outcome_none_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) : (ldSandwichLineOnePointRightFamily params strategy family k i q).outcome none = 0

The postprocessed one-point right family has zero-operator none outcome, because the selected slot satisfies i < k and is always postprocessed to some.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointRightFamily_total_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) : (ldSandwichLineOnePointRightFamily params strategy family k i q).total = 1

The one-point right family is measurement-valued when the selected coordinate exists. This is the source of nonnegativity for the linear consistency defect.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointPrefixMovedFamily_outcome_none_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) : (ldSandwichLineOnePointPrefixMovedFamily params family hi q).outcome none = 0

The rotated prefix-only one-point left family has no none outcome.

theorem MIPStarRE.LDT.Pasting.gHatSandwichFamily_restrict_eval_outcome_some {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {n : ℕ} (xs : PointTuple params n) (idx : Fin n) (u : Point params) (a : Fq params) : (postprocess (restrictSubMeas (gHatSandwichFamily params family n xs) fun (gs : GHatTupleOutcome params n) => Option.isSome (gs idx) = true) fun (gs : GHatTupleOutcome params n) => Option.map (fun (g : Polynomial params) => g.toFun u) (gs idx)).outcome (some a) = ∑ gs : GHatTupleOutcome params n, if Option.map (fun (g : Polynomial params) => g.toFun u) (gs idx) = some a then have half := gHatHalfProductOutcomeOperator params family n xs gs; half * Matrix.conjTranspose half else 0

Generic outcome expansion for evaluating a restricted completed-slice sandwich family at a concrete field value.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointLeftFamily_outcome_some {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) (a : Fq params) : (ldSandwichLineOnePointLeftFamily params strategy family k i q).outcome (some a) = ∑ gs : GHatTupleOutcome params k, if Option.map (fun (g : Polynomial params) => g.toFun q.1) (gs ⟨i, hi⟩) = some a then have half := gHatHalfProductOutcomeOperator params family k q.2 gs; half * Matrix.conjTranspose half else 0

Outcome expansion for the original full one-point left family at a concrete field value.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointPrefixOriginalFamily_outcome_some {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) (a : Fq params) : (ldSandwichLineOnePointPrefixOriginalFamily params family hi q).outcome (some a) = ∑ gs : GHatTupleOutcome params (i + 1), if Option.map (fun (g : Polynomial params) => g.toFun q.1) (gs ⟨i, ⋯⟩) = some a then have half := gHatHalfProductOutcomeOperator params family (i + 1) (fun (j : Fin (i + 1)) => q.2 ⟨↑j, ⋯⟩) gs; half * Matrix.conjTranspose half else 0

Outcome expansion for the original-order prefix family at a concrete field value.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointPrefixMovedFamily_outcome_some {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) (a : Fq params) : (ldSandwichLineOnePointPrefixMovedFamily params family hi q).outcome (some a) = ∑ gs : GHatTupleOutcome params (i + 1), if Option.map (fun (g : Polynomial params) => g.toFun q.1) (gs 0) = some a then have xsTail := fun (j : Fin i) => q.2 ⟨↑j, ⋯⟩; have xs := Fin.cons (q.2 ⟨i, hi⟩) xsTail; have half := gHatHalfProductOutcomeOperator params family (i + 1) xs gs; half * Matrix.conjTranspose half else 0

Outcome expansion for the selected-first prefix family at a concrete field value.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointLeftFamily_outcome_none_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) : (ldSandwichLineOnePointLeftFamily params strategy family k i q).outcome none = 0

The full one-point left family has no none outcome: the selected coordinate is restricted to genuine completed polynomials before postprocessing by evaluation.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointPrefixOriginalFamily_outcome_none_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) : (ldSandwichLineOnePointPrefixOriginalFamily params family hi q).outcome none = 0

The prefix-only one-point left family has no none outcome.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointLeftFamily_drop_last_outcome_some {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {n i : ℕ} (hi : i < n) (q : SandwichedLineQuestion params (n + 1)) (a : Fq params) : (ldSandwichLineOnePointLeftFamily params strategy family (n + 1) i q).outcome (some a) = (ldSandwichLineOnePointLeftFamily params strategy family n i (q.1, fun (j : Fin n) => q.2 ⟨↑j, ⋯⟩)).outcome (some a)

Delete one trailing sandwiched-line coordinate from the full one-point left family, for a genuine field outcome.

This is the one-coordinate version of paper ld-pasting.tex lines 934--941: summing over an extraneous completed-slice outcome collapses that measurement to I, leaving the shorter sandwich.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointLeftFamily_eq_prefixOriginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : ldSandwichLineOnePointLeftFamily params strategy family k i = ldSandwichLineOnePointPrefixOriginalFamily params family hi

Deleting all coordinates after i from the full one-point left family leaves exactly the prefix family used in the Cauchy--Schwarz transport.

This closes the paper's exact marginalization step ld-pasting.tex lines 932--953; the remaining analytic residual starts after this deletion.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_endpoint_comm_error_le (params : Parameters) [FieldModel params.q] (eps delta gamma zeta : Error) {j k : ℕ} (hj_pos : 1 ≤ j) (hjk : j ≤ k) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le : zeta ≤ 1) : zeta + √(8 * ↑params.m * min eps 1 + 4 * min delta 1) + 2 * √(commuteGHalfSandwichError params gamma zeta j) ≤ ldSandwichLineOnePointError params eps delta gamma zeta k

Scalar absorption for the post-tail-deletion one-point estimate.

This is the arithmetic at references/ldt-paper/ld-pasting.tex:1028--1033, with the endpoint error from eq:ld-gbcon and the two Cauchy--Schwarz losses from ld-pasting.tex:954--1024 kept separate. The proof uses the paper's √426 ≤ 21 estimate and the square comparison √(γ^(1/16)+ζ^(1/16)+(d/q)^(1/16)) ≤ γ^(1/32)+ζ^(1/32)+(d/q)^(1/32).