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

The two analytic moves in the adjacent-stage paper chain, M₂ → M₃ and M₃ → E: the Cauchy--Schwarz and collapse steps in ld-pasting.tex, immediately before the adjacent-stage recurrence is assembled. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/FromHToG/PaperMoveChain/Moves.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 renamed W. Both vendored moves take the normalization hypothesis hnorm : ψbi.IsNormalized, used only to feed fromHToG_closenessOfIP_avgContext and fromHToG_SUS_context_avg_le_one, 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.

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.fromHToGAdjacentStageM2M3_paperMove {𝔓 : 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) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params S family gamma zeta j) (hstageExact : FromHToGAdjacentStageExactFacts params S family) (k ℓ : ℕ) : |fromHToGAdjacentStageM2 params S family k ℓ - fromHToGAdjacentStageM3 params S family k ℓ| ≤ √(MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta k)

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

theorem MIPRE.LIDT.Co.Pasting.fromHToGAdjacentStageM3E_paperMove {𝔓 : 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 : ℝ) (hfacts : GHatFactsStatement params S family gamma zeta) (hstageExact : FromHToGAdjacentStageExactFacts params S family) (k ℓ : ℕ) : |fromHToGAdjacentStageM3 params S family k ℓ - fromHToGStageMass params S family k (ℓ + 1)| ≤ √(2 * zeta)

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