Sum-form (cardinality-free) 2ε axis-parallel consistency endpoints

The lemmas below are the polynomial-sum (i.e. unnormalized ∑_g) analogues of the per-g 2ε endpoints above. They keep the answer space at Fq params rather than postprocessing to the per-g Option Unit event, then group polynomials by the common value g(u) via the cabApproxDelta multiplier if a = g s.1 then rightTensor (G_g)^{1/2} else 0. Combined with the submeasurement contraction ∑_{g : g(u) = a} G_g ≤ I from rightPolynomialWeightSqrt_grouped_contraction, this gives 2ε for the full polynomial sum, with no polynomial-cardinality loss. These are the steps 2 and 5 sum-level inputs to eq:equivalent-local-variance (references/ldt-paper/expansion.tex:317--321).

theorem MIPStarRE.LDT.GlobalVariance.axisParallelBaseEventApproximation_weighted_sample_sum {ι : 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, avgOver (uniformDistribution (AxisParallelTestSample params)) fun (s : AxisParallelTestSample params) => have qu := ({ base := s.1, direction := s.2 }, s.1); have D := weightedGeneralizeBLeftOperatorAtPolynomial params strategy G g qu - weightedPointConditionedRightOperatorAtPolynomial params strategy G g s.1; ev strategy.state (Matrix.conjTranspose D * D)) ≤ 2 * eps

Sum-level base-sample form of the 2ε axis-parallel consistency move, oriented with the line event on the left register and the point event on the right register.

This is the polynomial-sum version of axisParallelBaseEventApproximation_weighted_sample: instead of fixing g and postprocessing both sides to the Option Unit event a = g(u), we keep the full Fq params answer space and use the multiplier C s a g := if a = g s.1 then rightTensor (G_g)^{1/2} else 0 inside prop:cab-approx-delta. The contraction ∀ s a, ∑_g (C s a g)ᴴ * (C s a g) ≤ I is supplied by rightPolynomialWeightSqrt_grouped_contraction, which uses the submeasurement inequality ∑_{g : g(s.1) = a} G_g ≤ I. Consequently the bound is 2ε for the polynomial sum, with no polynomial-cardinality loss.

theorem MIPStarRE.LDT.GlobalVariance.axisParallelPointLineConsistency_weighted_leftToRightLineQuestion_sum {ι : 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, avgOver (axisParallelLineQuestionDistribution params) fun (qu : AxisParallelLineQuestion params) => have D := weightedGeneralizeBLeftOperatorAtPolynomial params strategy G g qu - weightedPointConditionedRightOperatorAtPolynomial params strategy G g qu.2; ev strategy.state (Matrix.conjTranspose D * D)) ≤ 2 * eps

Sum-level form of the weighted line-to-point approximation (expansion.tex:309--310, paper step 5) on the axisParallelLineQuestionDistribution distribution.

This is the polynomial-sum analogue of axisParallelPointLineConsistency_weighted_leftToRightLineQuestion. After reindexing the line-question sampling along its incident-pair structure (using the existing rebasing covariance for the line operator), it reduces to the sum-level base-sample bound axisParallelBaseEventApproximation_weighted_sample_sum.

theorem MIPStarRE.LDT.GlobalVariance.axisParallelPointLineConsistency_weighted_rightToLeftLineQuestion_sum {ι : 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, avgOver (axisParallelLineQuestionDistribution params) fun (qu : AxisParallelLineQuestion params) => have D := weightedPointConditionedRightOperatorAtPolynomial params strategy G g qu.2 - weightedGeneralizeBLeftOperatorAtPolynomial params strategy G g qu; ev strategy.state (Matrix.conjTranspose D * D)) ≤ 2 * eps

Sum-level form of the reverse weighted point-to-line approximation (expansion.tex:306--307, paper step 2) on the axisParallelLineQuestionDistribution distribution.

This is the polynomial-sum analogue of axisParallelPointLineConsistency_weighted_rightToLeftLineQuestion. Each summand is unchanged after swapping the two endpoint operators, so this reduces to axisParallelPointLineConsistency_weighted_leftToRightLineQuestion_sum.