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.

References

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedFromFullSliceProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) : IdxOpFamily (EvaluatedSliceQuestion params) (EvaluatedSliceOutcome params) (ι × ι)

Postprocess the full-slice ordered product at sampled points. On the bipartite space d * d.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedFromFullSliceProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) : IdxOpFamily (EvaluatedSliceQuestion params) (EvaluatedSliceOutcome params) (ι × ι)

Postprocess the full-slice reversed product at sampled points. On the bipartite space d * d.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityOneLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) : IdxOpFamily (EvaluatedSliceQuestion params) (StabilityOneOutcome params) (ι × ι)

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. On the bipartite space d * d.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityOneRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) : IdxOpFamily (EvaluatedSliceQuestion params) (StabilityOneOutcome params) (ι × ι)

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. On the bipartite space d * d.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityTwoLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) : IdxOpFamily (EvaluatedSliceQuestion params) (StabilityTwoOutcome params) (ι × ι)

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. On the bipartite space d * d.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityTwoRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) : IdxOpFamily (EvaluatedSliceQuestion params) (StabilityTwoOutcome params) (ι × ι)

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. On the bipartite space d * d.

Equations

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

theorem MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityOneLeft_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (q : EvaluatedSliceQuestion params) (ah : StabilityOneOutcome params) : (commDataProcessedGStabilityOneLeft params strategy family G q).outcome ah = (leftPlacedSubMeas (evaluatedSliceSandwichRaw params strategy family q)).outcome (ah.1, ah.2.toFun (truncatePoint params q.2)) * leftTensor (fullSliceSecondFactor params family (fullSliceQuestionOfEvaluatedSlice params q)).total * rightTensor (CFC.sqrt ((G (pointHeight params q.2)).outcome ah.2))

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

theorem MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityOneRight_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (q : EvaluatedSliceQuestion params) (ah : StabilityOneOutcome params) : (commDataProcessedGStabilityOneRight params strategy family G q).outcome ah = leftTensor ((evaluatedSliceSandwichRaw params strategy family q).outcome (ah.1, ah.2.toFun (truncatePoint params q.2))) * rightTensor (CFC.sqrt ((G (pointHeight params q.2)).outcome ah.2))

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

theorem MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityTwoLeft_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (q : EvaluatedSliceQuestion params) (gb : StabilityTwoOutcome params) : (commDataProcessedGStabilityTwoLeft params strategy family G q).outcome gb = (evaluatedSliceProductLeft params strategy family q).outcome (gb.1.toFun (truncatePoint params q.1), gb.2) * leftTensor (fullSliceFirstFactor params family (fullSliceQuestionOfEvaluatedSlice params q)).total * rightTensor (CFC.sqrt ((G (pointHeight params q.1)).outcome gb.1))

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

theorem MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityTwoRight_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (q : EvaluatedSliceQuestion params) (gb : StabilityTwoOutcome params) : (commDataProcessedGStabilityTwoRight params strategy family G q).outcome gb = leftTensor ((CommutativityPoints.orderedProductOpFamily (evaluatedSliceFirstFactor params family q) (evaluatedSliceSecondFactor params family q)).outcome (gb.1.toFun (truncatePoint params q.1), gb.2)) * rightTensor (CFC.sqrt ((G (pointHeight params q.1)).outcome gb.1))

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