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

The outcome lemmas of the line one-point transport: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/LdSandwichLineOnePoint/OutcomeLemmas.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The slice family is an IdxPolyFamily params 𝔓, so the one-point left families and their outcomes are local, in 𝔓, and the vendored conjugate transpose ᴴ is star. The lemmas expand the outcomes of the restricted sandwich families (G_{g} G_{g}^* summed over the tuples whose selected slot evaluates to a), show that no family has mass on none, and delete the trailing coordinates of the full left family, leaving the prefix family (ldSandwichLineOnePointLeftFamily_eq_prefixOriginal, the exact marginalization of ld-pasting.tex lines 932--953). No statement mentions the state, so no swap or normalization hypothesis appears, the vendored statements having none.

Not ported

• ldSandwichLineOnePoint_endpoint_comm_error_le: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

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

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointRightFamily_outcome_none_eq_zero {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.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 MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointRightFamily_total_eq_one {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.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 MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointPrefixMovedFamily_outcome_none_eq_zero {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) : (ldSandwichLineOnePointPrefixMovedFamily params family hi q).outcome none = 0

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

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

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

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointLeftFamily_outcome_some {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (a : MIPStarRE.LDT.Fq params) : (ldSandwichLineOnePointLeftFamily params strategy family k i q).outcome (some a) = ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k, if Option.map (fun (g : MIPStarRE.LDT.Polynomial params) => g.toFun q.1) (gs ⟨i, hi⟩) = some a then have half := gHatHalfProductOutcomeOperator params family k q.2 gs; half * star half else 0

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

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointPrefixOriginalFamily_outcome_some {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (a : MIPStarRE.LDT.Fq params) : (ldSandwichLineOnePointPrefixOriginalFamily params family hi q).outcome (some a) = ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1), if Option.map (fun (g : MIPStarRE.LDT.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 * star half else 0

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

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointPrefixMovedFamily_outcome_some {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (a : MIPStarRE.LDT.Fq params) : (ldSandwichLineOnePointPrefixMovedFamily params family hi q).outcome (some a) = ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1), if Option.map (fun (g : MIPStarRE.LDT.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 * star half else 0

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

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointLeftFamily_outcome_none_eq_zero {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.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 MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointPrefixOriginalFamily_outcome_none_eq_zero {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) : (ldSandwichLineOnePointPrefixOriginalFamily params family hi q).outcome none = 0

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

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointLeftFamily_drop_last_outcome_some {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) {n i : ℕ} (hi : i < n) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params (n + 1)) (a : MIPStarRE.LDT.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 MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointLeftFamily_eq_prefixOriginal {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (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.