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

Selected-family contraction inputs and raw √(2δ) estimates for the first two add-in-u moves in the self-improvement chain.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step1_abs_le_sqrt_two_delta {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) (delta : Error) (hssc : BipartiteSSCRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas delta) : |addInUSelectedCSChainQ0 params strategy M T S - addInUSelectedCSChainQ1 params strategy M T S| ≤ √(2 * delta)

Raw selected |Q₀ - Q₁| ≤ √(2δ) bound for the first add-in-u move.

This is the selection-parametrized form of addInU_cs_chain_step1_abs_le_sqrt_two_delta. It applies the weighted Cauchy--Schwarz estimate to the selected pairs (o,h) ∈ S_u; the contraction side condition is addInU_selected_step1_C_contraction.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step2_abs_le_sqrt_two_delta {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (M : IdxSubMeas (Point params) Outcome ι) (T : SubMeas (Polynomial params) ι) (S : AddInUSelection params Outcome) (delta : Error) (hssc : BipartiteSSCRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas delta) : |addInUSelectedCSChainQ1 params strategy M T S - addInUSelectedCSChainQ2 params strategy M T S| ≤ √(2 * delta)

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

This is the selection-parametrized form of addInU_cs_chain_step2_abs_le_sqrt_two_delta. It uses the left-action Cauchy--Schwarz estimate with the selected Step 2 contraction side condition.