Section 11 commutativity: G-stability overlap (step two) #
Second overlap-averaging step for the G-stability argument: completes the
integral reduction begun in OverlapOne.
References #
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.gCommStabilityTwo_overlap
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(gamma 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))
(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.
Transport from evaluated to full-slice commutation #
This section converts the evaluated commutation estimate into the full-slice
commutation bound. It collects the postprocessing identities, question
reindexing lemmas, and large/small parameter case split used in the proof of
thm:com-main.