Collision-free distributed tangent realization from residual ledgers
ProvedErdos390.WholePaper.BankPaperRealization.tangentPaperDistributedSplitEndpointsDistinct_of_residualCensus_compactLet be finite, with an injective prime labeling , and let be a flow whose positive edges have distinct endpoints. Suppose its divergence is a residual vector , its total traffic is at most the distributed residual/cut ledger, and the incident flow at is at most , where is the port-load vector. Assume and , and with , , . Fix a paper bank, a compatible guarded central-anchor certificate, a finite exceptional set, and natural list parameters .
Take with . Suppose the total ledger is at most , and . The source's distributed main, error and ceiling budgets for these constants are required to be at most , respectively. Every split request must have a positive lower-cardinality bound no greater than its clean multiplier-list size, and must satisfy at either endpoint label .
Then one can choose a multiplier from each clean list so that all selected endpoint products are distinct. Moreover, divergence is , and for every natural prime-index ,
Here ranges over the split positive-flow requests, is its split weight, and its labels; denotes the natural factorization coordinate, defined also for nonprime . This turns explicit residual, traffic, density and parameter budgets into a collision-free realization.
import Definitions.Def_erdos390_remaining_analytic_propositions_008 universe u_1
theorem Erdos390.WholePaper.BankPaperRealization.tangentPaperDistributedSplitEndpointsDistinct_of_residualCensus_compact : Erdos390.RemainingAnalyticGoal008_001.{u_1} := by sorry