Section 12 pasting: from-H-to-G paper telescope

Assembles the adjacent-stage paper move chain A → M₁ → M₂ → M₃ → E and records the final stage-mass telescope for the fromHToG reduction: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/FromHToG/PaperMoveChain/Telescope.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The vendored bipartite state ψbi : QuantumState (ι × ι) is the symmetric model S : SymModel 𝔓 K, in the vendored argument position; leftTensor/rightTensor are S.L/S.R, ᴴ is star, and the vendored weight operator, also named S, is W. The three lemmas take the normalization hypothesis hnorm : ψbi.IsNormalized, used only to feed closenessOfIP, closenessOfIPAdjoint and the two paper moves of Moves, whose ported forms drop it; it is dropped here as well (section "Port conventions"), so vendored callers pass strategy.state where they passed ψbi hnorm. No lemma has a swap or density hypothesis.

The two Cauchy--Schwarz context bounds (A → M₁ and M₁ → M₂) are proved with the keystone's placement positivity (S.opTensor_nonneg, S.opTensor_le_leftTensor, S.opTensor_mono_right) and the projectivity gHatIdxMeas_proj of the completed outcomes, in place of the vendored Kronecker and sq_le_self chains. They are the two private theorems fromHToGAdjacentStage_moveA0M1 and fromHToGAdjacentStage_moveM1M2, which the vendored proof of fromHToGAdjacentStage_paperMoveChain has inline: inline, that proof took 3.6 s, and split, each takes 1.6–2.3 s (load about 1; the vendored proof, 11.6 s).

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.fromHToGAdjacentStage_paperMoveChain {𝔓 : 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 𝔓) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hfacts : GHatFactsStatement params S family gamma zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params S family gamma zeta j) (hstageExact : FromHToGAdjacentStageExactFacts params S family) (k ℓ : ℕ) (hℓ : ℓ < k) : |fromHToGStageMass params S family k ℓ - fromHToGStageMass params S family k (ℓ + 1)| ≤ MIPStarRE.LDT.Pasting.fromHToGRecurrenceError params gamma zeta k

One adjacent fromHToG paper step.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_recurrenceStep_of_paperMoveChain {𝔓 : 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 𝔓) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hfacts : GHatFactsStatement params S family gamma zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params S family gamma zeta j) (hstageExact : FromHToGAdjacentStageExactFacts params S family) (k ℓ : ℕ) : ℓ < k → |fromHToGStageMass params S family k ℓ - fromHToGStageMass params S family k (ℓ + 1)| ≤ MIPStarRE.LDT.Pasting.fromHToGRecurrenceError params gamma zeta k

Adjacent-stage recurrence obtained by applying the paper move chain at every nonterminal stage.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_stageMassTelescope_of_paperMoveChain {𝔓 : 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 𝔓) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hfacts : GHatFactsStatement params S family gamma zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params S family gamma zeta j) (hstageExact : FromHToGAdjacentStageExactFacts params S family) (k : ℕ) : |fromHToGStageMass params S family k 0 - fromHToGStageMass params S family k k| ≤ MIPStarRE.LDT.Pasting.fromHToGPaperTotalError params gamma zeta k

The paper-total stage-mass telescope for fromHToG.

This follows the iteration in ld-pasting.tex:1354--1372: applying the adjacent-stage estimate over all k stages gives k copies of the per-stage error. Lean records that literal telescope before the final scalar bound fromHToGPaperTotalError_le absorbs it into fromHToGError.