Section 12 pasting: commute G half-sandwich setup — sum bounds

Sum-of-adjoint-products ≤ 1 bounds for the half-product, reverse-half-product, pair-prefix and bipartite placed families: the counterpart of the vendored file of the same path under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The half-product, reverse-half-product and pair-prefix bounds read no state: they are inequalities in the local C*-algebra 𝔓 (the vendored Op ι). The bipartite bound leftTensor_rightTensor_sum_adjoint_mul_le_one is about the placements S.L and S.R, so it takes the symmetric model S : SymModel 𝔓 K as an explicit first argument, in place of the vendored named carriers (ι₁ := ι), (ι₂ := ι); callers write leftTensor_rightTensor_sum_adjoint_mul_le_one strategy.state prefixOp tailOp hprefix htail. No vendored lemma here has a swap, density or normalization hypothesis.

The vendored half-product and pair-prefix proofs expand ∑_g (G_g T)^* (G_g T) in a calc each; here the private sum_star_gHat_mul_mul_self (∑_g (Ĝ^x_g b)^* (Ĝ^x_g b) = b^* b, the outcomes being projections summing to 1) serves both, and the pair-prefix bound is proved from it directly rather than through the length-two half-product and its reindexing. The bipartite bound is a sum of S.opTensor (p^* p) (t^* t) (S.conjTranspose_opTensor, S.opTensor_mul) bounded by S.opTensor_le_leftTensor, without the vendored Kronecker identities.

Not ported

• rpow_oneSixteenth_nonneg: classical, imported.
• commuteGHalfSandwich_error_bound: classical, imported.

References

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

• references/ldt-paper/ld-pasting.tex
• blueprint/src/chapter/ch09_pasting.tex

Half-product sum bounds

theorem MIPRE.LIDT.Co.Pasting.gHatHalfProduct_sum_adjoint_mul_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (r : ℕ) (xs : MIPStarRE.LDT.PointTuple params r) : ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params r, star (gHatHalfProductOutcomeOperator params family r xs gs) * gHatHalfProductOutcomeOperator params family r xs gs ≤ 1

The ordered half-products of completed-slice outcomes satisfy ∑_gs T_gs^* T_gs ≤ 1.

theorem MIPRE.LIDT.Co.Pasting.gHatReverseHalfProduct_sum_adjoint_mul_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (r : ℕ) (xs : MIPStarRE.LDT.PointTuple params r) : ∑ gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params r, star (gHatReverseHalfProductOutcomeOperator params family r xs gs) * gHatReverseHalfProductOutcomeOperator params family r xs gs ≤ 1

The reverse-ordered half-products of completed-slice outcomes satisfy ∑_gs T_gs^* T_gs ≤ 1.

Pair-prefix and bipartite tensor bounds

theorem MIPRE.LIDT.Co.Pasting.gHatPairPrefix_sum_adjoint_mul_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) : ∑ og : MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatOutcome params, star ((gHatIdxMeas params family q.1).outcome og.1 * (gHatIdxMeas params family q.2).outcome og.2) * ((gHatIdxMeas params family q.1).outcome og.1 * (gHatIdxMeas params family q.2).outcome og.2) ≤ 1

The products Ĝ^x_g Ĝ^y_h of two completed slices satisfy ∑_{g,h} (Ĝ^x_g Ĝ^y_h)^* (Ĝ^x_g Ĝ^y_h) ≤ 1, with equality.

theorem MIPRE.LIDT.Co.Pasting.leftTensor_rightTensor_sum_adjoint_mul_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (prefixOp : α → 𝔓) (tailOp : β → 𝔓) (hprefix : ∑ a : α, star (prefixOp a) * prefixOp a ≤ 1) (htail : ∑ b : β, star (tailOp b) * tailOp b ≤ 1) : ∑ ag : α × β, star (S.L (prefixOp ag.1) * S.R (tailOp ag.2)) * (S.L (prefixOp ag.1) * S.R (tailOp ag.2)) ≤ 1

Generic tensor-contraction bound: if prefixOp : α → 𝔓 and tailOp : β → 𝔓 each satisfy ∑ (·)^* (·) ≤ 1, then the joint family S.L (prefixOp a) * S.R (tailOp b) on α × β also satisfies ∑ (·)^* (·) ≤ 1.