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

Second overlap-averaging step for the G-stability argument: completes the integral reduction begun in OverlapOne. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/GCommStability/OverlapTwo.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The relation of gCommStabilityTwo_overlap is strategy.state.SDDOpRel, a vector-state relation on joint operators, and the placements are strategy.state.L and strategy.state.R. The vendored hypothesis hnorm : strategy.state.IsNormalized of gCommStabilityTwo_overlap is dropped, as the port conventions drop hψ : ψ.IsNormalized and as OverlapOne drops it from gCommStability_raw_le_one_of: a vector state has ev 1 = 1 (VecState.ev_one_of_isNormalized). Callers omit that argument, which stood between gamma zeta and family.

The proofs are shorter than the vendored ones. The vendored self-adjointness of G^x through Matrix.PosSemidef is IsSelfAdjoint.of_nonneg, the entrywise ᴴ computation of gCommStabilityTwo_pointwise_summand_bound is star_mul with the self-adjointness of the evaluated outcomes, and the vendored simpa through leftTensor_mul_rightTensor_eq_opTensor is the keystone's opTensor_mono_left, S.opTensor A B being S.L A * S.R B by definition.

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.gCommStabilityTwo_pointwise_sum_bound {𝔓 : 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) (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) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) : ∑ gb : MIPStarRE.LDT.Commutativity.StabilityTwoOutcome params, strategy.state.ev (strategy.state.L ((1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total) * (evaluatedPointFamily params family q.2).outcome gb.2 * (1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total)) * strategy.state.R ((G (MIPStarRE.LDT.pointHeight params q.1)).outcome gb.1)) ≤ gCommOverlapTerm params strategy G (MIPStarRE.LDT.pointHeight params q.1)

Summing the stability-two comparison family leaves only the overlap term for G^x.

theorem MIPRE.LIDT.Co.Commutativity.gCommStabilityTwo_pointwise_summand_bound {𝔓 : 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) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (gb : MIPStarRE.LDT.Commutativity.StabilityTwoOutcome params) : strategy.state.ev (strategy.state.L ((1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total) * (star ((CommutativityPoints.orderedProductOpFamily (evaluatedSliceFirstFactor params family q) (evaluatedSliceSecondFactor params family q)).outcome (gb.1.toFun (MIPStarRE.LDT.truncatePoint params q.1), gb.2)) * (CommutativityPoints.orderedProductOpFamily (evaluatedSliceFirstFactor params family q) (evaluatedSliceSecondFactor params family q)).outcome (gb.1.toFun (MIPStarRE.LDT.truncatePoint params q.1), gb.2)) * (1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total)) * strategy.state.R ((G (MIPStarRE.LDT.pointHeight params q.1)).outcome gb.1)) ≤ strategy.state.ev (strategy.state.L ((1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total) * (evaluatedPointFamily params family q.2).outcome gb.2 * (1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total)) * strategy.state.R ((G (MIPStarRE.LDT.pointHeight params q.1)).outcome gb.1))

A single stability-two summand is controlled by replacing the inner ordered product square by the corresponding evaluated point outcome.

theorem MIPRE.LIDT.Co.Commutativity.gCommStabilityTwo_pointwise_bound {𝔓 : 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) (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) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) : strategy.state.qSDDOp (commDataProcessedGStabilityTwoLeft params strategy family G q) (commDataProcessedGStabilityTwoRight params strategy family G q) ≤ strategy.state.ev (strategy.state.L (1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total) * strategy.state.R (G (MIPStarRE.LDT.pointHeight params q.1)).total)

The full stability-two defect is bounded by the overlap term for the target slice measurement G^x.

theorem MIPRE.LIDT.Co.Commutativity.gCommStabilityTwo_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) (gamma 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)) (commDataProcessedGStabilityTwoLeft params strategy family G) (commDataProcessedGStabilityTwoRight params strategy family G) (√zeta + 6 * √(gamma * ↑(params.m + 1)))

Overlap-only version of the second stability estimate.

This removes the trailing G^x in the current SDD package via slice SSC overlap. The paper's clm:g-comm-stability2 first transports the right-register point operators with commutativityPoints, then applies the boundedness witness Z^x; that scalar mechanism is not what this internal lemma proves. The vendored theorem asks for a normalized state.