Section 11 commutativity: core definitions

Outcome and question abbreviations for the evaluated-slice, full-slice, and stability steps of the Section 11 commutativity argument.

References

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

@[reducible, inline]

abbrev MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion (params : Parameters) : Type

Evaluated-slice questions consist of the two sampled points in the next ambient space. Their height coordinates are later retained as a full-slice question.

Equations

• MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params = (MIPStarRE.LDT.Point params.next × MIPStarRE.LDT.Point params.next)

@[reducible, inline]

abbrev MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome (params : Parameters) : Type

Evaluated-slice outcomes are the two field values obtained after evaluating the selected slice polynomials at the sampled points.

Equations

• MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params = (MIPStarRE.LDT.Fq params × MIPStarRE.LDT.Fq params)

@[reducible, inline]

abbrev MIPStarRE.LDT.Commutativity.FullSliceQuestion (params : Parameters) : Type

Full-slice questions are the two height coordinates associated with an evaluated-slice sample.

Equations

• MIPStarRE.LDT.Commutativity.FullSliceQuestion params = (MIPStarRE.LDT.Fq params × MIPStarRE.LDT.Fq params)

@[reducible, inline]

abbrev MIPStarRE.LDT.Commutativity.FullSliceOutcome (params : Parameters) [FieldModel params.q] : Type u_2

Full-slice outcomes are the pair of slice polynomials measured at the two height coordinates of a full-slice question.

Equations

• MIPStarRE.LDT.Commutativity.FullSliceOutcome params = (MIPStarRE.LDT.Polynomial params × MIPStarRE.LDT.Polynomial params)

@[reducible, inline]

abbrev MIPStarRE.LDT.Commutativity.StabilityOneOutcome (params : Parameters) [FieldModel params.q] : Type u_2

Outcomes for the G^y stability step.

We keep the first coordinate evaluated at u, but retain the full second polynomial h because the right-register weight is √(G_h). Postprocessing that coordinate down to h(v) would sum over the whole fiber {h | h(v) = b} and introduce a spurious multiplicity.

Equations

• MIPStarRE.LDT.Commutativity.StabilityOneOutcome params = (MIPStarRE.LDT.Fq params × MIPStarRE.LDT.Polynomial params)

@[reducible, inline]

abbrev MIPStarRE.LDT.Commutativity.StabilityTwoOutcome (params : Parameters) [FieldModel params.q] : Type u_2

Outcomes for the G^x stability step.

We retain the full first polynomial g because the right-register weight is √(G_g), while the second coordinate is already evaluated at v. This keeps the .1/.2 usage aligned with the paper's G^x versus G^y roles.

Equations

• MIPStarRE.LDT.Commutativity.StabilityTwoOutcome params = (MIPStarRE.LDT.Polynomial params × MIPStarRE.LDT.Fq params)

noncomputable def MIPStarRE.LDT.Commutativity.leftOrderedProductOpFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : OpFamily (α × β) (ι × ι)

Ordered product placed on the left tensor factor of the bipartite space ι × ι.

Equations

• MIPStarRE.LDT.Commutativity.leftOrderedProductOpFamily A B = (MIPStarRE.LDT.CommutativityPoints.orderedProductOpFamily A B).leftPlacedOpFamily

noncomputable def MIPStarRE.LDT.Commutativity.appendRightTotalOpFamily {α : Type u_2} [Fintype α] {κ : Type u_3} [Fintype κ] [DecidableEq κ] (A : OpFamily α κ) (X : Quantum.Op κ) : OpFamily α κ

Append a total operator on the right of every outcome operator.

Equations

• MIPStarRE.LDT.Commutativity.appendRightTotalOpFamily A X = { outcome := fun (a : α) => A.outcome a * X, total := A.total * X }

noncomputable def MIPStarRE.LDT.Commutativity.sandwichByOuterSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : SubMeas (α × β) ι

Sandwiched product A_a B_b A_a.

Its total operator should be the sum-of-sandwiches ∑_a A_a (∑_b B_b) A_a whenever α is finitely enumerable.

Equations

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

def MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice (params : Parameters) (q : EvaluatedSliceQuestion params) : FullSliceQuestion params

The full-slice question underlying an evaluated-slice sample.

Equations

• MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q = (MIPStarRE.LDT.pointHeight params q.1, MIPStarRE.LDT.pointHeight params q.2)

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedPointFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (Point params.next) (Fq params) ι

The postprocessed family ((u,x) ↦ G^x_[g(u)=a]).

Equations

• MIPStarRE.LDT.Commutativity.evaluatedPointFamily params family = family.evaluatedAtNextPoint

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedPointFamilyLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (Point params.next) (Fq params) (ι × ι)

Left tensor-placement for the evaluated family G^x_[g(u)=a] on the bipartite space d * d.

Equations

• MIPStarRE.LDT.Commutativity.evaluatedPointFamilyLeft params family u = MIPStarRE.LDT.leftPlacedSubMeas (MIPStarRE.LDT.Commutativity.evaluatedPointFamily params family u)

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedPointFamilyRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (Point params.next) (Fq params) (ι × ι)

Right tensor-placement for the evaluated family G^x_[g(u)=a] on the bipartite space d * d.

Equations

• MIPStarRE.LDT.Commutativity.evaluatedPointFamilyRight params family u = MIPStarRE.LDT.rightPlacedSubMeas (MIPStarRE.LDT.Commutativity.evaluatedPointFamily params family u)

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSliceFirstFactor {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (EvaluatedSliceQuestion params) (Fq params) ι

The first evaluated factor G^x_[g(u)=a].

Equations

• MIPStarRE.LDT.Commutativity.evaluatedSliceFirstFactor params family q = MIPStarRE.LDT.Commutativity.evaluatedPointFamily params family q.1

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSliceSecondFactor {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (EvaluatedSliceQuestion params) (Fq params) ι

The second evaluated factor G^y_[h(v)=b].

Equations

• MIPStarRE.LDT.Commutativity.evaluatedSliceSecondFactor params family q = MIPStarRE.LDT.Commutativity.evaluatedPointFamily params family q.2

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

The ordered evaluated-slice product (G^x_[g(u)=a] G^y_[h(v)=b]) ⊗ I on the bipartite space d * d.

Equations

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

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

The reversed evaluated-slice product (G^y_[h(v)=b] G^x_[g(u)=a]) ⊗ I on the bipartite space d * d.

Equations

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

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

The sandwiched evaluated product G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a] on the single-register space d.

Equations

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

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

The sandwiched evaluated product (G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a]) ⊗ I on the bipartite space d * d.

Equations

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

def MIPStarRE.LDT.Commutativity.fullSliceFirstFactor {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (FullSliceQuestion params) (Polynomial params) ι

The first full slice measurement G^x.

Equations

• MIPStarRE.LDT.Commutativity.fullSliceFirstFactor params family q = (family.meas q.1).toSubMeas

def MIPStarRE.LDT.Commutativity.fullSliceSecondFactor {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (FullSliceQuestion params) (Polynomial params) ι

The second full slice measurement G^y.

Equations

• MIPStarRE.LDT.Commutativity.fullSliceSecondFactor params family q = (family.meas q.2).toSubMeas

noncomputable def MIPStarRE.LDT.Commutativity.fullSliceProductLeft {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (_strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) : IdxOpFamily (FullSliceQuestion params) (FullSliceOutcome params) (ι × ι)

The ordered full-slice product (G^x_g G^y_h) ⊗ I on the bipartite space d * d.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.fullSliceProductRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (_strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) : IdxOpFamily (FullSliceQuestion params) (FullSliceOutcome params) (ι × ι)

The reversed full-slice product (G^y_h G^x_g) ⊗ I on the bipartite space d * d.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.evaluateFullSliceOutcomeAtQuestion (params : Parameters) [FieldModel params.q] (q : EvaluatedSliceQuestion params) : FullSliceOutcome params → EvaluatedSliceOutcome params

Evaluate a pair of full-slice outcomes at the sampled points ((u,x),(v,y)).

Equations

• MIPStarRE.LDT.Commutativity.evaluateFullSliceOutcomeAtQuestion params q gh = (gh.1.toFun (MIPStarRE.LDT.truncatePoint params q.1), gh.2.toFun (MIPStarRE.LDT.truncatePoint params q.2))

noncomputable def MIPStarRE.LDT.Commutativity.evaluateStabilityOneOutcomeAtQuestion (params : Parameters) [FieldModel params.q] (q : EvaluatedSliceQuestion params) : StabilityOneOutcome params → EvaluatedSliceOutcome params

Evaluate a G^y-stability outcome at the sampled second point v.

Equations

• MIPStarRE.LDT.Commutativity.evaluateStabilityOneOutcomeAtQuestion params q ah = (ah.1, ah.2.toFun (MIPStarRE.LDT.truncatePoint params q.2))

noncomputable def MIPStarRE.LDT.Commutativity.evaluateStabilityTwoOutcomeAtQuestion (params : Parameters) [FieldModel params.q] (q : EvaluatedSliceQuestion params) : StabilityTwoOutcome params → EvaluatedSliceOutcome params

Evaluate a G^x-stability outcome at the sampled first point u.

The first coordinate stays as the full polynomial g until this final evaluation step, while the second coordinate is already the measured value b. This matches the one-vs-two indexing used in the paper's two stability steps.

Equations

• MIPStarRE.LDT.Commutativity.evaluateStabilityTwoOutcomeAtQuestion params q gb = (gb.1.toFun (MIPStarRE.LDT.truncatePoint params q.1), gb.2)