Section 12 pasting: commute G half-sandwich

The public statement of lem:commute-g-half-sandwich: the counterpart of the vendored file of the same path under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

commuteGHalfSandwich_ofGHatFacts params S family gamma zeta k hk hzeta_le hfacts takes the symmetric model S : SymModel 𝔓 K where the vendored ψbi was, and the source-facing commuteGHalfSandwich takes a SymStrat params.next 𝔓 K and concludes on strategy.state, as the ported gHatFacts does. Neither vendored lemma has a swap, density or normalization hypothesis, so both statements are the vendored ones with the state translated.

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
• blueprint/src/chapter/ch09_pasting.tex

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich_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] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (k : ℕ) (hk : 2 ≤ k) (hzeta_le : zeta ≤ 1) (hfacts : GHatFactsStatement params S family gamma zeta) : CommuteGHalfSandwichStatement params S family gamma zeta k

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

Source: The proof in references/ldt-paper/ld-pasting.tex:871-910 uses the completed-measurement self-consistency and commutation estimates from cor:G-hat-facts. The paper-facing theorem commuteGHalfSandwich below derives those estimates from the source hypotheses.

theorem MIPRE.LIDT.Co.Pasting.commuteGHalfSandwich {𝔓 : 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) (hgamma_le : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le : 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 : ℕ) (hk : 2 ≤ k) : CommuteGHalfSandwichStatement params strategy.state family gamma zeta k

lem:commute-g-half-sandwich, source-facing form.