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.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatSandwichFamily_total_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (n : ℕ) (xs : PointTuple params n) : (gHatSandwichFamily params family n xs).total = 1

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

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatSandwichFamily_sum_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (n : ℕ) (xs : PointTuple params n) : ∑ gs : GHatTupleOutcome params n, (gHatSandwichFamily params family n xs).outcome gs = 1

The tail sandwich outcomes sum to the identity.

theorem MIPStarRE.LDT.Pasting.fromHToG_ev_sum_isSome_sandwich_weight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (x : Fq params) (b : Bool) (A S : Quantum.Op ι) : ∑ g : GHatOutcome params with Option.isSome g = b, ev ψbi (leftTensor A * rightTensor (S * (gHatIdxMeas params family x).outcome g * S)) = ev ψbi (leftTensor A * rightTensor ((S * if b = true then (completePartSubMeas params family x).total else (incompletePartSubMeas params family x).total) * S))

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

theorem MIPStarRE.LDT.Pasting.fromHToG_avgOver_head_ev_sandwich {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (A S : Quantum.Op ι) (F : Fq params → Quantum.Op ι) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => ev ψbi (leftTensor A * rightTensor (S * F x * S))) = ev ψbi (leftTensor A * rightTensor (S * averageOperatorOverDistribution (uniformDistribution (Fq params)) F * S))

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

theorem MIPStarRE.LDT.Pasting.fromHToG_avgOver_head_branch_ev_sandwich {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (hcomplete : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (completePartSubMeas params family x).total) = family.averagedSubMeas.total) (hincomplete : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (incompletePartSubMeas params family x).total) = 1 - family.averagedSubMeas.total) (b : Bool) (A S : Quantum.Op ι) : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => have B := if b = true then (completePartSubMeas params family x).total else (incompletePartSubMeas params family x).total; ev ψbi (leftTensor A * rightTensor (S * B * S))) = ev ψbi (leftTensor A * rightTensor ((S * if b = true then family.averagedSubMeas.total else 1 - family.averagedSubMeas.total) * S))

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

theorem MIPStarRE.LDT.Pasting.fromHToG_sum_averagedSandwichByType_total_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (n : ℕ) : ∑ τ : 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 MIPStarRE.LDT.Pasting.fromHToG_SUS_context_avg_le_one {ι : Type u_2} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (hcomplete : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (completePartSubMeas params family x).total) = family.averagedSubMeas.total) (hincomplete : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (incompletePartSubMeas params family x).total) = 1 - family.averagedSubMeas.total) (ℓ n : ℕ) : (avgOver (uniformDistribution (Fq params × PointTuple params n)) fun (q : Fq params × PointTuple params n) => ∑ ogs : GHatOutcome params × GHatTupleOutcome params n, have S := fromHToGRecurrenceWeight params family ℓ (prependTypeBit (Option.isSome ogs.1) (gHatTupleType ogs.2)); have U := (gHatIdxMeas params family q.1).outcome ogs.1; have T := gHatHalfProductOutcomeOperator params family n q.2 ogs.2; ev ψbi (leftTensor T * rightTensor (S * U) * (leftTensor T * rightTensor (S * U)).conjTranspose)) ≤ 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.