Section 12 pasting: line one-point transport — Cauchy–Schwarz setup

The setup of the two Cauchy–Schwarz moves of the line one-point transport: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/LdSandwichLineOnePoint/CSSetup.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The linear (pre-max) consistency defect qBipartiteLinearConsDefect and its expansion against the complementary right outcome; the source, intermediate and moved outcome sums of ld-pasting.tex lines 960--1010; the ordered and rotated half-products, which are local, in 𝔓, and their left placements ldSandwichLineOnePointCS_Aord/_Arot, joint, in K →L[ℂ] K; the raw commutation of the half-sandwich reindexed to original outcomes, as an SDDOpRel on a symmetric model; and the fact records the Cauchy–Schwarz step consumes. The vendored conjugate transpose ᴴ is star.

The vendored qBipartiteLinearConsDefect and its three lemmas (qBipartiteLinearConsDefect_option_eq_sum_some_complement, qBipartiteLinearConsDefect_nonneg_of_right_total_one and bipartiteConsError_le_of_linearDefect_average_bound) allow two tensor factors ιA, ιB; here, as for every bipartite quantity of the port ("Same-space and bipartite quantities"), both factors are 𝔓 in a symmetric model S, taken as an explicit first argument. Every vendored use applies them to strategy.state with both families on one carrier (LdSandwichLineOnePoint/{Core,CauchySchwarz}.lean), so the narrowed forms serve them. The definitions that place without a strategy (ldSandwichLineOnePointCS_Aord, _Arot, their adjoint families and the two adjoint raw families) and the two lemmas about them take (S : SymModel 𝔓 K) as an explicit first argument, in place of the vendored named carrier (ι₂ := ι). No vendored statement here carries a swap or normalization hypothesis.

Not ported

Nothing: every vendored declaration has a counterpart of the same name.

References

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

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

noncomputable def MIPRE.LIDT.Co.Pasting.qBipartiteLinearConsDefect {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A B : SubMeas Outcome 𝔓) : ℝ

The linear (pre-max) form of the bipartite consistency defect, ev(A_total ⊗ B_total) − Σ_o ev(A_o ⊗ B_o).

Equations

• MIPRE.LIDT.Co.Pasting.qBipartiteLinearConsDefect S A B = S.ev (S.opTensor A.total B.total) - S.qBipartiteMatchMass A B

theorem MIPRE.LIDT.Co.Pasting.qBipartiteLinearConsDefect_option_eq_sum_some_complement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (S : SymModel 𝔓 K) (A B : SubMeas (Option α) 𝔓) (hBtotal : B.total = 1) (hAnone : A.outcome none = 0) (hBnone : B.outcome none = 0) : qBipartiteLinearConsDefect S A B = ∑ a : α, S.ev (S.opTensor (A.outcome (some a)) (1 - B.outcome (some a)))

For option-valued families with no none mass, the linear bipartite consistency defect is the paper's sum against the complementary right outcome: ev(A_total ⊗ B_total) − Σ_o ev(A_o ⊗ B_o) = Σ_a ev(A_a ⊗ (1 − B_a)) when Bob's family is a measurement and both none outcomes vanish.

theorem MIPRE.LIDT.Co.Pasting.qBipartiteLinearConsDefect_nonneg_of_right_total_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A B : SubMeas Outcome 𝔓) (hBtotal : B.total = 1) : 0 ≤ qBipartiteLinearConsDefect S A B

The linear consistency defect is nonnegative when the right-hand family is a measurement. This lets the paper's averaged linear estimate feed the max 0 qBipartiteConsDefect form without a pointwise absolute-value gap.

theorem MIPRE.LIDT.Co.Pasting.bipartiteConsError_le_of_linearDefect_average_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B C : IdxSubMeas Question Outcome 𝔓) (η : ℝ) (hCtotal : ∀ (q : Question), (C q).total = 1) (hgap : (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => qBipartiteLinearConsDefect S (A q) (C q)) ≤ (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => qBipartiteLinearConsDefect S (B q) (C q)) + η) : S.bipartiteConsError 𝒟 A C ≤ S.bipartiteConsError 𝒟 B C + η

If the averaged linear consistency-defect comparison holds and the right family is measurement-valued, then the averaged max 0 bipartite consistency error comparison follows.

This is the paper-faithful formulation of lem:ld-sandwich-line-one-point: the Cauchy–Schwarz argument controls an averaged linear expression, not an average of pointwise absolute values. Nonnegativity of the linear defects removes the outer max 0.

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_sourceOutcomeSum {𝔓 : 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) : ℝ

The original expanded off-diagonal scalar in ld-pasting.tex:960--963.

This is the source side after deleting extraneous tail coordinates and expanding the linear consistency defect as Σ_a ev(A_a ⊗ (I − B_a)).

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum {𝔓 : 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) : ℝ

The intermediate scalar after the first Cauchy–Schwarz move ld-pasting.tex:964--986 (eq:gonna-need-a-bigger-cauchy-schwarz).

For an original-order prefix outcome gs, orderedHalf is G^{x_<i}_{g_<i} G^{x_i}_{g_i} while rotatedHalf is G^{x_i}_{g_i} G^{x_<i}_{g_<i}. The first CS move replaces only the left half of the sandwich, leaving star orderedHalf on the right.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_movedOutcomeSum {𝔓 : 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) : ℝ

The target expanded off-diagonal scalar after the two CS moves.

This is the moved-prefix side. The separate endpoint/prefix-completeness collapse to ldGbcon is the already-proved ldSandwichLineOnePointPrefixMoved_eq_endpoint, corresponding to ld-pasting.tex:1011--1024.

Equations

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

structure MIPRE.LIDT.Co.Pasting.LdSandwichLineOnePointOutcomeSumCSRoute {𝔓 : 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 𝔓) (gamma zeta : ℝ) {k i : ℕ} (hi : i < k) : Prop

Paper-faithful split of the remaining off-diagonal CS route.

The fields isolate the two uses of Preliminaries.closenessOfIP / Preliminaries.closenessOfIPAdjoint in ld-pasting.tex:964--1010. The endpoint collapse after these fields is already packaged by ldSandwichLineOnePointPrefixMoved_eq_endpoint (ld-pasting.tex:1011--1024).

• firstCauchySchwarz : ldSandwichLineOnePoint_prefix_sourceOutcomeSum params strategy family hi ≤ ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum params strategy family hi + √(MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1))

  First CS move, paper lines 964--986 and label eq:gonna-need-a-bigger-cauchy-schwarz: move the selected G to the left of the prefix in the left half of the sandwich.

• secondCauchySchwarz : ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum params strategy family hi ≤ ldSandwichLineOnePoint_prefix_movedOutcomeSum params strategy family hi + √(MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1))

  Second CS move, paper lines 987--1010 and label eq:even-bigger-CS: move the selected G through the adjoint/right half, reaching the moved-prefix scalar.

structure MIPRE.LIDT.Co.Pasting.LdSandwichLineOnePointOutcomeSumCSAbsBounds {𝔓 : 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 𝔓) (gamma zeta : ℝ) {k i : ℕ} (hi : i < k) : Prop

Absolute-value form of the two off-diagonal Cauchy–Schwarz moves.

This is the direct output shape of Preliminaries.closenessOfIPAdjoint and Preliminaries.closenessOfIP: each field compares the two adjacent scalar averages from ld-pasting.tex:964--1010 with error √ν₄. The one-sided route used downstream is only an arithmetic consequence of these absolute-value bounds.

• firstAbs : |ldSandwichLineOnePoint_prefix_sourceOutcomeSum params strategy family hi - ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum params strategy family hi| ≤ √(MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1))

  First CS move in the exact absolute-value form of prop:closeness-of-ip, paper lines 964--986 and label eq:gonna-need-a-bigger-cauchy-schwarz.

• secondAbs : |ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum params strategy family hi - ldSandwichLineOnePoint_prefix_movedOutcomeSum params strategy family hi| ≤ √(MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1))

  Second CS move in the exact absolute-value form of prop:closeness-of-ip, paper lines 987--1010 and label eq:even-bigger-CS.

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_orderedHalf {𝔓 : 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) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) : 𝔓

Ordered half-product appearing in the line-one-point CS step.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_rotatedHalf {𝔓 : 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) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) : 𝔓

Rotated half-product appearing after moving the selected slice to the front.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_rightComplement {𝔓 : 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 : ℕ} (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) : 𝔓

Right-hand complement selected by the completed polynomial outcome.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_Aord {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k → MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1) → K →L[ℂ] K

Raw ordered left-placed family used in the generic CS proposition.

Equations

• MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_Aord S params family hi q gs = S.L (MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_orderedHalf params family hi q gs)

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_Arot {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k → MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1) → K →L[ℂ] K

Raw rotated left-placed family used in the generic CS proposition.

Equations

• MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_Arot S params family hi q gs = S.L (MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_rotatedHalf params family hi q gs)

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_AordAdjointFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) : IdxOpFamily (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) (K →L[ℂ] K)

The adjoint of the ordered raw CS family, as an indexed operator family.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_ArotAdjointFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) : IdxOpFamily (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) (K →L[ℂ] K)

The adjoint of the rotated raw CS family, as an indexed operator family.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointAdjointRawLeftFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (_hi : i < k) : IdxOpFamily (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) (K →L[ℂ] K)

Raw left family for the adjoint-oriented CS input, indexed by original outcomes.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointAdjointRawRightFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (_hi : i < k) : IdxOpFamily (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) (K →L[ℂ] K)

Raw right family for the adjoint-oriented CS input, indexed by original outcomes.

Equations

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

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_adjointRawCommutation_originalOutcome {𝔓 : 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] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (hcomm : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params S family gamma zeta j) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointAdjointRawLeftFamily S params family hi) (ldSandwichLineOnePointAdjointRawRightFamily S params family hi) (MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1))

Raw commutation after last-reverse reindexing, lifted to sandwiched-line questions.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointAdjointRawLeftFamily_eq_CS_Aord_adjoint {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) : (ldSandwichLineOnePointAdjointRawLeftFamily S params family hi q).outcome gs = star (ldSandwichLineOnePointCS_Aord S params family hi q gs)

The adjoint raw family agrees with the ordered CS family.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointAdjointRawRightFamily_eq_CS_Arot_adjoint {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) : (ldSandwichLineOnePointAdjointRawRightFamily S params family hi q).outcome gs = star (ldSandwichLineOnePointCS_Arot S params family hi q gs)

The adjoint raw family agrees with the rotated CS family.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_adjointRawCommutation_qSDDCore_bound {𝔓 : 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 𝔓) (gamma zeta : ℝ) (hcomm : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params strategy.state family gamma zeta j) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) fun (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) => strategy.state.qSDDCore (fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) => star (ldSandwichLineOnePointCS_Aord strategy.state params family hi q gs)) fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) => star (ldSandwichLineOnePointCS_Arot strategy.state params family hi q gs)) ≤ MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1)

The adjoint-oriented raw-core bound needed by the line-one-point CS step.

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_Cfirst {𝔓 : 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) : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k → MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1) → Unit → K →L[ℂ] K

The C family for the first, right-action CS move.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_Csecond {𝔓 : 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) : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k → MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1) → Unit → K →L[ℂ] K

The C family for the second, left-action CS move.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_firstSourceRaw {𝔓 : 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) : ℝ

Raw scalar on the source side of the first CS application.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_firstTargetRaw {𝔓 : 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) : ℝ

Raw scalar on the target side of the first CS application.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_secondSourceRaw {𝔓 : 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) : ℝ

Raw scalar on the source side of the second CS application.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointCS_secondTargetRaw {𝔓 : 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) : ℝ

Raw scalar on the target side of the second CS application.

Equations

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

structure MIPRE.LIDT.Co.Pasting.LdSandwichLineOnePointCSFacts {𝔓 : 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 𝔓) (gamma zeta : ℝ) {k i : ℕ} (hi : i < k) : Prop

Exact low-level facts needed to turn the generic closenessOfIP* lemmas into ld-pasting.tex:964--1010 for the line-one-point statement.

This record separates the generic CS theorem instantiation from the paper-specific facts:

• the adjoint-oriented raw square-distance bound corresponding to the first square root in lines 974--985 and reused in lines 1005--1010;
• the two unit-side measurement-completeness bounds from lines 986 and 1008;
• the algebraic regrouping/reindexing that identifies the raw CS scalars with the existing source, intermediate, and moved outcome sums.

• adjointRawCore : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) fun (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) => strategy.state.qSDDCore (fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) => star (ldSandwichLineOnePointCS_Aord strategy.state params family hi q gs)) fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) => star (ldSandwichLineOnePointCS_Arot strategy.state params family hi q gs)) ≤ MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1)

  The adjoint-oriented raw square-distance bound.

• firstUnitBound (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) : ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1), star (∑ u : Unit, ldSandwichLineOnePointCS_Cfirst params strategy family hi q gs u) * ∑ u : Unit, ldSandwichLineOnePointCS_Cfirst params strategy family hi q gs u ≤ 1

  The unit-side completeness bound of the first CS move.

• secondUnitBound (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) : ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1), (∑ u : Unit, ldSandwichLineOnePointCS_Csecond params strategy family hi q gs u) * star (∑ u : Unit, ldSandwichLineOnePointCS_Csecond params strategy family hi q gs u) ≤ 1

  The unit-side completeness bound of the second CS move.

• source_eq_firstSourceRaw : ldSandwichLineOnePoint_prefix_sourceOutcomeSum params strategy family hi = ldSandwichLineOnePointCS_firstSourceRaw params strategy family hi

  The source outcome sum is the raw source scalar of the first CS move.

• afterFirst_eq_firstTargetRaw : ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum params strategy family hi = ldSandwichLineOnePointCS_firstTargetRaw params strategy family hi

  The intermediate outcome sum is the raw target scalar of the first CS move.

• afterFirst_eq_secondSourceRaw : ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum params strategy family hi = ldSandwichLineOnePointCS_secondSourceRaw params strategy family hi

  The intermediate outcome sum is the raw source scalar of the second CS move.

• moved_eq_secondTargetRaw : ldSandwichLineOnePoint_prefix_movedOutcomeSum params strategy family hi = ldSandwichLineOnePointCS_secondTargetRaw params strategy family hi

  The moved outcome sum is the raw target scalar of the second CS move.

structure MIPRE.LIDT.Co.Pasting.LdSandwichLineOnePointAdjointRawCoreBound {𝔓 : 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 𝔓) (gamma zeta : ℝ) {k i : ℕ} (hi : i < k) : Prop

The adjoint-oriented raw commutator square-distance bound used by the two Cauchy–Schwarz applications in the proof of lem:ld-sandwich-line-one-point.

The surrounding endpoint expansions and option-valued match-mass identities are proved directly where they are used; this structure records only the nontrivial orientation of the half-sandwich commutation estimate.

• bound : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) fun (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) => strategy.state.qSDDCore (fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) => star (ldSandwichLineOnePointCS_Aord strategy.state params family hi q gs)) fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) => star (ldSandwichLineOnePointCS_Arot strategy.state params family hi q gs)) ≤ MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1)

  The averaged raw-core bound.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_adjointRawCore {𝔓 : 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 𝔓) (gamma zeta : ℝ) {k i : ℕ} (hi : i < k) (_hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) fun (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) => strategy.state.qSDDCore (fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) => star (ldSandwichLineOnePointCS_Aord strategy.state params family hi q gs)) fun (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) => star (ldSandwichLineOnePointCS_Arot strategy.state params family hi q gs)) ≤ MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1)

The adjoint-oriented estimate for the paper's eq:add-in-the-bot term.

The generic closenessOfIP* applications need the adjoint-oriented D D^† square-distance term that appears in ld-pasting.tex:980--985 and is reused at lines 1005--1010.