Section 11 commutativity: shared scalar stability helpers

Auxiliary positivity, order, and bounded-residual lemmas used by the scalar stability estimates.

theorem MIPStarRE.LDT.Commutativity.GCommStability.Scalar.averagedSlicePointEvaluationOperator_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (g : Polynomial params) : 0 ≤ IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

theorem MIPStarRE.LDT.Commutativity.GCommStability.Scalar.averagedSlicePointEvaluationOperator_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (g : Polynomial params) : IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g ≤ 1

theorem MIPStarRE.LDT.Commutativity.GCommStability.Scalar.averagedSlicePointEvaluationOperator_hermitian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (g : Polynomial params) : Matrix.conjTranspose (IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g) = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

theorem MIPStarRE.LDT.Commutativity.GCommStability.Scalar.averagedSlicePointEvaluationOperator_sq_le_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (x : Fq params) (g : Polynomial params) : IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g * IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g ≤ IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

theorem MIPStarRE.LDT.Commutativity.GCommStability.Scalar.storedResidual_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (zeta : Error) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (x : Fq params) : 0 ≤ hbound.storedResidual G x

theorem MIPStarRE.LDT.Commutativity.GCommStability.Scalar.scalar_pointwise_cauchy_schwarz_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (zeta : Error) (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) (R : SubMeas (Polynomial params) ι) (x : Fq params) (hfirstR : ∑ g : Polynomial params, ev strategy.state (leftTensor (R.outcome g)) ≤ 1) : |∑ g : Polynomial params, ev strategy.state (leftTensor (R.outcome g * (1 - (G x).total)) * rightTensor (IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g))| ≤ √(hbound.storedResidual G x)

Common pointwise Cauchy--Schwarz estimate for the scalar G-commutativity stability bounds.

The proof applies to either scalar stability estimate once the intermediate submeasurement R and its first Cauchy--Schwarz factor are supplied.