Section 12 — Definitions: consistency and families

Global-consistency predicates and the completed-slice family constructions: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Defs/Families.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

A slice family is an IdxPolyFamily params 𝔓 (Co/Test/StrategyPolynomialFamilies.lean), with its projective submeasurements in the local C*-algebra 𝔓 (the vendored Op ι). Its complete part G^x, incomplete part G^x_⊥ = 1 - G^x and completion \widehat G^x are local submeasurements in 𝔓. The four placed families take the symmetric model S : SymModel 𝔓 K as their first explicit argument, in place of the vendored named carriers (ιA := ι), (ιB := ι), and place by S.leftPlacedSubMeas and S.rightPlacedSubMeas (Co/Basic/SubMeasurementFamilies.lean), so their outcomes are S.L (…) and S.R (…) by rfl.

The classical half of the vendored file (the global-consistency predicate Global_τ(x), its classical decidability, the global and nonglobal outcome sets, the choice of a global witness and the interpolation map interpolateCompletedSlices) is not ported: this file imports the vendored file, and the ported files of Pasting name those declarations through explicit open MIPStarRE.LDT.Pasting (…) lists. The vendored instance isGloballyConsistent_decidablePred comes with the import.

Not ported

• IsGloballyConsistent: classical, imported.
• isGloballyConsistent_decidablePred: classical, imported.
• globallyConsistentOutcomesByType: classical, imported.
• nonglobalOutcomesByType: classical, imported.
• globallyConsistentWitness: classical, imported.
• interpolateCompletedSlices: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/ld-pasting.tex

noncomputable def MIPRE.LIDT.Co.Pasting.completePartSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (x : MIPStarRE.LDT.Fq params) : SubMeas Unit 𝔓

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

Equations

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

@[simp]

theorem MIPRE.LIDT.Co.Pasting.completePartSubMeas_total {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (x : MIPStarRE.LDT.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 MIPRE.LIDT.Co.Pasting.completePartSubMeas_outcome_unit {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (x : MIPStarRE.LDT.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 MIPRE.LIDT.Co.Pasting.incompletePartSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (x : MIPStarRE.LDT.Fq params) : SubMeas Unit 𝔓

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

Equations

• MIPRE.LIDT.Co.Pasting.incompletePartSubMeas params family x = MIPRE.LIDT.Co.SubMeas.singleOutcome (1 - (MIPRE.LIDT.Co.Pasting.completePartSubMeas params family x).total) ⋯ ⋯

noncomputable def MIPRE.LIDT.Co.Pasting.gHatIdxMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxMeas (MIPStarRE.LDT.Fq params) (MIPStarRE.LDT.Pasting.GHatOutcome params) 𝔓

Complete each projective slice submeasurement by adjoining the failure outcome.

Equations

• MIPRE.LIDT.Co.Pasting.gHatIdxMeas params family x = MIPRE.LIDT.Co.completeSubMeas (family.meas x).toSubMeas

theorem MIPRE.LIDT.Co.Pasting.gHatIdxMeas_proj {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (x : MIPStarRE.LDT.Fq params) (g : MIPStarRE.LDT.Pasting.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 MIPRE.LIDT.Co.Pasting.completePartLeftFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxSubMeas (MIPStarRE.LDT.Pasting.SliceQuestion params) Unit (K →L[ℂ] K)

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

Equations

• MIPRE.LIDT.Co.Pasting.completePartLeftFamily S params family x = S.leftPlacedSubMeas (MIPRE.LIDT.Co.Pasting.completePartSubMeas params family x)

noncomputable def MIPRE.LIDT.Co.Pasting.completePartRightFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxSubMeas (MIPStarRE.LDT.Pasting.SliceQuestion params) Unit (K →L[ℂ] K)

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

Equations

• MIPRE.LIDT.Co.Pasting.completePartRightFamily S params family x = S.rightPlacedSubMeas (MIPRE.LIDT.Co.Pasting.completePartSubMeas params family x)

noncomputable def MIPRE.LIDT.Co.Pasting.incompletePartLeftFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxSubMeas (MIPStarRE.LDT.Pasting.SliceQuestion params) Unit (K →L[ℂ] K)

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

Equations

• MIPRE.LIDT.Co.Pasting.incompletePartLeftFamily S params family x = S.leftPlacedSubMeas (MIPRE.LIDT.Co.Pasting.incompletePartSubMeas params family x)

noncomputable def MIPRE.LIDT.Co.Pasting.incompletePartRightFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxSubMeas (MIPStarRE.LDT.Pasting.SliceQuestion params) Unit (K →L[ℂ] K)

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

Equations

• MIPRE.LIDT.Co.Pasting.incompletePartRightFamily S params family x = S.rightPlacedSubMeas (MIPRE.LIDT.Co.Pasting.incompletePartSubMeas params family x)