Section 11 commutativity: stability definitions

Reindexing and postprocessing infrastructure used in the full-slice and stability reductions, including the weighted reindex of raw operator families: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Defs/Stability.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The stability families are joint operator families of a symmetric strategy strategy : SymStrat params.next 𝔓 K: the vendored placements leftTensor (ι₂ := ι) and rightTensor (ι₁ := ι) are strategy.state.L and strategy.state.R, so each outcome lemma holds by rfl, as in the vendored file. weightedReindexOpFamily is generic over any type with an addition and a multiplication. The weights CFC.sqrt G_h are taken in the local C*-algebra 𝔓 before placement.

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.weightedReindexOpFamily {α : Type u_1} {β : Type u_2} [Fintype β] {R : Type u_3} [AddCommMonoid R] [Mul R] (base : OpFamily α R) (reindex : β → α) (weight : β → R) : OpFamily β R

Reindex a raw operator family and append an explicit weight.

The outcome type β must retain every coordinate that still appears in weight; otherwise any later postprocessing would sum over an irrelevant fiber and change the operator by a multiplicity factor.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedFromFullSliceProductLeft {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) (K →L[ℂ] K)

Postprocess the full-slice ordered product at sampled points.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedFromFullSliceProductRight {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) (K →L[ℂ] K)

Postprocess the full-slice reversed product at sampled points.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityOneLeft {𝔓 : 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) 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Commutativity.StabilityOneOutcome params) (K →L[ℂ] K)

Internal overlap family from the G^y insertion/removal step.

The paper writes the extra factor as the left-register total G^y = ∑_h G^y_h. For the SDDOpRel packaging we keep the polynomial h explicit and attach the right-register weight (G_h^y)^{1/2} to each outcome. Summing the squared differences over h then recovers the total G^y without introducing a fiber multiplicity from unrelated g values.

This is deliberately an overlap estimate family, not the scalar clm:g-comm-stability expression from the paper. The paper claim keeps the right-register factor A_b^{v,y} and is driven by the boundedness witness Z^y; the overlap family below instead measures a stronger-looking SDD package against G_h^y weights.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityOneRight {𝔓 : 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) 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Commutativity.StabilityOneOutcome params) (K →L[ℂ] K)

Internal overlap family after removing the trailing G^y, while keeping the G_h^y right-register square-root weight used by the SDD package.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityTwoLeft {𝔓 : 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) 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Commutativity.StabilityTwoOutcome params) (K →L[ℂ] K)

Internal overlap family from the G^x insertion/removal step.

As for commDataProcessedGStabilityOneLeft, this packages an overlap-style SDD comparison. The paper's clm:g-comm-stability2 is a scalar boundedness argument with right-register factor A_a^{u,x} A_b^{v,y} and an internal commutativityPoints transport step.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityTwoRight {𝔓 : 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) 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Commutativity.StabilityTwoOutcome params) (K →L[ℂ] K)

Internal overlap family after removing the trailing G^x, while keeping the G_g^x right-register square-root weight used by the SDD package.

Equations

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

theorem MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityOneLeft_outcome {𝔓 : 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) 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (ah : MIPStarRE.LDT.Commutativity.StabilityOneOutcome params) : (commDataProcessedGStabilityOneLeft params strategy family G q).outcome ah = (strategy.state.leftPlacedSubMeas (evaluatedSliceSandwichRaw params strategy family q)).outcome (ah.1, ah.2.toFun (MIPStarRE.LDT.truncatePoint params q.2)) * strategy.state.L (fullSliceSecondFactor params family (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)).total * strategy.state.R (CFC.sqrt ((G (MIPStarRE.LDT.pointHeight params q.2)).outcome ah.2))

Expand one outcome of the first G^y stability family.

theorem MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityOneRight_outcome {𝔓 : 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) 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (ah : MIPStarRE.LDT.Commutativity.StabilityOneOutcome params) : (commDataProcessedGStabilityOneRight params strategy family G q).outcome ah = strategy.state.L ((evaluatedSliceSandwichRaw params strategy family q).outcome (ah.1, ah.2.toFun (MIPStarRE.LDT.truncatePoint params q.2))) * strategy.state.R (CFC.sqrt ((G (MIPStarRE.LDT.pointHeight params q.2)).outcome ah.2))

Expand one outcome of the second G^y stability family.

theorem MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityTwoLeft_outcome {𝔓 : 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) 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (gb : MIPStarRE.LDT.Commutativity.StabilityTwoOutcome params) : (commDataProcessedGStabilityTwoLeft params strategy family G q).outcome gb = (evaluatedSliceProductLeft params strategy family q).outcome (gb.1.toFun (MIPStarRE.LDT.truncatePoint params q.1), gb.2) * strategy.state.L (fullSliceFirstFactor params family (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)).total * strategy.state.R (CFC.sqrt ((G (MIPStarRE.LDT.pointHeight params q.1)).outcome gb.1))

Expand one outcome of the first G^x stability family.

theorem MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityTwoRight_outcome {𝔓 : 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) 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (gb : MIPStarRE.LDT.Commutativity.StabilityTwoOutcome params) : (commDataProcessedGStabilityTwoRight params strategy family G q).outcome gb = strategy.state.L ((CommutativityPoints.orderedProductOpFamily (evaluatedSliceFirstFactor params family q) (evaluatedSliceSecondFactor params family q)).outcome (gb.1.toFun (MIPStarRE.LDT.truncatePoint params q.1), gb.2)) * strategy.state.R (CFC.sqrt ((G (MIPStarRE.LDT.pointHeight params q.1)).outcome gb.1))

Expand one outcome of the second G^x stability family.