Section 11 commutativity: shared scalar stability helpers

Auxiliary positivity, order, and bounded-residual lemmas used by the scalar stability estimates: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/GCommStability/Scalar/Common.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The averaged slice point operator E_u A^{u,x}_{g(u)} lives in the local C*-algebra 𝔓, and the Cauchy–Schwarz estimate scalar_pointwise_cauchy_schwarz_bound is stated with the placements strategy.state.L and strategy.state.R. averagedSlicePointEvaluationOperator_hermitian states star W = W for the vendored Wᴴ = W.

The proofs are shorter than the vendored ones. Self-adjointness through Matrix.PosSemidef is IsSelfAdjoint.of_nonneg, the Kronecker positivity of storedResidual_nonneg is the keystone's opTensor_nonneg, and the entrywise ᴴ and product computations of the Cauchy–Schwarz factors are the keystone's conjTranspose_opTensor, opTensor_mul and leftTensor_mul_leftTensor. The finite sum over outcomes collapses through opTensor_sum_left_univ and ev_sum.

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.GCommStability.Scalar.averagedSlicePointEvaluationOperator_nonneg {𝔓 : 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) (x : MIPStarRE.LDT.Fq params) (g : MIPStarRE.LDT.Polynomial params) : 0 ≤ IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

The averaged slice point operator E_u A^{u,x}_{g(u)} is positive.

theorem MIPRE.LIDT.Co.Commutativity.GCommStability.Scalar.averagedSlicePointEvaluationOperator_le_one {𝔓 : 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) (x : MIPStarRE.LDT.Fq params) (g : MIPStarRE.LDT.Polynomial params) : IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g ≤ 1

The averaged slice point operator E_u A^{u,x}_{g(u)} is at most 1.

theorem MIPRE.LIDT.Co.Commutativity.GCommStability.Scalar.averagedSlicePointEvaluationOperator_hermitian {𝔓 : 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) (x : MIPStarRE.LDT.Fq params) (g : MIPStarRE.LDT.Polynomial params) : star (IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g) = IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

The averaged slice point operator E_u A^{u,x}_{g(u)} is self-adjoint.

theorem MIPRE.LIDT.Co.Commutativity.GCommStability.Scalar.averagedSlicePointEvaluationOperator_sq_le_self {𝔓 : 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) (x : MIPStarRE.LDT.Fq params) (g : MIPStarRE.LDT.Polynomial params) : IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g * IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g ≤ IdxPolyFamily.averagedSlicePointEvaluationOperator strategy x g

The averaged slice point operator W = E_u A^{u,x}_{g(u)} satisfies W² ≤ W.

theorem MIPRE.LIDT.Co.Commutativity.GCommStability.Scalar.storedResidual_nonneg {𝔓 : 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) 𝔓) (zeta : ℝ) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (x : MIPStarRE.LDT.Fq params) : 0 ≤ hbound.storedResidual G x

The stored boundedness residual ⟨Ψ, (I - G^x) ⊗ Z^x Ψ⟩ is nonnegative.

theorem MIPRE.LIDT.Co.Commutativity.GCommStability.Scalar.scalar_pointwise_cauchy_schwarz_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) (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) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (R : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (x : MIPStarRE.LDT.Fq params) (hfirstR : ∑ g : MIPStarRE.LDT.Polynomial params, strategy.state.ev (strategy.state.L (R.outcome g)) ≤ 1) : |∑ g : MIPStarRE.LDT.Polynomial params, strategy.state.ev (strategy.state.L (R.outcome g * (1 - (G x).total)) * strategy.state.R (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.