Section 12 pasting: exact identities and error-bound lemma

Exact recurrence identities and the paper-total error absorption lemma that assemble the final fromHToG telescope conclusion.

structure MIPStarRE.LDT.Pasting.FromHToGAdjacentStageExactFacts {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) : Prop

Exact bookkeeping at the end of the adjacent-stage comparison.

This isolates the paper's S-recurrence step references/ldt-paper/ld-pasting.tex:1417--1425 and its use in the final collapse at lines 1657--1661: once the analytic move-right / commute / move-right approximations have reached the branch-split expression, the recurrence weight is exactly the next-stage weight.

• completeBranchAverage : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (completePartSubMeas params family x).total) = family.averagedSubMeas.total
• incompleteBranchAverage : (averageOperatorOverDistribution (uniformDistribution (Fq params)) fun (x : Fq params) => (incompletePartSubMeas params family x).total) = 1 - family.averagedSubMeas.total
• tailWeightRecurrence (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) : fromHToGTailStageMass params ψbi family (prefixLen + 1) τtail = ev ψbi (leftTensor (averagedSandwichByTypeSubMeas params family tailLen τtail).total * rightTensor (fromHToGRecurrenceWeight params family prefixLen (prependTypeBit true τtail) * family.averagedSubMeas.total + fromHToGRecurrenceWeight params family prefixLen (prependTypeBit false τtail) * (1 - family.averagedSubMeas.total)))

theorem MIPStarRE.LDT.Pasting.fromHToGAdjacentStageExactFacts_of_weights {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) : FromHToGAdjacentStageExactFacts params ψbi family

Collect the exact S-recurrence identities proved in Core/AveragesAndOps and Core/StageMass.

theorem MIPStarRE.LDT.Pasting.fromHToGPaperTotalError_le (params : Parameters) (gamma zeta : Error) (k : ℕ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le_one : zeta ≤ 1) : fromHToGPaperTotalError params gamma zeta k ≤ fromHToGError params gamma zeta k

The paper's scalar absorption line for lem:from-H-to-G.

Under the side conditions needed for the √(2ζ) term (γ, ζ ≥ 0 and ζ ≤ 1), the paper-total error from references/ldt-paper/ld-pasting.tex:1372--1375 is bounded by the displayed fromHToGError. The proof follows the paper arithmetic: bound √(2ζ) by 2 ζ^(1/32), bound √426 by 21, and use √(γ^(1/16)+ζ^(1/16)+(d/q)^(1/16)) ≤ γ^(1/32)+ζ^(1/32)+(d/q)^(1/32).