Section 12 — Definitions: consistency and families

Global-consistency predicates and the completed-slice family constructions.

def MIPStarRE.LDT.Pasting.IsGloballyConsistent (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) (gs : GHatTupleOutcome params k) : Prop

A completed-slice tuple gs is globally consistent at evaluation points xs if there exists a single polynomial h in m+1 variables whose restriction to each genuine slice height xᵢ agrees with the corresponding slice polynomial gᵢ.

This matches the paper's Global_τ(x) predicate from references/ldt-paper/ld-pasting.tex lines 1123-1131.

Equations

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

@[implicit_reducible]

noncomputable instance MIPStarRE.LDT.Pasting.isGloballyConsistent_decidablePred (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) : DecidablePred (IsGloballyConsistent params xs)

IsGloballyConsistent params xs is only classically decidable. The predicate quantifies over a witness polynomial in the ambient global polynomial space, so there is no finitary decision procedure to search for such a witness. This nonconstructive instance is used only for finite restrictSubMeas filters.

Equations

• MIPStarRE.LDT.Pasting.isGloballyConsistent_decidablePred params xs _gs = Classical.dec (MIPStarRE.LDT.Pasting.IsGloballyConsistent params xs _gs)

def MIPStarRE.LDT.Pasting.globallyConsistentOutcomesByType (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) (τ : GHatType k) : Set (GHatTupleOutcome params k)

The subset \mathsf{Global}_\tau(x) of \mathsf{Outcomes}_\tau consisting of tuples that arise from restrictions of a single global polynomial at the slice heights xs.

Equations

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

def MIPStarRE.LDT.Pasting.nonglobalOutcomesByType (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) (τ : GHatType k) : Set (GHatTupleOutcome params k)

The complement \overline{\mathsf{Global}_\tau(x)} inside \mathsf{Outcomes}_\tau.

Equations

• MIPStarRE.LDT.Pasting.nonglobalOutcomesByType params xs τ = MIPStarRE.LDT.Pasting.outcomesByType τ \ MIPStarRE.LDT.Pasting.globallyConsistentOutcomesByType params xs τ

noncomputable def MIPStarRE.LDT.Pasting.globallyConsistentWitness (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) (gs : GHatTupleOutcome params k) (hGlobal : IsGloballyConsistent params xs gs) : Polynomial params.next

Paper origin: references/ldt-paper/ld-pasting.tex:1131-1135 (definition of \mathsf{Global}_{\tau}(x)).

Choose a witness polynomial for a globally consistent tuple.

Equations

• MIPStarRE.LDT.Pasting.globallyConsistentWitness params xs gs hGlobal = Classical.choose hGlobal

noncomputable def MIPStarRE.LDT.Pasting.interpolateCompletedSlices (params : Parameters) [FieldModel params.q] (k : ℕ) : PointTuple params k → GHatTupleOutcome params k → Polynomial params.next

Recover a global polynomial from a completed-slice tuple.

On the actual pasting path this map is only applied after restricting to tuples in Global_τ(x) with |τ| ≥ d+1, so the ineligible branch lies outside the support of pastedInterpolationFamily. We nevertheless make the nonempty ineligible branch honest: for globally consistent tuples of length k + 1 that fail the eligibility cutoff, we return a chosen witness polynomial rather than a placeholder.

The empty-tuple branch keeps the distinguished fallback outcome h₀, matching the completion outcome used in constructedPastedMeasurement.

In the eligible branch we still keep the explicit interpolation support witness: a chosen subset σ ⊆ support(gs) of size d+1 is packaged together with its proof fields and then passed to interpolateCompletedSlicesFromSupport.

Equations

• One or more equations did not get rendered due to their size.
• MIPStarRE.LDT.Pasting.interpolateCompletedSlices params 0 _xs _gs = MIPStarRE.LDT.Pasting.fallbackInterpolatedPolynomial params

noncomputable def MIPStarRE.LDT.Pasting.completePartSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) : SubMeas Unit ι

Aggregate the polynomial outcomes of G^x into its complete part G^x.

Equations

• MIPStarRE.LDT.Pasting.completePartSubMeas params family x = MIPStarRE.LDT.postprocess (family.meas x).toSubMeas fun (x : MIPStarRE.LDT.Polynomial params) => ()

@[simp]

theorem MIPStarRE.LDT.Pasting.completePartSubMeas_total {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) : (completePartSubMeas params family x).total = (family.meas x).total

The total operator of the complete part is the original slice total.

@[simp]

theorem MIPStarRE.LDT.Pasting.completePartSubMeas_outcome_unit {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) : (completePartSubMeas params family x).outcome () = (completePartSubMeas params family x).total

The unique outcome of the complete part equals its total operator.

noncomputable def MIPStarRE.LDT.Pasting.incompletePartSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) : SubMeas Unit ι

Placeholder for the incomplete part G^x_⊥ = I - G^x.

Equations

• MIPStarRE.LDT.Pasting.incompletePartSubMeas params family x = MIPStarRE.LDT.SubMeas.singleOutcome (1 - (MIPStarRE.LDT.Pasting.completePartSubMeas params family x).total) ⋯ ⋯

noncomputable def MIPStarRE.LDT.Pasting.gHatIdxMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxMeas (Fq params) (GHatOutcome params) ι

Complete each projective slice submeasurement by adjoining the failure outcome.

Equations

• MIPStarRE.LDT.Pasting.gHatIdxMeas params family x = MIPStarRE.LDT.completeSubMeas (family.meas x).toSubMeas

theorem MIPStarRE.LDT.Pasting.gHatIdxMeas_proj {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) (g : GHatOutcome params) : (gHatIdxMeas params family x).outcome g * (gHatIdxMeas params family x).outcome g = (gHatIdxMeas params family x).outcome g

Each completed \widehat G outcome is projective.

noncomputable def MIPStarRE.LDT.Pasting.completePartLeftFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (SliceQuestion params) Unit (ι × ι)

Left tensor-placement for the complete part G^x on the bipartite space d * d.

Equations

• MIPStarRE.LDT.Pasting.completePartLeftFamily params family x = MIPStarRE.LDT.leftPlacedSubMeas (MIPStarRE.LDT.Pasting.completePartSubMeas params family x)

noncomputable def MIPStarRE.LDT.Pasting.completePartRightFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (SliceQuestion params) Unit (ι × ι)

Right tensor-placement for the complete part G^x on the bipartite space d * d.

Equations

• MIPStarRE.LDT.Pasting.completePartRightFamily params family x = MIPStarRE.LDT.rightPlacedSubMeas (MIPStarRE.LDT.Pasting.completePartSubMeas params family x)

noncomputable def MIPStarRE.LDT.Pasting.incompletePartLeftFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (SliceQuestion params) Unit (ι × ι)

Left tensor-placement for the incomplete part G^x_⊥ on the bipartite space d * d.

Equations

• MIPStarRE.LDT.Pasting.incompletePartLeftFamily params family x = MIPStarRE.LDT.leftPlacedSubMeas (MIPStarRE.LDT.Pasting.incompletePartSubMeas params family x)

noncomputable def MIPStarRE.LDT.Pasting.incompletePartRightFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxSubMeas (SliceQuestion params) Unit (ι × ι)

Right tensor-placement for the incomplete part G^x_⊥ on the bipartite space d * d.

Equations

• MIPStarRE.LDT.Pasting.incompletePartRightFamily params family x = MIPStarRE.LDT.rightPlacedSubMeas (MIPStarRE.LDT.Pasting.incompletePartSubMeas params family x)