Finite Section 9 payload from a rounded selector and guarded slack
ProvedErdos390.WholePaper.BankPaperRealization.bankPaperCanonicalSectionNineFinalPayload_of_roundedSelector_guardedSlack_compactFix a regular mesh with , a bridge with its canonical partition and moment-ready certificate, a compatible bank and guarded anchor certificate, and endpoint selector . Assume dominates the reciprocal-prime quadrature cutoff; fixed-ratio prime count and occupancy hold at ratio ; ; and positive cell scale points are at least two. Let satisfy and . Require the rounded-selector tangent input with the actual Proposition 8.7 pointwise bound and its ratio-cell tail bound, guarded endpoint slack for the same selector, , divisibility of the fixed-factor charge into the precharged target, and the named fixed-component collision-free condition. The distributed main, error, and ceiling budgets must be at most , respectively. For every split request in the canonical ratio-cell flow, its prescribed lower cardinality must be positive, at most the actual clean-list cardinality, and have product with either endpoint label at least . Then, retaining all parameters literally,
This adapter uses only the rounded tangent input and guarded slack from the endpoint source; its finite analytic and collision hypotheses remain explicit.
import Definitions.Def_erdos390_remaining_analytic_propositions_004
theorem Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalSectionNineFinalPayload_of_roundedSelector_guardedSlack_compact : Erdos390.RemainingAnalyticGoal004_011 := by sorry