Section 12 pasting: operator averages and projective submeasurement lemmas

Averages over uniform distributions, tensor placement identities, and projective submeasurement algebraic lemmas for the fromHToG reduction.

theorem MIPStarRE.LDT.Pasting.fromHToG_averageOperator_uniform_const_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (α : Type u_2) [Fintype α] [DecidableEq α] [Nonempty α] : (averageOperatorOverDistribution (uniformDistribution α) fun (x : α) => 1) = 1

theorem MIPStarRE.LDT.Pasting.fromHToG_completePart_average_total_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (completePartSubMeas params family x).total) = family.averagedSubMeas.total

The completed branch of \widehat G averages to the operator G used in the Bernoulli recurrence, matching references/ldt-paper/ld-pasting.tex:1408--1415 for the τ_ℓ = 1 case.

theorem MIPStarRE.LDT.Pasting.fromHToG_incompletePart_average_total_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (incompletePartSubMeas params family x).total) = 1 - family.averagedSubMeas.total

The incomplete branch of \widehat G averages to I - G, matching references/ldt-paper/ld-pasting.tex:1408--1415 for the τ_ℓ = 0 case.

theorem MIPStarRE.LDT.Pasting.fromHToG_emptyRestrictedSandwichTotal_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (xs : PointTuple params 0) (τ : GHatType 0) : (postprocess (restrictSubMeas (gHatSandwichFamily params family 0 xs) fun (gs : GHatTupleOutcome params 0) => gs ∈ outcomesByType τ) fun (x : GHatTupleOutcome params 0) => ()).total = 1

A zero-length type restriction of the sandwiched family has total identity. This isolates the tailLen = 0 collapse of outcomesByType, restrictSubMeas, and the empty half-sandwich product.

theorem MIPStarRE.LDT.Pasting.fromHToG_averagedSandwichByTypeSubMeas_zero_total_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (τ : GHatType 0) : (averagedSandwichByTypeSubMeas params family 0 τ).total = 1

The empty suffix sandwich has total identity.

theorem MIPStarRE.LDT.Pasting.fromHToG_leftTensor_mul_rightTensor_indicator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Quantum.Op ι) (p : Prop) [Decidable p] : leftTensor A * rightTensor (if p then 1 else 0) = leftTensor (if p then A else 0)

Tensor placement collapses to the left factor when the right recurrence weight is the stage-0 eligibility indicator.

theorem MIPStarRE.LDT.Pasting.fromHToG_rightTensor_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A B : Quantum.Op ι) : rightTensor (A + B) = rightTensor A + rightTensor B

Right tensor placement distributes over addition.

theorem MIPStarRE.LDT.Pasting.fromHToG_leftTensor_conjTranspose {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Quantum.Op ι) : Matrix.conjTranspose (leftTensor A) = leftTensor (Matrix.conjTranspose A)

Conjugate transpose commutes with left tensor placement.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatIdxMeas_sum_isSome_true {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) : ∑ g : GHatOutcome params with Option.isSome g = true, (gHatIdxMeas params family x).outcome g = (completePartSubMeas params family x).total

Summing completed outcomes with isSome = true gives the complete branch.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatIdxMeas_sum_isSome_false {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) : ∑ g : GHatOutcome params with Option.isSome g = false, (gHatIdxMeas params family x).outcome g = (incompletePartSubMeas params family x).total

Summing completed outcomes with isSome = false gives the incomplete branch.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatIdxMeas_sum_isSome_true_weight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) (S : Quantum.Op ι) : ∑ g : GHatOutcome params with Option.isSome g = true, S * (gHatIdxMeas params family x).outcome g * (gHatIdxMeas params family x).outcome g = S * (completePartSubMeas params family x).total

Weighted complete-branch sum after using completed-outcome projectivity.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatIdxMeas_sum_isSome_false_weight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) (S : Quantum.Op ι) : ∑ g : GHatOutcome params with Option.isSome g = false, S * (gHatIdxMeas params family x).outcome g * (gHatIdxMeas params family x).outcome g = S * (incompletePartSubMeas params family x).total

Weighted incomplete-branch sum after using completed-outcome projectivity.

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

Expectation-level weighted complete-branch sum.

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

Expectation-level weighted incomplete-branch sum.