Section 12 pasting: from-H-to-G S U S context-average bounds

Sandwich-sum identities and the S U S context-average bound used in the second half-sandwich and final move-right Cauchy--Schwarz steps: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/FromHToG/PaperBounds/SandwichContext.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The slice family is an IdxPolyFamily params 𝔓, so the completed-slice outcomes, the half-products and the recurrence weights are local operators in 𝔓 (the vendored Op ι), and ᴴ is star. The vendored bipartite state ψbi : QuantumState (ι × ι) both places and evaluates, so it is the symmetric model S : SymModel 𝔓 K, in the vendored argument position; leftTensor/rightTensor are S.L/S.R. The vendored weight operator, also named S (a let in fromHToG_SUS_context_avg_le_one, an explicit argument of the three sandwich-average lemmas), is renamed W. The vendored fromHToG_SUS_context_avg_le_one takes the normalization hypothesis hnorm : ψbi.IsNormalized, used only for ev 1 = 1; it is dropped here (S.ev_one_of_isNormalized holds for every model), so vendored callers pass strategy.state where they passed ψbi hnorm. No other lemma has a swap, density or normalization hypothesis.

Not ported

Every declaration of the vendored file has a counterpart here.

References

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

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

theorem MIPRE.LIDT.Co.Pasting.fromHToG_gHatSandwichFamily_total_eq_one {𝔓 : 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) : (gHatSandwichFamily params family n xs).total = 1

The total mass of the tail sandwich family is the identity.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_gHatSandwichFamily_sum_eq_one {𝔓 : 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, (gHatSandwichFamily params family n xs).outcome gs = 1

The tail sandwich outcomes sum to the identity.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_ev_sum_isSome_sandwich_weight {𝔓 : 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 𝔓) (x : MIPStarRE.LDT.Fq params) (b : Bool) (A W : 𝔓) : ∑ g : MIPStarRE.LDT.Pasting.GHatOutcome params with Option.isSome g = b, S.ev (S.L A * S.R (W * (gHatIdxMeas params family x).outcome g * W)) = S.ev (S.L A * S.R ((W * if b = true then (completePartSubMeas params family x).total else (incompletePartSubMeas params family x).total) * W))

Expectation-level branch sum with an S · U · S sandwich.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_avgOver_head_ev_sandwich {𝔓 : 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) (A W : 𝔓) (F : MIPStarRE.LDT.Fq params → 𝔓) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => S.ev (S.L A * S.R (W * F x * W))) = S.ev (S.L A * S.R (W * averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) F * W))

Fold a head-point scalar average with an S · F x · S sandwich into the right tensor factor.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_avgOver_head_branch_ev_sandwich {𝔓 : 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 𝔓) (hcomplete : (averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => (completePartSubMeas params family x).total) = family.averagedSubMeas.total) (hincomplete : (averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => (incompletePartSubMeas params family x).total) = 1 - family.averagedSubMeas.total) (b : Bool) (A W : 𝔓) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => have B := if b = true then (completePartSubMeas params family x).total else (incompletePartSubMeas params family x).total; S.ev (S.L A * S.R (W * B * W))) = S.ev (S.L A * S.R ((W * if b = true then family.averagedSubMeas.total else 1 - family.averagedSubMeas.total) * W))

Fold the complete/incomplete head branch average with an S · B · S sandwich into the stored exact branch averages.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_sum_averagedSandwichByType_total_eq_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (n : ℕ) : ∑ τ : MIPStarRE.LDT.Pasting.GHatType n, (averagedSandwichByTypeSubMeas params family n τ).total = 1

Summing the per-type averaged sandwich totals gives the full tail sandwich total, hence the identity.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_SUS_context_avg_le_one {𝔓 : 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 𝔓) (hcomplete : (averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => (completePartSubMeas params family x).total) = family.averagedSubMeas.total) (hincomplete : (averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => (incompletePartSubMeas params family x).total) = 1 - family.averagedSubMeas.total) (ℓ n : ℕ) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params × MIPStarRE.LDT.PointTuple params n)) fun (q : MIPStarRE.LDT.Fq params × MIPStarRE.LDT.PointTuple params n) => ∑ ogs : MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatTupleOutcome params n, have W := fromHToGRecurrenceWeight params family ℓ (MIPStarRE.LDT.Pasting.prependTypeBit (Option.isSome ogs.1) (MIPStarRE.LDT.Pasting.gHatTupleType ogs.2)); have U := (gHatIdxMeas params family q.1).outcome ogs.1; have T := gHatHalfProductOutcomeOperator params family n q.2 ogs.2; S.ev (S.L T * S.R (W * U) * star (S.L T * S.R (W * U)))) ≤ 1

Averaged first-root context bound for the S U S sandwich used in the second half-sandwich and final move-right Cauchy--Schwarz steps.