Section 12 pasting: from-H-to-G collapsed bounds

Collapses the paper endpoint M₄ to the next Lean stage and records the scalar bounds used by the final telescope: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/FromHToG/PaperBounds.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The slice family is an IdxPolyFamily params 𝔓, so the completed-slice outcomes, the half-products and the recurrence weights are local operators in 𝔓 (the vendored Op ι), and ᴴ is star. The vendored bipartite state ψbi : QuantumState (ι × ι) both places and evaluates, so it is the symmetric model S : SymModel 𝔓 K, in the vendored argument position; leftTensor/rightTensor are S.L/S.R, and the vendored qSDDCore ψbi is S.qSDDCore, the vector-state defect read through the parent VecState. No lemma here has a swap, density or normalization 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

noncomputable def MIPRE.LIDT.Co.Pasting.fromHToGAdjacentStageCollapsed {𝔓 : 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 𝔓) (k ℓ : ℕ) : ℝ

The branch-averaged recurrence expression that M₄ collapses to: for each tail type τ, the averaged sandwich total against the two recurrence weights times the branch averages G and 1 - G.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Co.Pasting.fromHToGAdjacentStageCollapsed_eq_stage_succ {𝔓 : 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 𝔓) (hstageExact : FromHToGAdjacentStageExactFacts params S family) (k ℓ : ℕ) : fromHToGAdjacentStageCollapsed params S family k ℓ = fromHToGStageMass params S family k (ℓ + 1)

The collapsed branch expression is exactly the next Lean stage.

theorem MIPRE.LIDT.Co.Pasting.fromHToGAdjacentStageM4_eq_collapsed {𝔓 : 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 𝔓) (hcomplete : (averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => (completePartSubMeas params family x).total) = family.averagedSubMeas.total) (hincomplete : (averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => (incompletePartSubMeas params family x).total) = 1 - family.averagedSubMeas.total) (k ℓ : ℕ) : fromHToGAdjacentStageM4 params S family k ℓ = fromHToGAdjacentStageCollapsed params S family k ℓ

M₄ collapses exactly to the branch-averaged recurrence expression.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_headTail_qSDDCore_bound {𝔓 : 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) {n k : ℕ} (hn : 2 ≤ n + 1) (hnk : n + 1 ≤ k) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params × MIPStarRE.LDT.PointTuple params n)) fun (q : MIPStarRE.LDT.Fq params × MIPStarRE.LDT.PointTuple params n) => S.qSDDCore (fun (ogs : MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatTupleOutcome params n) => S.L ((gHatIdxMeas params family q.1).outcome ogs.1 * gHatHalfProductOutcomeOperator params family n q.2 ogs.2)) fun (ogs : MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatTupleOutcome params n) => S.L (gHatHalfProductOutcomeOperator params family n q.2 ogs.2 * (gHatIdxMeas params family q.1).outcome ogs.1)) ≤ MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta k

Raw qSDDCore form of the half-sandwich commutation hypothesis after splitting a nonempty sandwich into its head and tail, with the error weakened to the ambient length k.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_selfConsistency_qSDDCore_bound {𝔓 : 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 𝔓) (zeta : ℝ) (hcompleted : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (gHatSelfConsistencyLeftFamily S params family) (gHatSelfConsistencyRightFamily S params family) (MIPStarRE.LDT.Pasting.gHatSelfConsistencyError zeta)) {n : ℕ} : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params × MIPStarRE.LDT.PointTuple params n)) fun (q : MIPStarRE.LDT.Fq params × MIPStarRE.LDT.PointTuple params n) => S.qSDDCore (fun (g : MIPStarRE.LDT.Pasting.GHatOutcome params) => S.L ((gHatIdxMeas params family q.1).outcome g)) fun (g : MIPStarRE.LDT.Pasting.GHatOutcome params) => S.R ((gHatIdxMeas params family q.1).outcome g)) ≤ 2 * zeta

The completed self-consistency estimate used in the first and final move-right steps, after adjoining an irrelevant uniform suffix-question register.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_headTail_adjoint_qSDDCore_bound {𝔓 : 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) {n k : ℕ} (hn : 2 ≤ n + 1) (hnk : n + 1 ≤ k) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params × MIPStarRE.LDT.PointTuple params n)) fun (q : MIPStarRE.LDT.Fq params × MIPStarRE.LDT.PointTuple params n) => S.qSDDCore (fun (ogs : MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatTupleOutcome params n) => S.L (star (gHatHalfProductOutcomeOperator params family n q.2 ogs.2) * (gHatIdxMeas params family q.1).outcome ogs.1)) fun (ogs : MIPStarRE.LDT.Pasting.GHatOutcome params × MIPStarRE.LDT.Pasting.GHatTupleOutcome params n) => S.L ((gHatIdxMeas params family q.1).outcome ogs.1 * star (gHatHalfProductOutcomeOperator params family n q.2 ogs.2))) ≤ MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta k

Adjoint-oriented raw qSDDCore form of the half-sandwich commutation hypothesis. This is the orientation used by the paper's Cauchy--Schwarz decompositions in eq:call-this-later and eq:call-again-later-part-dos.