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

This file contains the two analytic moves in the adjacent-stage paper chain: M₂ → M₃ and M₃ → E. They are the Cauchy--Schwarz and collapse steps in ld-pasting.tex, immediately before the adjacent-stage recurrence is assembled.

theorem MIPStarRE.LDT.Pasting.fromHToGAdjacentStageM2M3_paperMove {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params ψbi family gamma zeta j) (hstageExact : FromHToGAdjacentStageExactFacts params ψbi family) (k ℓ : ℕ) : |fromHToGAdjacentStageM2 params ψbi family k ℓ - fromHToGAdjacentStageM3 params ψbi family k ℓ| ≤ √(commuteGHalfSandwichError params gamma zeta k)

The second half-sandwich commutation move M₂ → M₃ in the paper chain.

theorem MIPStarRE.LDT.Pasting.fromHToGAdjacentStageM3E_paperMove {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (hnorm : ψbi.IsNormalized) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hfacts : GHatFactsStatement params ψbi family gamma zeta) (hstageExact : FromHToGAdjacentStageExactFacts params ψbi family) (k ℓ : ℕ) : |fromHToGAdjacentStageM3 params ψbi family k ℓ - fromHToGStageMass params ψbi family k (ℓ + 1)| ≤ √(2 * zeta)

The final analytic/collapse move M₃ → E in the paper chain.