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. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/GCommStability/OverlapOne.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The relations are strategy.state.SDDOpRel, a vector-state relation on joint operators, and sddOpRel_of_sqrt_bound_from_half_one takes a vector state V : VecState K in place of the vendored one-space state ψ. The vendored hypothesis hnorm : strategy.state.IsNormalized of gCommOverlapTerm_le_one, gCommStability_raw_le_one_of and gCommStability_overlap is dropped, as the port conventions drop hψ : ψ.IsNormalized: a vector state has ev 1 = 1 (VecState.ev_one_of_isNormalized). Callers omit that argument.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

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

theorem MIPRE.LIDT.Co.Commutativity.gCommOverlap_avgOver_point {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) fun (w : MIPStarRE.LDT.Point params.next) => gCommOverlapTerm params strategy G (MIPStarRE.LDT.pointHeight params w)) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => gCommOverlapTerm params strategy G x

Averaging the common overlap term over Point params.next depends only on the final coordinate x : F_q.

theorem MIPRE.LIDT.Co.Commutativity.gCommOverlap_avgOver_fst {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => gCommOverlapTerm params strategy G (MIPStarRE.LDT.pointHeight params q.1)) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.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 MIPRE.LIDT.Co.Commutativity.gCommOverlapTerm_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (x : MIPStarRE.LDT.Fq params) : gCommOverlapTerm params strategy G x ≤ 1

The common overlap term is always at most 1. The vendored lemma asks for a normalized state.

theorem MIPRE.LIDT.Co.Commutativity.gCommStability_raw_le_half_of {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (zeta : ℝ) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) (hself : family.StronglySelfConsistent strategy.state zeta) {Outcome : Type u_3} [Fintype Outcome] (A B : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) Outcome (K →L[ℂ] K)) (point : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params → MIPStarRE.LDT.Point params.next) (hmarg : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => gCommOverlapTerm params strategy G (MIPStarRE.LDT.pointHeight params (point q))) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => gCommOverlapTerm params strategy G x) (hpointwise : ∀ (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params), strategy.state.qSDDOp (A q) (B q) ≤ gCommOverlapTerm params strategy G (MIPStarRE.LDT.pointHeight params (point q))) : strategy.state.sddErrorOp (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.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 MIPRE.LIDT.Co.Commutativity.gCommStability_raw_le_one_of {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) {Outcome : Type u_3} [Fintype Outcome] (A B : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) Outcome (K →L[ℂ] K)) (point : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params → MIPStarRE.LDT.Point params.next) (hpointwise : ∀ (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params), strategy.state.qSDDOp (A q) (B q) ≤ gCommOverlapTerm params strategy G (MIPStarRE.LDT.pointHeight params (point q))) : strategy.state.sddErrorOp (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) A B ≤ 1

Any pointwise defect bound by the common overlap term is trivially at most 1. The vendored lemma asks for a normalized state.

theorem MIPRE.LIDT.Co.Commutativity.sddOpRel_of_sqrt_bound_from_half_one {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxOpFamily Question Outcome (K →L[ℂ] K)) (zeta : ℝ) (hz_nonneg : 0 ≤ zeta) (hhalf : V.sddErrorOp 𝒟 A B ≤ zeta / 2) (hone : V.sddErrorOp 𝒟 A B ≤ 1) : V.SDDOpRel 𝒟 A B √zeta

Upgrade raw zeta / 2 and 1 bounds to the displayed sqrt zeta relation. The vendored one-space state ψ is a vector state V.

theorem MIPRE.LIDT.Co.Commutativity.gCommStability_overlap {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (zeta : ℝ) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) (hself : family.StronglySelfConsistent strategy.state zeta) : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.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. The vendored theorem asks for a normalized state.