Section 12 pasting: fourth-term chain helpers

The steps of the fourth-term chain in commutativitySwitcheroo: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooCompletion/FourthTermChain.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 the three closeness steps is dropped, normalization being a theorem of the model (section "Swap symmetry is a theorem"): callers pass params S family M zeta hselfG and params S family M chi hcomm.

The pointwise mixed identity is the commutation S.L_comm_R of the two placements, in place of the vendored pair of opTensor rewrites. The left-front comparison merges the placements by S.leftTensor_mul_leftTensor and absorbs the complete-part total by Preliminaries.projSubMeas_outcome_mul_total_eq_outcome. The last √χ step applies Preliminaries.closenessOfInnerProduct_right to the state S.toVecState, passed explicitly, with the contraction witness switcherooAggregateLeftFront_contraction S params family M q and the two pointwise normalizations of Co/Pasting/SwitcherooCompletion/Expansion.lean.

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

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

Pointwise identity rewriting the mixed scalar expression into right/left tensor order.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateMixedScalar_close_leftFrontScalar {𝔓 : 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) : |switcherooAggregateMixedScalar params S family M - switcherooAggregateLeftFrontScalar params S family M| ≤ √zeta

The mixed scalar expression is within √ζ of the left-front scalar expression.

theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateOnceCommutedScalar_point {𝔓 : 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) : ∑ g : MIPStarRE.LDT.Polynomial params, ∑ o : Outcome, S.ev (S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (family.meas q.1).outcome g * (M q.2).outcome o * (family.meas q.1).outcome g)) = ∑ go : MIPStarRE.LDT.Polynomial params × Outcome, S.ev (S.L ((completePartSubMeas params family q.1).total * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1 * (M q.2).outcome go.2 * (family.meas q.1).outcome go.1))

Sum-rewrite identity collapsing the product-type sum for the once-commuted scalar.

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

The once-commuted scalar expression is within √ζ of the mixed scalar expression.

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

The final sqrt chi comparison in the fourth-term chain: compare the left-front scalar expression with the split-by-g scalar that later collapses to the first positive switcheroo term.