Add-in-u Cauchy--Schwarz algebraic alignment

Algebraic operator-rewrites that align the add-in-u chain differences with the forms used in the Cauchy--Schwarz estimates from the paper.

Contents

• addInU_step1/step2/step3/step4_pointwise_op_eq (private) — operator-level difference rewrites for the four scalar moves.
• addInU_cs_chain_step1/step2/step3/step4_diff_eq — algebraic alignment of the diagonal chain differences to commutator-times-PSD form.
• addInU_selected_cs_chain_step1/step2/step3/step4_diff_eq — the same algebraic alignments before specializing the add-in-u selection.

The contraction and raw √(2δ) estimates using these identities live in AddInUStep12.Raw; the selected-family raw estimates live in AddInUStep12.Selected.

References

• references/ldt-paper/self_improvement.tex lines 255–297
• blueprint/src/chapter/ch07_self_improvement.tex

Algebraic CS-alignment for the add-in-u Step 1/2 differences

This section records pure operator-algebra rewrites that bring the differences addInUCSChainQ1 - addInUCSChainQ0 and addInUCSChainQ2 - addInUCSChainQ1 into the shapes required by the paper's Cauchy--Schwarz steps eq:move-one-cauchy-schwarz and eq:move-another-cauchy-schwarz (references/ldt-paper/self_improvement.tex, lines 261--266 and 285--289). The reverse-difference companions give the downstream orientation Q₀ - Q₁ and Q₁ - Q₂ without repeating subtraction bookkeeping.

They do not discharge the Cauchy--Schwarz estimate itself; they reduce the raw |Q₁ - Q₀| ≤ √(2δ) and |Q₁ - Q₂| ≤ √(2δ) bounds to (a) a sandwich-form Cauchy--Schwarz on the resulting D · (M^u_h ⊗ T_h) · D'-style expression, plus (b) the two square-root inputs available via addInU_pointMeasurement_snd_selfConsistency and addInU_filtered_sandwiched_tensor_sum_le_one.

Names are deliberately suffixed _diff_eq to keep them honest as intermediate algebraic identities rather than as the final scalar bounds.

theorem MIPStarRE.LDT.SelfImprovement.addInU_cs_chain_step1_diff_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInUCSChainQ1 params strategy T - addInUCSChainQ0 params strategy T = avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.2; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state ((leftTensor Av - rightTensor Av) * (opTensor Mh (T.outcome h) * rightTensor Av))

Algebraic CS-alignment for the Q₀ → Q₁ step.

Rewrites the difference addInUCSChainQ1 - addInUCSChainQ0 in the exact form appearing on the LHS of eq:move-one-cauchy-schwarz (paper lines 261--266): the inner-product of the commutator A^v_{h(v)} ⊗ I − I ⊗ A^v_{h(v)} with M^u_h ⊗ T_h · (I ⊗ A^v_{h(v)}), averaged over (u, v) and summed over h.

This identity is purely algebraic; the actual √(2δ) bound still requires the operator Cauchy--Schwarz step plus addInU_pointMeasurement_snd_selfConsistency.

theorem MIPStarRE.LDT.SelfImprovement.addInU_cs_chain_step2_diff_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInUCSChainQ2 params strategy T - addInUCSChainQ1 params strategy T = avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.2; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state (leftTensor Av * (opTensor Mh (T.outcome h) * (leftTensor Av - rightTensor Av)))

Algebraic CS-alignment for the Q₁ → Q₂ step.

Rewrites the difference addInUCSChainQ2 - addInUCSChainQ1 in the exact form appearing on the LHS of eq:move-another-cauchy-schwarz (paper lines 285--289): the inner-product of (A^v_{h(v)} · M^u_h) ⊗ T_h with the commutator A^v_{h(v)} ⊗ I − I ⊗ A^v_{h(v)}, averaged over (u, v) and summed over h. The Lean statement keeps the equivalent factored form (A^v_{h(v)} ⊗ I) · (M^u_h ⊗ T_h) before the commutator.

This identity is purely algebraic; the actual √(2δ) bound still requires the operator Cauchy--Schwarz step plus addInU_pointMeasurement_snd_selfConsistency and addInU_filtered_sandwiched_tensor_sum_le_one.

theorem MIPStarRE.LDT.SelfImprovement.addInU_cs_chain_step1_reverse_diff_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInUCSChainQ0 params strategy T - addInUCSChainQ1 params strategy T = -avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.2; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state ((leftTensor Av - rightTensor Av) * (opTensor Mh (T.outcome h) * rightTensor Av))

Reverse-orientation form of addInU_cs_chain_step1_diff_eq.

This is the same algebraic identity as the Q₀ → Q₁ rewrite, stated in the Q₀ - Q₁ orientation used by the later absolute-value chain.

theorem MIPStarRE.LDT.SelfImprovement.addInU_cs_chain_step2_reverse_diff_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInUCSChainQ1 params strategy T - addInUCSChainQ2 params strategy T = -avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.2; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state (leftTensor Av * (opTensor Mh (T.outcome h) * (leftTensor Av - rightTensor Av)))

Reverse-orientation form of addInU_cs_chain_step2_diff_eq.

This is the same algebraic identity as the Q₁ → Q₂ rewrite, stated in the Q₁ - Q₂ orientation used by the later absolute-value chain.

theorem MIPStarRE.LDT.SelfImprovement.addInU_cs_chain_step3_diff_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInUCSChainQ2 params strategy T - addInUCSChainQ3 params strategy T = avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.1; have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.2; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state (opTensor ((Av - Au) * Mh * Av) (T.outcome h))

Algebraic CS-alignment for the Q₂ → Q₃ step.

Rewrites the difference addInUCSChainQ2 - addInUCSChainQ3 in the exact form appearing on the LHS of eq:change-one-cauchy-schwarz (paper lines 306--311): the expectation of ((A^v_{h(v)} - A^u_{h(u)}) · H^u_h · A^v_{h(v)}) ⊗ T_h, averaged over (u, v) and summed over h.

The paper writes the middle factor as the fiber operator M^u_o; in this formalization the preceding o-sum has already been collapsed along o = h(u), so the same factor appears as H^u_h = (sandwichedPolynomialSubMeasAt params strategy T u).outcome h.

This identity is purely algebraic; the operator Cauchy--Schwarz estimate is proved downstream by add_in_u_cs_chain_q2_q3_factored_cs.

Selection-parametrized Step 1/2 algebraic identities

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step1_diff_eq {ι : 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) : addInUSelectedCSChainQ1 params strategy M T S - addInUSelectedCSChainQ0 params strategy M T S = avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ ah ∈ addInUSelectionPairs params S uv.1, have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.2; have Moh := (M uv.1).outcome ah.1; ev strategy.state ((leftTensor Av - rightTensor Av) * (opTensor Moh (T.outcome ah.2) * rightTensor Av))

Algebraic CS-alignment for the selected Q₀ → Q₁ step.

This is the selection-parametrized form of addInU_cs_chain_step1_diff_eq. The identity is stated in the same orientation as the diagonal chain, namely as Q₁ - Q₀. It rewrites the scalar difference using the same commutator A^v_{h(v)} ⊗ I − I ⊗ A^v_{h(v)}, but sums only over the selected pairs (o,h) ∈ S_u and leaves the arbitrary outcome operator M^u_o in place.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step2_diff_eq {ι : 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) : addInUSelectedCSChainQ2 params strategy M T S - addInUSelectedCSChainQ1 params strategy M T S = avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ ah ∈ addInUSelectionPairs params S uv.1, have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.2; have Moh := (M uv.1).outcome ah.1; ev strategy.state (leftTensor Av * (opTensor Moh (T.outcome ah.2) * (leftTensor Av - rightTensor Av)))

Algebraic CS-alignment for the selected Q₁ → Q₂ step.

This is the selection-parametrized form of addInU_cs_chain_step2_diff_eq, with the arbitrary selected outcome operator M^u_o in the left tensor factor.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step1_reverse_diff_eq {ι : 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) : addInUSelectedCSChainQ0 params strategy M T S - addInUSelectedCSChainQ1 params strategy M T S = -avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ ah ∈ addInUSelectionPairs params S uv.1, have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.2; have Moh := (M uv.1).outcome ah.1; ev strategy.state ((leftTensor Av - rightTensor Av) * (opTensor Moh (T.outcome ah.2) * rightTensor Av))

Reverse-orientation selected form of addInU_selected_cs_chain_step1_diff_eq.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step2_reverse_diff_eq {ι : 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) : addInUSelectedCSChainQ1 params strategy M T S - addInUSelectedCSChainQ2 params strategy M T S = -avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ ah ∈ addInUSelectionPairs params S uv.1, have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.2; have Moh := (M uv.1).outcome ah.1; ev strategy.state (leftTensor Av * (opTensor Moh (T.outcome ah.2) * (leftTensor Av - rightTensor Av)))

Reverse-orientation selected form of addInU_selected_cs_chain_step2_diff_eq.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step3_diff_eq {ι : 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) : addInUSelectedCSChainQ2 params strategy M T S - addInUSelectedCSChainQ3 params strategy M T S = avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ ah ∈ addInUSelectionPairs params S uv.1, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.1; have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.2; have Moh := (M uv.1).outcome ah.1; ev strategy.state (opTensor ((Av - Au) * Moh * Av) (T.outcome ah.2))

Algebraic CS-alignment for the selected Q₂ → Q₃ step.

This rewrites the first point-replacement move for an arbitrary selected outcome family. The only changed factor is the left copy of the point projector, from A^v_{h(v)} to A^u_{h(u)}.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step4_diff_eq {ι : 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) : addInUSelectedCSChainQ3 params strategy M T S - addInUSelectedCSChainQ4 params strategy M T S = avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ ah ∈ addInUSelectionPairs params S uv.1, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.1; have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.2; have Moh := (M uv.1).outcome ah.1; ev strategy.state (opTensor (Au * Moh * (Av - Au)) (T.outcome ah.2))

Algebraic CS-alignment for the selected Q₃ → Q₄ step.

This rewrites the second point-replacement move for an arbitrary selected outcome family. The only changed factor is the right copy of the point projector, from A^v_{h(v)} to A^u_{h(u)}.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step3_reverse_diff_eq {ι : 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) : addInUSelectedCSChainQ3 params strategy M T S - addInUSelectedCSChainQ2 params strategy M T S = -avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ ah ∈ addInUSelectionPairs params S uv.1, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.1; have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.2; have Moh := (M uv.1).outcome ah.1; ev strategy.state (opTensor ((Av - Au) * Moh * Av) (T.outcome ah.2))

Reverse-orientation selected form of addInU_selected_cs_chain_step3_diff_eq.

theorem MIPStarRE.LDT.SelfImprovement.addInU_selected_cs_chain_step4_reverse_diff_eq {ι : 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) : addInUSelectedCSChainQ4 params strategy M T S - addInUSelectedCSChainQ3 params strategy M T S = -avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ ah ∈ addInUSelectionPairs params S uv.1, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.1; have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy ah.2 uv.2; have Moh := (M uv.1).outcome ah.1; ev strategy.state (opTensor (Au * Moh * (Av - Au)) (T.outcome ah.2))

Reverse-orientation selected form of addInU_selected_cs_chain_step4_diff_eq.

theorem MIPStarRE.LDT.SelfImprovement.addInU_cs_chain_step4_diff_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : addInUCSChainQ3 params strategy T - addInUCSChainQ4 params strategy T = avgOver (uniformDistribution (Point params × Point params)) fun (uv : Point params × Point params) => ∑ h : Polynomial params, have Au := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.1; have Av := GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h uv.2; have Mh := (sandwichedPolynomialSubMeasAt params strategy T uv.1).outcome h; ev strategy.state (opTensor (Au * Mh * (Av - Au)) (T.outcome h))

Algebraic CS-alignment for the Q₃ → Q₄ step.

Rewrites the difference addInUCSChainQ3 - addInUCSChainQ4 in the exact form appearing on the left-hand side of eq:change-another (paper lines 326--332): the expectation of (A^u_{h(u)} · H^u_h · (A^v_{h(v)} - A^u_{h(u)})) ⊗ T_h, averaged over (u, v) and summed over h.

This identity is purely algebraic; the actual operator Cauchy--Schwarz step is provided by add_in_u_cs_chain_q3_q4_factored_cs.