Absorbed clean-list bounds for every distributed request
ProvedErdos390.WholePaper.BankPaperRealization.eventually_canonicalDistributedSectionNineCleanListLower_absorbed_compactanalytic-number-theoryerdos-390erdos390-source-construction
Write , , , and . Fix , , , and . Assume and put . Eventually, uniformly over bank realizations and guarded certificates, fixed exceptional subsets of the upper tail, arbitrary finite band and ratio-cell assignments, residuals, and split parameters, assume , , below the central-anchor cutoff, and the fixed-ratio cell geometry at . For every split request in the ratio-cell earthmover flow, its prescribed lower cardinality satisfies
This supplies all requestwise clean-list hypotheses of the distributed Section 9 construction.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_004 universe u_1
Formal statement
theorem Erdos390.WholePaper.BankPaperRealization.eventually_canonicalDistributedSectionNineCleanListLower_absorbed_compact : Erdos390.RemainingAnalyticGoal004_015.{u_1} := by sorrySource