Section 12 pasting: commuting-with-G complete part #
Complete-part commuting-with-G bounds.
theorem
MIPStarRE.LDT.Pasting.commutingWithGComplete_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 : GCompleteSelfConsistencyStatement params strategy.state family zeta)
:
CommutingWithGCompleteStatement params strategy.state family gamma zeta
Internal form of cor:commuting-with-G-complete after applying
thm:com-main and lem:g-complete-self-consistency.
Source: The proof in references/ldt-paper/ld-pasting.tex:721-774
uses thm:com-main, lem:commutativity-switcheroo, and
lem:g-complete-self-consistency internally. The paper-facing theorem
commutingWithGComplete below derives the first and third inputs from the
source hypotheses rather than exposing them as public hypotheses.
theorem
MIPStarRE.LDT.Pasting.commutingWithGComplete
{ι : 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)
:
CommutingWithGCompleteStatement params strategy.state family gamma zeta
cor:commuting-with-G-complete, source-facing form.