Section 12 pasting: switcheroo infrastructure

Initial switcheroo infrastructure and aggregate expansion helpers: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooSetup/Infrastructure.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The vendored second bipartite state ψbi : QuantumState (ι × ι) is the symmetric model S : SymModel 𝔓 K, in the vendored argument position, and the switcheroo families of Co/Pasting/Sandwich/Switcheroo.lean are called as X S params …. The slice family is an IdxPolyFamily params 𝔓 and the auxiliary family M an IdxProjSubMeas (Fq params) Outcome 𝔓. The two state-free lemmas on projective submeasurements are generic: projSubMeas_sandwich_sum_le_one holds in any star-ordered ring and projSubMeas_total_sq in any C*-algebra with its order, so they serve 𝔓 and K →L[ℂ] K alike.

switcherooAggregate_qSDDOp_expand computes the defect in the local algebra, from (L a - L b)^* (L a - L b) = L ((a - b)^* (a - b)), in place of the vendored expansion on the joint space.

Not ported

• avgOver_abs_le_avgOver_abs: classical, imported.

References

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

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

theorem MIPRE.LIDT.Co.Pasting.projSubMeas_sandwich_sum_le_one {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (A : ProjSubMeas Outcome R) (B : R) (hB : B ≤ 1) : ∑ a : Outcome, A.outcome a * B * A.outcome a ≤ 1

A projective sandwich family with middle operator bounded by 1 sums to at most 1.

theorem MIPRE.LIDT.Co.Pasting.projSubMeas_total_sq {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (P : ProjSubMeas Outcome R) : P.total * P.total = P.total

The total operator of a projective submeasurement is idempotent.

Switcheroo infrastructure

theorem MIPRE.LIDT.Co.Pasting.switcherooSelfConsistency_bip {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) (omega : ℝ) (hselfM : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (switcherooSelfConsistencyLeft S params M) (switcherooSelfConsistencyRight S params M) omega) : Preliminaries.BipartiteSDDRel S (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) M.toIdxSubMeas M.toIdxSubMeas omega

Convert the one-question switcheroo self-consistency input into the bipartite form used by switchSandwich.

theorem MIPRE.LIDT.Co.Pasting.switcherooCompletePartSelfConsistency_pairBound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) (hselfG : GCompleteSelfConsistencyStatement params S family zeta) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => S.qSDDCore (fun (g : MIPStarRE.LDT.Polynomial params) => S.L ((family.meas q.1).outcome g)) fun (g : MIPStarRE.LDT.Polynomial params) => S.R ((family.meas q.1).outcome g)) ≤ zeta

Lift slicewise complete-part self-consistency to the slice-pair distribution.

This states the G^x self-consistency input in the form used by the switcheroo tensor-bound steps.

theorem MIPRE.LIDT.Co.Pasting.switcherooPointProductCommutation_coreBound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) (chi : ℝ) (hcomm : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (switcherooPointProductLeft S params family M) (switcherooPointProductRight S params family M) chi) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => S.qSDDCore (fun (go : MIPStarRE.LDT.Polynomial params × Outcome) => (switcherooPointProductLeft S params family M q).outcome go) fun (go : MIPStarRE.LDT.Polynomial params × Outcome) => (switcherooPointProductRight S params family M q).outcome go) ≤ chi

Read the switcheroo point-product commutation hypothesis as an average qSDDCore bound.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregate_qSDDOp_expand {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) : S.qSDDOp (switcherooAggregateLeft S params family M q) (switcherooAggregateRight S params family M q) = ∑ o : Outcome, (S.ev (S.L ((M q.2).outcome o * (completePartSubMeas params family q.1).total * (M q.2).outcome o)) + S.ev (S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (completePartSubMeas params family q.1).total)) - S.ev (S.L ((M q.2).outcome o * (completePartSubMeas params family q.1).total * (M q.2).outcome o * (completePartSubMeas params family q.1).total)) - S.ev (S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (completePartSubMeas params family q.1).total * (M q.2).outcome o)))

Expand a single-question switcheroo qSDDOp term into its four scalar components.