Section 12 pasting: from-H-to-G move lemmas

Tensor, positivity, and Cauchy--Schwarz helper lemmas for the adjacent paper chain: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/FromHToG/MoveLemmas/Basic.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The slice family is an IdxPolyFamily params 𝔓, so the completed slices, the half-products and the recurrence weights are local operators in 𝔓 (the vendored Op ι), and ᴴ is star. The sandwich domination psd_contraction_comm_sandwich_le reads no state and holds in any C⋆-algebra with its order. The two state lemmas whose vendored state only evaluates, fromHToG_qSDDCore_symm (vendored ψ : QuantumState ι, applied to the joint state) and fromHToG_closenessOfIP_avgContext (vendored ψ : QuantumState (ι × ι)), take a vector state V : VecState K with joint operators K →L[ℂ] K, to which callers pass strategy.state; the placement lemma fromHToG_ev_leftTensor_rightTensor_mono_right_of_nonneg_left takes the symmetric model S : SymModel 𝔓 K, in the vendored argument position. fromHToG_closenessOfIP_avgContext drops the unused normalization hypothesis _hψ : ψ.IsNormalized (section "Port conventions"), so its vendored callers' ψbi hnorm becomes strategy.state.

Not ported

• abs_sub_le_four: classical, imported.
• commuteGHalfSandwichError_mono_length: classical, imported.
• fromHToGPointTupleReverseEquiv: classical, imported.
• fromHToGGHatTupleOutcomeReverseEquiv: classical, imported.
• fromHToG_pointTupleTail_snoc: classical, imported.
• fromHToG_gHatTupleOutcomeTail_snoc: classical, imported.
• fromHToG_sum_product: classical, imported.
• fromHToG_avgOver_sub: classical, imported.
• fromHToG_type_filtered_outcome_sum: classical, imported.
• fromHToG_bool_type_filtered_outcome_sum: classical, imported.
• fromHToG_sum₂_avgOver₂: classical, imported.

References

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

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

theorem MIPRE.LIDT.Co.Pasting.fromHToG_qSDDCore_symm {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (V : VecState K) (A B : Outcome → K →L[ℂ] K) : V.qSDDCore A B = V.qSDDCore B A

Symmetry of the raw pointwise state-dependent distance core. This local form is useful when orienting adjoint half-sandwich commutators for the second paper commutation step.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_ev_leftTensor_rightTensor_mono_right_of_nonneg_left {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {A B C : 𝔓} (hA : 0 ≤ A) (hBC : B ≤ C) : S.ev (S.L A * S.R B) ≤ S.ev (S.L A * S.R C)

If A is PSD and B ≤ C, then the corresponding bipartite scalar expectations with left/right tensor placement are monotone in the right factor.

theorem MIPRE.LIDT.Co.Pasting.psd_contraction_comm_sandwich_le {𝔄 : Type u_3} [CStarAlgebra 𝔄] [PartialOrder 𝔄] [StarOrderedRing 𝔄] {S B : 𝔄} (hS0 : 0 ≤ S) (hS1 : S ≤ 1) (hB0 : 0 ≤ B) (hSB : Commute S B) : S * B * S ≤ B

If S is a PSD contraction commuting with B, then S * B * S ≤ B. This formalizes the paper's eq:S-sandwich domination step without using explicit square roots.

theorem MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight_sandwich_base_le {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) : have S := fromHToGRecurrenceWeight params family prefixLen τtail; S * family.averagedSubMeas.total * S ≤ family.averagedSubMeas.total

Paper eq:S-sandwich for the complete branch average G.

theorem MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight_sandwich_one_sub_base_le {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) : have S := fromHToGRecurrenceWeight params family prefixLen τtail; S * (1 - family.averagedSubMeas.total) * S ≤ 1 - family.averagedSubMeas.total

Paper eq:S-sandwich for the incomplete branch average I - G.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_gHatIdxMeas_outcome_isHermitian {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (x : MIPStarRE.LDT.Fq params) (g : MIPStarRE.LDT.Pasting.GHatOutcome params) : star ((gHatIdxMeas params family x).outcome g) = (gHatIdxMeas params family x).outcome g

Completed ĝ measurement outcomes are self-adjoint. This records the positivity-to-self-adjointness conversion used when orienting the adjoint half-sandwich commutator in the M₂ → M₃ move.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_gHatReverseHalfProductOutcomeOperator_eq_adjoint {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (n : ℕ) (xs : MIPStarRE.LDT.PointTuple params n) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params n) : gHatReverseHalfProductOutcomeOperator params family n xs gs = star (gHatHalfProductOutcomeOperator params family n xs gs)

The reverse half-product is the adjoint of the ordered half-product.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_gHatHalfProductOutcomeOperator_snoc {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (n : ℕ) (xs : MIPStarRE.LDT.PointTuple params n) (x : MIPStarRE.LDT.Fq params) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params n) (g : MIPStarRE.LDT.Pasting.GHatOutcome params) : gHatHalfProductOutcomeOperator params family (n + 1) (Fin.snoc xs x) (Fin.snoc gs g) = gHatHalfProductOutcomeOperator params family n xs gs * (gHatIdxMeas params family x).outcome g

Ordered half-products satisfy a snoc recursion.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_gHatHalfProduct_reverse_eq_adjoint {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (n : ℕ) (xs : MIPStarRE.LDT.PointTuple params n) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params n) : gHatHalfProductOutcomeOperator params family n ((MIPStarRE.LDT.Pasting.fromHToGPointTupleReverseEquiv params n) xs) ((MIPStarRE.LDT.Pasting.fromHToGGHatTupleOutcomeReverseEquiv params n) gs) = star (gHatHalfProductOutcomeOperator params family n xs gs)

Reversing a tuple turns the ordered half-product into its adjoint.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_closenessOfIP_avgContext {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {OutcomeA : Type u_4} {OutcomeB : Type u_5} [Fintype OutcomeA] [Fintype OutcomeB] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (_h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → K →L[ℂ] K) (C : Question → OutcomeA → OutcomeB → K →L[ℂ] K) (γ : ℝ) (hAB : (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => V.qSDDCore (A q) (B q)) ≤ γ) (hC : (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, V.ev ((∑ b : OutcomeB, C q a b) * star (∑ b : OutcomeB, C q a b))) ≤ 1) : |(MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.ev (C q a b * A q a)) - MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.ev (C q a b * B q a)| ≤ √γ

Averaged-context variant of closenessOfIP: the contraction side condition is only required after averaging over the question distribution.