Distributed tangent correction on a guarded candidate set
ProvedErdos390.WholePaper.BankPaperRealization.exists_canonicalDistributedSectionNinePostTangentOutput_of_paperBudgets_on_candidates_compactFix a bank realization at size , a guarded central-anchor certificate, finite exceptional and fixed factor sets, a finite candidate set , and a rounded selector satisfying the canonical tangent-input conditions for a finite band/cell partition of the tangent primes. Write for its tangent residual, for the canonical ratio-cell earthmover flow, and for the prescribed clean multiplier list of split request . Assume positive with , positive fixed factors and divisibility of their selector tail charge into the precharged target. Every prime lies at or below its band's last cell, and every cell through that last cell is occupied. Assume the weighted residual and port bounds and , total traffic at most , and . The paper main, error and ceiling budgets are at most , respectively. Each split request has positive canonical lower cardinality , with times either endpoint label. Every allowed multiplier places both endpoints in , where both selector values belong to . All lists use the specified natural parameters , dedicated rows and numerical guard set.
Then multipliers can be chosen with all numerical endpoints distinct, and there is a canonical post-tangent output whose selector is exactly the distributed update of . In particular, writing for request source, target and weight and for the selector valuation deficit,
This assembles collision-free tangent exactification while retaining an arbitrary guarded candidate support.
import Definitions.Def_erdos390_remaining_analytic_propositions_007 universe u_1
theorem Erdos390.WholePaper.BankPaperRealization.exists_canonicalDistributedSectionNinePostTangentOutput_of_paperBudgets_on_candidates_compact : Erdos390.RemainingAnalyticGoal007_001.{u_1} := by sorry