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

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.qBipartiteLinearConsDefect {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) : Error

The linear (pre-max) form of the bipartite consistency defect.

Internal helper for the LdSandwichLineOnePoint Cauchy--Schwarz setup; exposed for a future file-split (#1127).

Equations

• MIPStarRE.LDT.Pasting.qBipartiteLinearConsDefect ψ A B = MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.opTensor A.total B.total) - MIPStarRE.LDT.qBipartiteMatchMass ψ A B

theorem MIPStarRE.LDT.Pasting.qBipartiteLinearConsDefect_option_eq_sum_some_complement {α : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype α] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (A : SubMeas (Option α) ιA) (B : SubMeas (Option α) ιB) (hBtotal : B.total = 1) (hAnone : A.outcome none = 0) (hBnone : B.outcome none = 0) : qBipartiteLinearConsDefect ψ A B = ∑ a : α, ev ψ (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.

This is the bookkeeping step that rewrites ⟨ψ|A_total ⊗ B_total|ψ⟩ - Σ_o ⟨ψ|A_o ⊗ B_o|ψ⟩ as Σ_a ⟨ψ|A_a ⊗ (I - B_a)|ψ⟩ when Bob's family is a measurement and both none outcomes vanish.

Internal helper for the LdSandwichLineOnePoint Cauchy--Schwarz setup; exposed for a future file-split (#1127).

theorem MIPStarRE.LDT.Pasting.qBipartiteLinearConsDefect_nonneg_of_right_total_one {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) (hBtotal : B.total = 1) : 0 ≤ qBipartiteLinearConsDefect ψ 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 maximum form without needing a pointwise absolute-value gap.

Internal helper for the LdSandwichLineOnePoint Cauchy--Schwarz setup; exposed for a future file-split (#1127).

theorem MIPStarRE.LDT.Pasting.bipartiteConsError_le_of_linearDefect_average_bound {Question : Type u_2} {Outcome : Type u_3} {ιA : Type u_4} {ιB : Type u_5} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (A B : IdxSubMeas Question Outcome ιA) (C : IdxSubMeas Question Outcome ιB) (η : Error) (hCtotal : ∀ (q : Question), (C q).total = 1) (hgap : (avgOver 𝒟 fun (q : Question) => qBipartiteLinearConsDefect ψ (A q) (C q)) ≤ (avgOver 𝒟 fun (q : Question) => qBipartiteLinearConsDefect ψ (B q) (C q)) + η) : bipartiteConsError ψ 𝒟 A C ≤ 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.

Internal helper for the LdSandwichLineOnePoint Cauchy--Schwarz setup; exposed for a future file-split (#1127).

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_sourceOutcomeSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : Error

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 ⟨ψ|A_a ⊗ (I-B_a)|ψ⟩.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : Error

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 orderedHalf† on the right.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_movedOutcomeSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : Error

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 MIPStarRE.LDT.Pasting.LdSandwichLineOnePointOutcomeSumCSRoute {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {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 + √(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 + √(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 MIPStarRE.LDT.Pasting.LdSandwichLineOnePointOutcomeSumCSAbsBounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {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| ≤ √(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| ≤ √(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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_orderedHalf {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) (gs : GHatTupleOutcome params (i + 1)) : Quantum.Op ι

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_rotatedHalf {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) (gs : GHatTupleOutcome params (i + 1)) : Quantum.Op ι

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_rightComplement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (q : SandwichedLineQuestion params k) (gs : GHatTupleOutcome params (i + 1)) : Quantum.Op ι

Right-hand complement selected by the completed polynomial outcome.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_Aord {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : SandwichedLineQuestion params k → GHatTupleOutcome params (i + 1) → Quantum.Op (ι × ι)

Raw ordered left tensor family used in the generic CS proposition.

Equations

• MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_Aord params family hi q gs = MIPStarRE.LDT.leftTensor (MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_orderedHalf params family hi q gs)

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_Arot {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : SandwichedLineQuestion params k → GHatTupleOutcome params (i + 1) → Quantum.Op (ι × ι)

Raw rotated left tensor family used in the generic CS proposition.

Equations

• MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_Arot params family hi q gs = MIPStarRE.LDT.leftTensor (MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_rotatedHalf params family hi q gs)

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_AordAdjointFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : IdxOpFamily (SandwichedLineQuestion params k) (GHatTupleOutcome params (i + 1)) (ι × ι)

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_ArotAdjointFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : IdxOpFamily (SandwichedLineQuestion params k) (GHatTupleOutcome params (i + 1)) (ι × ι)

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointAdjointRawLeftFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (_hi : i < k) : IdxOpFamily (SandwichedLineQuestion params k) (GHatTupleOutcome params (i + 1)) (ι × ι)

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointAdjointRawRightFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (_hi : i < k) : IdxOpFamily (SandwichedLineQuestion params k) (GHatTupleOutcome params (i + 1)) (ι × ι)

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_adjointRawCommutation_originalOutcome {ι : 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) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) : SDDOpRel ψ (uniformDistribution (SandwichedLineQuestion params k)) (ldSandwichLineOnePointAdjointRawLeftFamily params family hi) (ldSandwichLineOnePointAdjointRawRightFamily params family hi) (commuteGHalfSandwichError params gamma zeta (i + 1))

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

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointAdjointRawLeftFamily_eq_CS_Aord_adjoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) (gs : GHatTupleOutcome params (i + 1)) : (ldSandwichLineOnePointAdjointRawLeftFamily params family hi q).outcome gs = Matrix.conjTranspose (ldSandwichLineOnePointCS_Aord params family hi q gs)

The adjoint raw family agrees with the ordered CS family.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointAdjointRawRightFamily_eq_CS_Arot_adjoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) (q : SandwichedLineQuestion params k) (gs : GHatTupleOutcome params (i + 1)) : (ldSandwichLineOnePointAdjointRawRightFamily params family hi q).outcome gs = Matrix.conjTranspose (ldSandwichLineOnePointCS_Arot params family hi q gs)

The adjoint raw family agrees with the rotated CS family.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_adjointRawCommutation_qSDDCore_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hcomm : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params strategy.state family gamma zeta j) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) : (avgOver (uniformDistribution (SandwichedLineQuestion params k)) fun (q : SandwichedLineQuestion params k) => qSDDCore strategy.state (fun (gs : GHatTupleOutcome params (i + 1)) => Matrix.conjTranspose (ldSandwichLineOnePointCS_Aord params family hi q gs)) fun (gs : GHatTupleOutcome params (i + 1)) => Matrix.conjTranspose (ldSandwichLineOnePointCS_Arot params family hi q gs)) ≤ commuteGHalfSandwichError params gamma zeta (i + 1)

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

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_Cfirst {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : SandwichedLineQuestion params k → GHatTupleOutcome params (i + 1) → Unit → Quantum.Op (ι × ι)

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_Csecond {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : SandwichedLineQuestion params k → GHatTupleOutcome params (i + 1) → Unit → Quantum.Op (ι × ι)

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_firstSourceRaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : Error

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_firstTargetRaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : Error

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_secondSourceRaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : Error

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 MIPStarRE.LDT.Pasting.ldSandwichLineOnePointCS_secondTargetRaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k i : ℕ} (hi : i < k) : Error

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 MIPStarRE.LDT.Pasting.LdSandwichLineOnePointCSFacts {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {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 (proved below) 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.

The construction lemma below proves the unit bounds and regrouping equalities; the remaining live analytic endpoint is the adjoint-oriented raw-core estimate recorded by LdSandwichLineOnePointAdjointRawCoreBound.

• adjointRawCore : (avgOver (uniformDistribution (SandwichedLineQuestion params k)) fun (q : SandwichedLineQuestion params k) => qSDDCore strategy.state (fun (gs : GHatTupleOutcome params (i + 1)) => Matrix.conjTranspose (ldSandwichLineOnePointCS_Aord params family hi q gs)) fun (gs : GHatTupleOutcome params (i + 1)) => Matrix.conjTranspose (ldSandwichLineOnePointCS_Arot params family hi q gs)) ≤ commuteGHalfSandwichError params gamma zeta (i + 1)
• firstUnitBound (q : SandwichedLineQuestion params k) : ∑ gs : GHatTupleOutcome params (i + 1), (∑ u : Unit, ldSandwichLineOnePointCS_Cfirst params strategy family hi q gs u).conjTranspose * ∑ u : Unit, ldSandwichLineOnePointCS_Cfirst params strategy family hi q gs u ≤ 1
• secondUnitBound (q : SandwichedLineQuestion params k) : ∑ gs : GHatTupleOutcome params (i + 1), (∑ u : Unit, ldSandwichLineOnePointCS_Csecond params strategy family hi q gs u) * (∑ u : Unit, ldSandwichLineOnePointCS_Csecond params strategy family hi q gs u).conjTranspose ≤ 1
• source_eq_firstSourceRaw : ldSandwichLineOnePoint_prefix_sourceOutcomeSum params strategy family hi = ldSandwichLineOnePointCS_firstSourceRaw params strategy family hi
• afterFirst_eq_firstTargetRaw : ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum params strategy family hi = ldSandwichLineOnePointCS_firstTargetRaw params strategy family hi
• afterFirst_eq_secondSourceRaw : ldSandwichLineOnePoint_prefix_afterFirstCSOutcomeSum params strategy family hi = ldSandwichLineOnePointCS_secondSourceRaw params strategy family hi
• moved_eq_secondTargetRaw : ldSandwichLineOnePoint_prefix_movedOutcomeSum params strategy family hi = ldSandwichLineOnePointCS_secondTargetRaw params strategy family hi

structure MIPStarRE.LDT.Pasting.LdSandwichLineOnePointAdjointRawCoreBound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {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 : (avgOver (uniformDistribution (SandwichedLineQuestion params k)) fun (q : SandwichedLineQuestion params k) => qSDDCore strategy.state (fun (gs : GHatTupleOutcome params (i + 1)) => Matrix.conjTranspose (ldSandwichLineOnePointCS_Aord params family hi q gs)) fun (gs : GHatTupleOutcome params (i + 1)) => Matrix.conjTranspose (ldSandwichLineOnePointCS_Arot params family hi q gs)) ≤ commuteGHalfSandwichError params gamma zeta (i + 1)

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_adjointRawCore {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {k i : ℕ} (hi : i < k) (_hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) : (avgOver (uniformDistribution (SandwichedLineQuestion params k)) fun (q : SandwichedLineQuestion params k) => qSDDCore strategy.state (fun (gs : GHatTupleOutcome params (i + 1)) => Matrix.conjTranspose (ldSandwichLineOnePointCS_Aord params family hi q gs)) fun (gs : GHatTupleOutcome params (i + 1)) => Matrix.conjTranspose (ldSandwichLineOnePointCS_Arot params family hi q gs)) ≤ 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^\dagger$ square-distance term that appears in ld-pasting.tex:980--985 and is reused at lines 1005--1010.