Section 11 commutativity: second scalar stability bound

The mirrored scalar stability defect and its Cauchy--Schwarz boundedness proof: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/GCommStability/Scalar/Second.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The mirrored slice submeasurement gCommStabilityTwoR lives in the local C*-algebra 𝔓, and the scalar defect is stated with the placements strategy.state.L and strategy.state.R. The vendored hypothesis hnorm : strategy.state.IsNormalized of gCommStabilityTwo_scalar is dropped, as the port conventions drop hψ : ψ.IsNormalized: the first Cauchy–Schwarz factor is bounded by the keystone's SymModel.sum_ev_leftTensor_outcome_le_one, which takes no normalization hypothesis. Callers omit that argument, which stood between zeta and family.

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

noncomputable def MIPRE.LIDT.Co.Commutativity.gCommStabilityTwoR {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (x : MIPStarRE.LDT.Fq params) : SubMeas (MIPStarRE.LDT.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.

noncomputable def MIPRE.LIDT.Co.Commutativity.gCommStabilityTwoScalarDefect {𝔓 : 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) 𝔓) (x : MIPStarRE.LDT.Fq params) : ℝ

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.

theorem MIPRE.LIDT.Co.Commutativity.gCommStabilityTwo_scalar {𝔓 : 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) : |MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.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. The vendored theorem asks for a normalized state.