Section 12 pasting: from-H-to-G theorem

Derivation of lem:from-H-to-G, from the G-hat facts, the half-sandwich commutation theorem, and the telescoping Bernoulli-stage comparison: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Bernoulli/FromHToG.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The vendored second bipartite state ψbi : QuantumState (ι × ι) is the symmetric model S : SymModel 𝔓 K, in the vendored argument position, a strategy is a SymStrat params.next 𝔓 K and the slice family an IdxPolyFamily params 𝔓. The vendored fromHToG_ofGHatFactsAndHalfSandwich and fromHToG_ofGHatFacts take the normalization hypothesis hnorm : ψbi.IsNormalized only to pass it to fromHToG_stageMassTelescope_of_paperMoveChain, whose ported form drops it (section "Swap symmetry is a theorem"), so it is dropped here as well, and the vendored calls that passed strategy.state strategy.isNormalized pass strategy.state. No lemma of the file 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.fromHToG_ofGHatFactsAndHalfSandwich {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le_one : zeta ≤ 1) (hfacts : GHatFactsStatement params S family gamma zeta) (hhalf : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params S family gamma zeta j) (k : ℕ) : FromHToGStatement params strategy S family gamma zeta k

Internal form of lem:from-H-to-G after applying cor:G-hat-facts and lem:commute-g-half-sandwich.

Source: The proof in references/ldt-paper/ld-pasting.tex:1295-1670 uses the completed-measurement facts and the half-sandwich commutation theorem internally. The paper-facing theorem fromHToG below derives those inputs from the source hypotheses.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_ofGHatFacts {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le_one : zeta ≤ 1) (hfacts : GHatFactsStatement params S family gamma zeta) (k : ℕ) : FromHToGStatement params strategy S family gamma zeta k

Internal form of lem:from-H-to-G from cor:G-hat-facts.

The half-sandwich estimates are obtained from the same G-hat facts.

theorem MIPRE.LIDT.Co.Pasting.fromHToG_ofComMain {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hgamma_le : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le_one : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hself : family.StronglySelfConsistent strategy.state zeta) (hcom : Commutativity.ComMainConclusion params strategy family gamma zeta) (k : ℕ) : FromHToGStatement params strategy strategy.state family gamma zeta k

Internal form of lem:from-H-to-G from the Section 11 commutativity conclusion.

theorem MIPRE.LIDT.Co.Pasting.fromHToG {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (eps delta gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hgamma_le : gamma ≤ 1) (hzeta_le_one : zeta ≤ 1) (hdq_le : params.d ≤ params.q) (hgood : strategy.IsGood eps delta gamma) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) (k : ℕ) : FromHToGStatement params strategy strategy.state family gamma zeta k

lem:from-H-to-G, source-facing form at the strategy state.