Section 11 commutativity: raw second scalar stability bound

The raw uncollapsed form of the second scalar stability estimate.

noncomputable def MIPStarRE.LDT.Commutativity.gCommStabilityTwoRawScalarDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (x : Fq params) : Error

Raw uncollapsed scalar defect for the paper's second G-commutativity stability estimate after the right-register point-product swap.

For fixed slice height x, this is the expression from commutativity-G.tex, clm:g-comm-stability2, before collapsing the (v,y), b-average into gCommStabilityTwoR. The left register contains G^x_g B^{v,y}_b (1-G^x), while the right register contains the swapped point product P^{v,y}_b P^{u,x}_{g(u)}.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Commutativity.gCommStabilityTwo_raw_scalar {ι : 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) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) : |avgOver (uniformDistribution (Fq params)) (gCommStabilityTwoRawScalarDefect params strategy family G)| ≤ √zeta

Raw paper form of the second scalar G-commutativity stability estimate.

This bounds the uncollapsed post-swap defect used in the paper line-87 removal: the defect still averages over (v,y), u, g, b rather than first packaging the left-register sandwich as gCommStabilityTwoR.