Sum-form local-variance chain (complete)

This section supplies the polynomial-sum reverse generalize-B bound (the last individual step bound) and the full chain-assembly lemma localVarianceDeviation_sum_le_localVarianceOfPointsError, which closes eq:equivalent-local-variance.

Individual sum-form step bounds (all available)

1. pointConditionedEventSelfConsistency_weighted_leftEdge_sum (2δ, Step 1)
2. axisParallelPointLineConsistency_weighted_rightToLeftLineQuestion_sum (2ε, Step 2)
3. generalizeBDeviationAtPolynomial_polysum_le_error (md/q forward, Step 3)
4. generalizeBReversePointwiseBound_polysum_le_error (md/q reverse, Step 4) — below
5. axisParallelPointLineConsistency_weighted_leftToRightLineQuestion_sum (2ε, Step 5)
6. pointConditionedEventSelfConsistency_weighted_rightEdge_sum (2δ, Step 6)

Six-step chain assembly

The chain assembly lemma localVarianceDeviation_sum_le_localVarianceOfPointsError (below) telescopes the six operator differences via ev_sum_conjTranspose_mul_sum_le, sums over g, swaps outer sums, and applies the six _sum bounds. The proof follows the sketch originally documented here (and tracked in #1137):

For each g, q:  A0_g(q) − A6_g(q) = Σ_{i=0}^5 (Ai_g(q) − A_{i+1}_g(q)).
By ev_sum_conjTranspose_mul_sum_le:
  ‖A0−A6‖² ≤ 6·Σ_i ‖Ai−A_{i+1}‖²   (pointwise).
Averaging over 𝒟 and summing over g:
  Σ_g avgOver ‖A0−A6‖² ≤ 6·Σ_i Σ_g avgOver ‖Ai−A_{i+1}‖².
Reindex each inner sum to a native distribution and apply the _sum bound.
Finally reindex the left side from 𝒟 to rerandomizeCoord.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBReversePointwiseBound_polysum_le_error {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) : (∑ g : Polynomial params, avgOver (axisParallelLineQuestionDistribution params) fun (qu : AxisParallelLineQuestion params) => have D := weightedGeneralizeBRightOperatorAtPolynomial params strategy G g qu - weightedGeneralizeBLeftOperatorAtPolynomial params strategy G g qu; ev strategy.state (Matrix.conjTranspose D * D)) ≤ generalizeBError params

Reverse generalize-B bound summed over all polynomials.

The reverse squared distance equals the forward one by ev_adjoint_sub_swap; therefore the polynomial-sum bound follows from the forward version generalizeBDeviationAtPolynomial_polysum_le_error. This supplies the sum-form Step 4 bound (the md/q reverse direction) for the six-step local-variance chain.

theorem MIPStarRE.LDT.GlobalVariance.localVarianceDeviation_sum_le_localVarianceOfPointsError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) (G : SubMeas (Polynomial params) ι) : ∑ g : Polynomial params, localVarianceDeviationAtPolynomial params strategy strategy.state G g ≤ localVarianceOfPointsError params eps delta

Chain assembly for eq:equivalent-local-variance.

This theorem closes the six-step sum-form local-variance chain. For each transport question q and polynomial g, the six operator differences telescope via ev_sum_conjTranspose_mul_sum_le, giving the pointwise inequality ‖A₀ − A₆‖² ≤ 6·Σᵢ ‖Aᵢ − Aᵢ₊₁‖². Summing over g and averaging over the uniform transport-question distribution and then swapping outer sums yields

Σ_g avgOver ‖A₀−A₆‖² ≤ 6·Σᵢ Σ_g avgOver ‖Aᵢ−Aᵢ₊₁‖².

Each inner term Σ_g avgOver ‖Aᵢ−Aᵢ₊₁‖² is reindexed to its native distribution and bounded by the corresponding _sum lemma (all six are now available on main). Finally the left side is reindexed from the transport-question distribution to rerandomizeCoord, and the localVarianceTransportChainError is absorbed into localVarianceOfPointsError.

This is the main theorem requested in #1088 and tracked in #1137.