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

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

The fact record LdSandwichLineOnePointCSFacts is assembled from the adjoint raw-core bound (ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_facts): the two unit-side bounds are the completeness of the half-products, placed by S.L and multiplied by a right complement between 0 and 1 (S.opTensor_le_leftTensor), and the four scalar identities regroup the outcome sums through S.leftTensor_mul_opTensor and S.opTensor_mul_leftTensor, in place of the vendored Kronecker calculations. The ported Preliminaries.closenessOfIPAdjoint and Preliminaries.closenessOfIP then give the two absolute-value bounds on the vector state of the strategy, without the vendored normalization argument, and the one-sided route, the expanded bound and the linear-defect bound follow as in the vendored file. The vendored conjugate transpose ᴴ is star. 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

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_facts {𝔓 : 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) : LdSandwichLineOnePointCSFacts params strategy family gamma zeta hi

Assemble the line-one-point CS facts from the single adjoint raw-core estimate.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_abs_bounds {𝔓 : 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) : LdSandwichLineOnePointOutcomeSumCSAbsBounds params strategy family gamma zeta hi

Narrow analytic endpoint for the two off-diagonal Cauchy--Schwarz moves in their absolute-value closenessOfIP output shape.

The generic applications of Preliminaries.closenessOfIPAdjoint and Preliminaries.closenessOfIP are proved here, on the vector state of the strategy. The CS facts record proves the measurement-completeness/unit bounds and scalar regrouping equalities; the remaining nontrivial estimate is the adjoint raw-core orientation lemma ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_adjointRawCore.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_route {𝔓 : 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) : LdSandwichLineOnePointOutcomeSumCSRoute params strategy family gamma zeta hi

One-sided route for the two off-diagonal Cauchy--Schwarz moves in ld-pasting.tex:964--1010.

The substantive analytic residual is the pair of absolute-value estimates ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_abs_bounds; this lemma only converts those two closenessOfIP-style bounds into the one-sided inequalities consumed by the downstream scalar transport.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_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 : ℝ) {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) => ∑ a : MIPStarRE.LDT.Fq params, strategy.state.ev (strategy.state.opTensor ((ldSandwichLineOnePointPrefixOriginalFamily params family hi q).outcome (some a)) (1 - (ldSandwichLineOnePointRightFamily params strategy family k i q).outcome (some a)))) ≤ (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) fun (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) => ∑ a : MIPStarRE.LDT.Fq params, strategy.state.ev (strategy.state.opTensor ((ldSandwichLineOnePointPrefixMovedFamily params family hi q).outcome (some a)) (1 - (ldSandwichLineOnePointRightFamily params strategy family k i q).outcome (some a)))) + 2 * √(MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1))

The remaining expanded off-diagonal scalar transport in lem:ld-sandwich-line-one-point.

This is the exact scalar form of ld-pasting.tex:954--1024 after the linear consistency defect has been expanded as Σ_a ev(A_a ⊗ (I − B_a)). The only remaining analytic content is the paper's two averaged Cauchy--Schwarz moves plus the prefix-completeness collapse; the surrounding qBipartiteLinearConsDefect bookkeeping is proved in ldSandwichLineOnePoint_prefix_linearDefect_average_cauchySchwarz_bound.

theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePoint_prefix_linearDefect_average_cauchySchwarz_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 : ℝ) {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) => qBipartiteLinearConsDefect strategy.state (ldSandwichLineOnePointPrefixOriginalFamily params family hi q) (ldSandwichLineOnePointRightFamily params strategy family k i q)) ≤ (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) fun (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) => qBipartiteLinearConsDefect strategy.state (ldSandwichLineOnePointPrefixMovedFamily params family hi q) (ldSandwichLineOnePointRightFamily params strategy family k i q)) + 2 * √(MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1))

Linear-defect reduction for the expanded off-diagonal post-deletion transport in lem:ld-sandwich-line-one-point.

The paper's two Cauchy--Schwarz moves and prefix collapse from references/ldt-paper/ld-pasting.tex:954--1024 act on the expanded scalar expression Σ_a ev(A_a ⊗ (I − B_a)). This lemma proves the exact bookkeeping reduction from the averaged linear consistency defects to that expanded residual, using the measurement-valued right family and the fact that both option-valued families have zero none mass. The remaining analytic gap is therefore the split Cauchy--Schwarz route ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_route; the arithmetic absorption into ν₅ is proved separately in ldSandwichLineOnePoint_endpoint_comm_error_le.