Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Commutativity.GCommStability.Scalar.Second

Section 11 commutativity: second scalar stability bound #

The mirrored scalar stability defect and its Cauchy--Schwarz boundedness proof.

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

The paper's mirrored slice submeasurement R'^x_g = E_{v,y} \sum_b G^{v,y}_b G^x_g G^{v,y}_b.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPStarRE.LDT.Commutativity.gCommStabilityTwoScalarDefect {ι : 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

    Named scalar defect for the boundedness half of the second paper stability claim.

    For fixed x, this is the post-transport mirror analogue of commutativity-G.tex, equation eq:bound-this-right-now!, with the slice sandwich R'^x_g in place of R^y_g. It is the scalar after the commutativityPoints transport and after collapsing the b-indexed left-register sandwich into R'^x_g; it is not literally the uncollapsed paper expression eq:g-comm-stab7. Concretely, gCommStabilityTwoR averages the left-register sandwich E_{v,y} \sum_b G_b^{v,y} G_g^x G_b^{v,y}, the factor (1 - (G x).total) is the paper's left-register (I-G^x), and IdxPolyFamily.averagedSlicePointEvaluationOperator is the right-register average E_u A^{u,x}_{g(u)}. Thus each summand has tensor placement (R'_g{}^x (I-G^x)) ⊗ E_u A^{u,x}_{g(u)}. The 6√(γ(m+1)) transport loss is a separate estimate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPStarRE.LDT.Commutativity.gCommStabilityTwo_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)) (gCommStabilityTwoScalarDefect params strategy family G)| ≤ √zeta

      Direct boundedness proof for the second paper scalar stability estimate.

      This is the Z^x boundedness half of references/ldt-paper/commutativity-G.tex, clm:g-comm-stability2 (lines 185--221), after the right-register point-commutation transport and after the b-indexed left-register sandwich is collapsed into gCommStabilityTwoScalarDefect. It bounds the post-transport mirror scalar by √ζ. The separate 6√(γ(m+1)) transport loss is not proved here; a full paper-budget theorem must combine this post-transport bound with the distinct commutativityPoints transport estimate.