Unselected add-in-u Step 1/2 Cauchy--Schwarz bounds

Unselected-family contraction inputs and raw √(2δ) estimates for the first two add-in-u moves in the self-improvement chain: the counterpart of the vendored SelfImprovement/Theorems/Results/AddInUStep12/Raw.lean (under MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10, section "Port conventions").

Contents

• addInU_step1_C_contraction, addInU_step2_C_contraction: the contraction side conditions ∑ₐ C_a^* C_a ≤ 1 and ∑ₐ C_a C_a^* ≤ 1 of the weighted Cauchy--Schwarz bounds, as inequalities in K →L[ℂ] K.
• addInU_cs_chain_step1_abs_le_sqrt_two_delta, addInU_cs_chain_step2_abs_le_sqrt_two_delta: |Q₀ − Q₁| ≤ √(2δ) and |Q₁ − Q₂| ≤ √(2δ).

Every scalar is strategy.state.ev of a joint operator; leftTensor A, rightTensor A and opTensor A B are strategy.state.L A, strategy.state.R A and strategy.state.opTensor A B, and Xᴴ is star X. The vendored Hermitian facts (Matrix.nonneg_iff_posSemidef.mp (…outcome_pos _)).isHermitian.eq and the Matrix.conjTranspose_sum/conjTranspose_opTensor computation of Kᴴ = K are (IsSelfAdjoint.of_nonneg …).star_eq, the positivity coming from the keystone (opTensor_nonneg, rightTensor_nonneg, leftTensor_nonneg). The vendored proofs pass strategy.isNormalized to closenessOfInnerProduct_right/_left; the ported Cauchy--Schwarz bounds (Co Preliminaries/SwitchSandwichPrep/InnerProduct) have no normalization hypothesis, so it is dropped. No statement of the vendored file carries a swap, density or normalization hypothesis.

The two contraction proofs share the step ∑ₐ Pₐ K²ₐ Pₐ ≤ ∑ₐ Pₐ = 1 for self-adjoint idempotents Pₐ summing to one and K²ₐ ≤ 1, which is addInU_sum_projection_sandwich_le_one over any star-ordered ring; the vendored proofs repeat it inline.

Not ported

Every declaration of the vendored file has a counterpart here.

New here

• addInU_sum_projection_sandwich_le_one: the sandwich step shared by the two contraction lemmas.
• addInU_sum_fiber_collapse: the collapse of ∑ₐ ∑_h onto the fibre a = h(v), shared by the two raw bounds (the vendored proofs repeat it inline as hAvg).

References

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

• references/ldt-paper/self_improvement.tex lines 255–297 (eq:move-one, eq:move-another)
• blueprint/src/chapter/ch07_self_improvement.tex

theorem MIPRE.LIDT.Co.SelfImprovement.addInU_sum_projection_sandwich_le_one {R : Type u_3} {ι : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Fintype ι] (Kf P : ι → R) (hK : ∀ (a : ι), Kf a * Kf a ≤ 1) (hP : ∀ (a : ι), IsSelfAdjoint (P a)) (hPP : ∀ (a : ι), P a * P a = P a) (hsum : ∑ a : ι, P a = 1) : ∑ a : ι, P a * (Kf a * Kf a) * P a ≤ 1

The sandwich step of the two contraction lemmas: if the Pₐ are self-adjoint idempotents summing to 1 and Kₐ Kₐ ≤ 1, then ∑ₐ Pₐ (Kₐ Kₐ) Pₐ ≤ 1.

theorem MIPRE.LIDT.Co.SelfImprovement.addInU_sum_fiber_collapse {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (V : VecState K) (v : MIPStarRE.LDT.Point params) (X : MIPStarRE.LDT.Fq params → MIPStarRE.LDT.Polynomial params → K →L[ℂ] K) (hX : ∀ (a : MIPStarRE.LDT.Fq params) (h : MIPStarRE.LDT.Polynomial params), h.toFun v ≠ a → X a h = 0) : ∑ a : MIPStarRE.LDT.Fq params, ∑ h : MIPStarRE.LDT.Polynomial params, V.ev (X a h) = ∑ h : MIPStarRE.LDT.Polynomial params, V.ev (X (h.toFun v) h)

Collapsing a double sum ∑ₐ ∑_h ev(X a h) onto the fibre a = h(v), when X a h vanishes off it: the step that turns the fibre-indexed Cauchy--Schwarz sums of the two raw bounds into the single sums over h of the algebraic alignment.

Raw Cauchy--Schwarz bound for the add-in-u Step 1 difference

This section proves the raw |Q₀ - Q₁| ≤ √(2δ) bound from references/ldt-paper/self_improvement.tex, lines 255--277 (eq:move-one).

The proof combines:

• addInU_cs_chain_step1_diff_eq (algebraic alignment to commutator-times-PSD),
• addInU_pointMeasurement_snd_selfConsistency (A^v self-consistency lifted to the (u, v) average),
• addInU_filtered_sandwiched_tensor_sum_le_one (filtered sandwich-tensor mass is a contraction),
• Preliminaries.closenessOfInnerProduct_right (the weighted Cauchy--Schwarz inner-product bound from prop:closeness-of-ip, eq:closeness4).

The analogous Step 2 bound (|Q₁ - Q₂| ≤ √(2δ)) is proved by the same strategy with closenessOfInnerProduct_left and the S.L-sandwiched analogue of the Step 1 contraction lemma.

theorem MIPRE.LIDT.Co.SelfImprovement.addInU_step1_C_contraction {𝔓 : 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 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (uv : MIPStarRE.LDT.Point params × MIPStarRE.LDT.Point params) : (∑ a : MIPStarRE.LDT.Fq params, star (∑ h : MIPStarRE.LDT.Polynomial params, if h.toFun uv.2 = a then strategy.state.opTensor ((sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h) (T.outcome h) * strategy.state.R ((strategy.pointMeasurement uv.2).outcome a) else 0) * ∑ h : MIPStarRE.LDT.Polynomial params, if h.toFun uv.2 = a then strategy.state.opTensor ((sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h) (T.outcome h) * strategy.state.R ((strategy.pointMeasurement uv.2).outcome a) else 0) ≤ 1

Cauchy--Schwarz contraction side condition for Step 1.

For a fixed (u, v), the right-placed sandwiched sum Σ_a (K_{u,v,a} · R A^v_a)^* · (K_{u,v,a} · R A^v_a) ≤ 1 where K_{u,v,a} = Σ_{h: h(v)=a} (M^u_h ⊗ T_h). This is the C side condition fed to closenessOfInnerProduct_right in the Step 1 raw bound proof.

theorem MIPRE.LIDT.Co.SelfImprovement.addInU_cs_chain_step1_abs_le_sqrt_two_delta {𝔓 : 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 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (delta : ℝ) (hssc : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas delta) : |addInUCSChainQ0 params strategy T - addInUCSChainQ1 params strategy T| ≤ √(2 * delta)

Raw |Q₀ - Q₁| ≤ √(2δ) bound for the add-in-u Step 1 Cauchy--Schwarz move.

Proves the paper's eq:move-one bound from references/ldt-paper/self_improvement.tex, lines 255--277, as a completed construction. The proof combines the algebraic alignment addInU_cs_chain_step1_diff_eq with the weighted Cauchy--Schwarz inner-product bound Preliminaries.closenessOfInnerProduct_right, the A^v self-consistency input via addInU_pointMeasurement_snd_selfConsistency, and the filtered-tensor contraction addInU_filtered_sandwiched_tensor_sum_le_one.

The hypothesis is the bipartite SSC for the unlifted point measurement on the single-point distribution; the lifted 2δ bound is constructed inside the proof via addInU_pointMeasurement_snd_selfConsistency.

theorem MIPRE.LIDT.Co.SelfImprovement.addInU_step2_C_contraction {𝔓 : 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 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (uv : MIPStarRE.LDT.Point params × MIPStarRE.LDT.Point params) : ∑ a : MIPStarRE.LDT.Fq params, (∑ h : MIPStarRE.LDT.Polynomial params, if h.toFun uv.2 = a then strategy.state.L ((strategy.pointMeasurement uv.2).outcome a) * strategy.state.opTensor ((sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h) (T.outcome h) else 0) * star (∑ h : MIPStarRE.LDT.Polynomial params, if h.toFun uv.2 = a then strategy.state.L ((strategy.pointMeasurement uv.2).outcome a) * strategy.state.opTensor ((sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h) (T.outcome h) else 0) ≤ 1

Cauchy--Schwarz contraction side condition for Step 2.

For a fixed (u, v), the left-placed sandwiched sum Σ_a (L A^v_a · K_{u,v,a}) · (L A^v_a · K_{u,v,a})^* ≤ 1 where K_{u,v,a} = Σ_{h: h(v)=a} (M^u_h ⊗ T_h). This is the C side condition fed to closenessOfInnerProduct_left in the Step 2 raw bound proof.

theorem MIPRE.LIDT.Co.SelfImprovement.addInU_cs_chain_step2_abs_le_sqrt_two_delta {𝔓 : 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 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (delta : ℝ) (hssc : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas delta) : |addInUCSChainQ1 params strategy T - addInUCSChainQ2 params strategy T| ≤ √(2 * delta)

Raw |Q₁ - Q₂| ≤ √(2δ) bound for the add-in-u Step 2 Cauchy--Schwarz move.

Proves the paper's eq:move-another bound from references/ldt-paper/self_improvement.tex, lines 279--297, as a completed construction. The proof combines the algebraic alignment addInU_cs_chain_step2_diff_eq with the weighted Cauchy--Schwarz inner-product bound Preliminaries.closenessOfInnerProduct_left, the A^v self-consistency input via addInU_pointMeasurement_snd_selfConsistency, and the filtered-tensor contraction addInU_filtered_sandwiched_tensor_sum_le_one.