Section 11 commutativity: G-stability overlap (step one)

First overlap-averaging step for the G-stability argument: averaging the common overlap term over Point params.next reduces to a single-coordinate integral.

References

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPStarRE.LDT.Commutativity.gCommOverlap_avgOver_fst {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (G : Fq params → SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) => gCommOverlapTerm params strategy G (pointHeight params q.1)) = avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => gCommOverlapTerm params strategy G x

Averaging the overlap term over evaluated-slice questions through the first point coordinate marginalizes to the uniform x : F_q average.

theorem MIPStarRE.LDT.Commutativity.gCommStability_raw_le_half_of {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (zeta : Error) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (hself : family.StronglySelfConsistent strategy.state zeta) {Outcome : Type u_2} [Fintype Outcome] (A B : IdxOpFamily (EvaluatedSliceQuestion params) Outcome (ι × ι)) (point : EvaluatedSliceQuestion params → Point params.next) (hmarg : (avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) => gCommOverlapTerm params strategy G (pointHeight params (point q))) = avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => gCommOverlapTerm params strategy G x) (hpointwise : ∀ (q : EvaluatedSliceQuestion params), qSDDOp strategy.state (A q) (B q) ≤ gCommOverlapTerm params strategy G (pointHeight params (point q))) : sddErrorOp strategy.state (uniformDistribution (EvaluatedSliceQuestion params)) A B ≤ zeta / 2

Any pointwise defect bound by the common overlap term inherits a raw zeta / 2 estimate after marginalizing to the slice SSC defect of G.

theorem MIPStarRE.LDT.Commutativity.gCommStability_raw_le_one_of {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (hnorm : strategy.state.IsNormalized) (G : Fq params → SubMeas (Polynomial params) ι) {Outcome : Type u_2} [Fintype Outcome] (A B : IdxOpFamily (EvaluatedSliceQuestion params) Outcome (ι × ι)) (point : EvaluatedSliceQuestion params → Point params.next) (hpointwise : ∀ (q : EvaluatedSliceQuestion params), qSDDOp strategy.state (A q) (B q) ≤ gCommOverlapTerm params strategy G (pointHeight params (point q))) : sddErrorOp strategy.state (uniformDistribution (EvaluatedSliceQuestion params)) A B ≤ 1

Any pointwise defect bound by the common overlap term is trivially at most 1.

theorem MIPStarRE.LDT.Commutativity.sddOpRel_of_sqrt_bound_from_half_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxOpFamily Question Outcome ι) (zeta : Error) (hz_nonneg : 0 ≤ zeta) (hhalf : sddErrorOp ψ 𝒟 A B ≤ zeta / 2) (hone : sddErrorOp ψ 𝒟 A B ≤ 1) : SDDOpRel ψ 𝒟 A B √zeta

Upgrade raw zeta / 2 and 1 bounds to the displayed sqrt zeta relation.

theorem MIPStarRE.LDT.Commutativity.gCommStability_overlap {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (zeta : Error) (hnorm : strategy.state.IsNormalized) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (hself : family.StronglySelfConsistent strategy.state zeta) : SDDOpRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params)) (commDataProcessedGStabilityOneLeft params strategy family G) (commDataProcessedGStabilityOneRight params strategy family G) √zeta

Overlap-only version of the first stability estimate.

This is not the paper's boundedness-driven scalar proof of clm:g-comm-stability: it bounds the current SDD package through the slice SSC overlap term ⟨ψ,(I-G^y)⊗G^y ψ⟩. It remains useful as an internal overlap lemma while the scalar-chain API is being completed.