Section 12 pasting: switcheroo scalar expressions

Named scalar expressions for the switcheroo contraction chain: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooContraction/ScalarTerms.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; the slice family is an IdxPolyFamily params 𝔓 and the auxiliary family M an IdxProjSubMeas (Fq params) Outcome 𝔓. The vendored hypothesis hnorm : ψbi.IsNormalized of switcherooAggregateFourthTerm_close_once_commuted_scalar and switcherooAggregateFourthTerm_mixed_close_left_front_scalar is dropped, normalization being a theorem of the model (section "Swap symmetry is a theorem"): callers pass params S family M chi hcomm and params S family M zeta hselfG.

The first restatement is switcherooAggregateFourthTerm_split_close_once_commuted by definitional unfolding. The second applies Preliminaries.closenessOfInnerProduct_right to the state S.toVecState, passed explicitly; its adjoint form of the self-consistency bound comes from switcherooCompletePartSelfConsistency_pairBound by S.leftTensor_conjTranspose, S.rightTensor_conjTranspose and the self-adjointness of the slice outcomes, in place of the vendored Matrix.PosSemidef argument.

Not ported

Nothing: every declaration of the vendored file is ported here.

References

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

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

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateLeftFrontScalar {𝔓 : 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 𝔓) : ℝ

The post-second-√ζ left-front expression in the paper's cross-term chain.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateFirstSplitScalar {𝔓 : 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 𝔓) : ℝ

The split-by-g expression that collapses back to the first positive term.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateOnceCommutedScalar {𝔓 : 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 𝔓) : ℝ

The post-first-√χ scalar expression in the fourth-term chain.

Equations

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

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm_close_once_commuted_scalar {𝔓 : 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) : |switcherooAggregateFourthTerm params S family M - switcherooAggregateOnceCommutedScalar params S family M| ≤ √chi

Restate the first sqrt chi step using the named scalar expression.

noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateMixedScalar {𝔓 : 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 𝔓) : ℝ

The post-first-√ζ mixed tensor scalar expression in the fourth-term chain.

Equations

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

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFourthTerm_mixed_close_left_front_scalar {𝔓 : 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 𝔓) (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) => ∑ g : MIPStarRE.LDT.Polynomial params, ∑ o : Outcome, S.ev (S.L ((family.meas q.1).outcome g) * S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o))) - MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => ∑ g : MIPStarRE.LDT.Polynomial params, ∑ o : Outcome, S.ev (S.R ((family.meas q.1).outcome g) * S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o))| ≤ √zeta

Restate the second sqrt zeta step using the named left-front scalar expression.