Section 12 — Sandwich constructions: switcheroo families

Switcheroo, complete-part, and half-product operator families: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Sandwich/Switcheroo.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The slice family is an IdxPolyFamily params 𝔓 and the auxiliary family M an IdxProjSubMeas (Fq params) Outcome 𝔓, both in the local C*-algebra 𝔓 (the vendored Op ι). The 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, S.rightPlacedSubMeas and OpFamily.leftPlacedOpFamily S, so their outcomes are S.L (…) and S.R (…) by rfl; callers write switcherooPointProductLeft strategy.state params family M where the vendored text was switcherooPointProductLeft params family M. The half-product operators read no state and are local operators in 𝔓.

Not ported

• gHatTupleOutcomeConsEquiv': 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.switcherooSelfConsistencyLeft {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) : IdxSubMeas (MIPStarRE.LDT.Pasting.SliceQuestion params) Outcome (K →L[ℂ] K)

Left tensor-placement for the auxiliary family M^x_o.

Equations

• MIPRE.LIDT.Co.Pasting.switcherooSelfConsistencyLeft S params M x = S.leftPlacedSubMeas (M x).toSubMeas

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooSelfConsistencyRight {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) : IdxSubMeas (MIPStarRE.LDT.Pasting.SliceQuestion params) Outcome (K →L[ℂ] K)

Right tensor-placement for the auxiliary family M^x_o.

Equations

• MIPRE.LIDT.Co.Pasting.switcherooSelfConsistencyRight S params M x = S.rightPlacedSubMeas (M x).toSubMeas

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooPointProductLeft {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) (MIPStarRE.LDT.Polynomial params × Outcome) (K →L[ℂ] K)

Concrete hypothesis family for G^x_g M^y_o.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooPointProductRight {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) (MIPStarRE.LDT.Polynomial params × Outcome) (K →L[ℂ] K)

Concrete hypothesis family for M^y_o G^x_g on the Polynomial params × Outcome outcome type.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateLeft {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) Outcome (K →L[ℂ] K)

Concrete aggregate family for G^x M^y_o.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateRight {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) Outcome (K →L[ℂ] K)

Concrete aggregate family for M^y_o G^x.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.completePartPointProductLeft {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) (MIPStarRE.LDT.Polynomial params) (K →L[ℂ] K)

Concrete family for G^x_g G^y.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.completePartPointProductRight {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) (MIPStarRE.LDT.Polynomial params) (K →L[ℂ] K)

Concrete family for G^y G^x_g.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.completePartTotalProductLeft {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) Unit (K →L[ℂ] K)

Concrete family for G^x G^y.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.completePartTotalProductRight {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) Unit (K →L[ℂ] K)

Concrete family for G^y G^x.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.incompletePartPointProductLeft {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) (MIPStarRE.LDT.Polynomial params) (K →L[ℂ] K)

Concrete family for G^x_g G^y_⊥.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.incompletePartPointProductRight {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) (MIPStarRE.LDT.Polynomial params) (K →L[ℂ] K)

Concrete family for G^y_⊥ G^x_g.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.incompletePartTotalProductLeft {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) Unit (K →L[ℂ] K)

Concrete family for G^x_⊥ G^y_⊥.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.incompletePartTotalProductRight {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) Unit (K →L[ℂ] K)

Concrete family for G^y_⊥ G^x_⊥.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.gHatSelfConsistencyLeftFamily {𝔓 : 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) (MIPStarRE.LDT.Pasting.GHatOutcome params) (K →L[ℂ] K)

Left tensor-placement for \widehat G^x_g.

Equations

• MIPRE.LIDT.Co.Pasting.gHatSelfConsistencyLeftFamily S params family x = S.leftPlacedSubMeas (MIPRE.LIDT.Co.Pasting.gHatIdxMeas params family x).toSubMeas

noncomputable def MIPRE.LIDT.Co.Pasting.gHatSelfConsistencyRightFamily {𝔓 : 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) (MIPStarRE.LDT.Pasting.GHatOutcome params) (K →L[ℂ] K)

Right tensor-placement for \widehat G^x_g.

Equations

• MIPRE.LIDT.Co.Pasting.gHatSelfConsistencyRightFamily S params family x = S.rightPlacedSubMeas (MIPRE.LIDT.Co.Pasting.gHatIdxMeas params family x).toSubMeas

noncomputable def MIPRE.LIDT.Co.Pasting.gHatPairProductLeft {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) (MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatOutcome params) (K →L[ℂ] K)

Concrete family for the pairwise product \widehat G^x_g \widehat G^y_h.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.gHatPairProductRight {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) (MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatOutcome params) (K →L[ℂ] K)

Concrete family for the reversed pairwise product \widehat G^y_h \widehat G^x_g.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.gHatHalfProductOutcomeOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (k : ℕ) : MIPStarRE.LDT.PointTuple params k → MIPStarRE.LDT.Pasting.GHatTupleOutcome params k → 𝔓

The ordered half-product \widehat G^{x_1}_{g_1} \cdots \widehat G^{x_k}_{g_k}.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.Co.Pasting.gHatHalfProductOutcomeOperator params family 0 _xs _gs = 1

noncomputable def MIPRE.LIDT.Co.Pasting.gHatHalfProductTotalOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (k : ℕ) : MIPStarRE.LDT.PointTuple params k → 𝔓

The total half-product \sum_{g_1,\dots,g_k} \widehat G^{x_1}_{g_1} \cdots \widehat G^{x_k}_{g_k}.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.Co.Pasting.gHatHalfProductTotalOperator params family 0 _xs = 1

noncomputable def MIPRE.LIDT.Co.Pasting.gHatRotatedHalfProductOutcomeOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (k : ℕ) : MIPStarRE.LDT.PointTuple params k → MIPStarRE.LDT.Pasting.GHatTupleOutcome params k → 𝔓

The cyclically rotated half-product \widehat G^{x_2}_{g_2} \cdots \widehat G^{x_k}_{g_k} \widehat G^{x_1}_{g_1}.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.Co.Pasting.gHatRotatedHalfProductOutcomeOperator params family 0 _xs _gs = 1

noncomputable def MIPRE.LIDT.Co.Pasting.gHatRotatedHalfProductTotalOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (k : ℕ) : MIPStarRE.LDT.PointTuple params k → 𝔓

The total cyclically rotated half-product.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.Co.Pasting.gHatRotatedHalfProductTotalOperator params family 0 _xs = 1

theorem MIPRE.LIDT.Co.Pasting.gHatHalfProductTotalOperator_eq_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (k : ℕ) (xs : MIPStarRE.LDT.PointTuple params k) : gHatHalfProductTotalOperator params family k xs = 1

The total operator of the ordered half-product is always the identity.

theorem MIPRE.LIDT.Co.Pasting.gHatHalfProduct_sum_eq_total {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (k : ℕ) (xs : MIPStarRE.LDT.PointTuple params k) : ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params k, gHatHalfProductOutcomeOperator params family k xs gs = gHatHalfProductTotalOperator params family k xs

Summing the ordered half-product over all completed outcomes gives its total operator.