Section 12 pasting: G-hat facts

Quadrant decompositions and GHat bookkeeping facts.

theorem MIPStarRE.LDT.Pasting.gHatFacts_ofSelfConsistencyAndCommutation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hgamma : gamma ≤ 1) (_hzeta_nonneg : 0 ≤ zeta) (hzeta : zeta ≤ 1) (hd_le_q : params.d ≤ params.q) (hselfComplete : GCompleteSelfConsistencyStatement params ψbi family zeta) (hselfIncomplete : GBotSelfConsistencyStatement params ψbi family zeta) (hcommComplete : CommutingWithGCompleteStatement params ψbi family gamma zeta) (hcommIncomplete : CommutingWithGIncompleteStatement params ψbi family gamma zeta) : GHatFactsStatement params ψbi family gamma zeta

Internal form of cor:G-hat-facts after applying lem:g-complete-self-consistency, cor:g-bot-self-consistency, cor:commuting-with-G-complete, and cor:commuting-with-G-incomplete.

Source: The proof in references/ldt-paper/ld-pasting.tex:817-862 uses these four preceding Section 12 results internally. The paper-facing theorem gHatFacts below derives them from the source hypotheses rather than exposing them as public hypotheses.

theorem MIPStarRE.LDT.Pasting.gHatFacts {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (eps delta gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hgamma : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta : zeta ≤ 1) (hd_le_q : 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) : GHatFactsStatement params strategy.state family gamma zeta

cor:G-hat-facts, source-facing form.

theorem MIPStarRE.LDT.Pasting.gHatFacts_ofComMainAndSelfConsistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hgamma : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta : zeta ≤ 1) (hd_le_q : params.d ≤ params.q) (hcom : Commutativity.ComMainConclusion params strategy family gamma zeta) (hself : family.StronglySelfConsistent strategy.state zeta) : GHatFactsStatement params strategy.state family gamma zeta

Internal form of cor:G-hat-facts after applying thm:com-main.

The construction of the \widehat G estimates needs the commutativity conclusion of Section 11 and the strong self-consistency of the slice family. The full good-strategy hypothesis is therefore not part of this passage; it is used only upstream when proving thm:com-main.