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.

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 leftTensor-sandwiched analogue of the Step 1 contraction lemma.

theorem MIPStarRE.LDT.SelfImprovement.addInU_cs_chain_step1_abs_le_sqrt_two_delta {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (delta : Error) (hssc : BipartiteSSCRel strategy.state (uniformDistribution (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 MIPStarRE.LDT.SelfImprovement.addInU_cs_chain_step2_abs_le_sqrt_two_delta {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (delta : Error) (hssc : BipartiteSSCRel strategy.state (uniformDistribution (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.