Main scalar chain assembly

The core lemma evaluatedSlice_scalar_chain_bound that assembles the ten-step scalar approximation chain for lem:comm-data-processed-g. This is the heavyweight proof corresponding to references/ldt-paper/commutativity-G.tex, lines 72–131. Phases 1, 3, 4, 6–7, and 8–9 are supplied by the reverse and tail parts of the paper chain; Phase 2 uses the reindexing infrastructure from PhaseTwo.

theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_scalar_chain_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (gamma zeta : Error) (_hnorm : strategy.state.IsNormalized) (_hcomm : SDDOpRel strategy.state (uniformDistribution (GlobalVariance.PointPairQuestion params.next)) (CommutativityPoints.pointMeasurementProductLeft params.next strategy) (CommutativityPoints.pointMeasurementProductRight params.next strategy) (CommutativityPoints.commutativityPointsError params.next gamma)) (_hgamma_nonneg : 0 ≤ gamma) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (_hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (_hcons : family.ConsistentWithPoints strategy zeta) (_hself : family.StronglySelfConsistent strategy.state zeta) (_hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (_hpostSSC : SDDRel strategy.state (uniformDistribution (Point params.next)) (evaluatedPointFamilyLeft params family) (evaluatedPointFamilyRight params family) zeta) : 2 * ((avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) => ∑ ab : EvaluatedSliceOutcome params, evaluatedSliceABATerm params strategy family q ab) - avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) => ∑ ab : EvaluatedSliceOutcome params, evaluatedSliceABABTerm params strategy family q ab) ≤ commDataProcessedGError params gamma zeta