bibkey: balister2018covering authors: “Paul Balister; Béla Bollobás; Robert Morris; Julian Sahasrabudhe; Marius Tiba” year: 2018 title: “On the Erdős Covering Problem: the density of the uncovered set” doi: 10.48550/arXiv.1811.03547 url: https://arxiv.org/abs/1811.03547 claim: “The paper develops distortion estimates for uncovered density, proves Schinzel’s divisibility-pair conjecture, and constructs near-covers with reciprocal sum below one.” strata_touched:
- D5/S3/Arith/Congruence/TwoOddPrimeUncoveredDensity license: citation-only triage: anchor
Distortion and uncovered density
Locator: https://doi.org/10.48550/arXiv.1811.03547; https://arxiv.org/abs/1811.03547, submitted 8 November 2018; metadata and abstract checked 16 September 2026. This is background for the distortion and second-moment route, alongside the squarefree paper.
An arbitrary-head application must uniformly extend each later prime-power block before applying the cap. Conditioning on pure-prime survivors alone does not remove old mixed classes; conditioning on all old survivors changes normalized cylinder costs. This proposed extension is not a quoted theorem of these papers and has no local Lean proof.
The primary v1 text was also read for the labelled-modulus application in report 348. Lemma 3.6 (pages 11–12) bounds moments by sums over congruence tuples; Lemma 3.7 bounds their divisor sums. Section 6 (pages 17–19) explicitly indexes all primes and accepts any constant kappa satisfying its second-moment hypothesis (20), then supplies the recurrence in Lemma 6.2 and the unrestricted continuation criterion in Theorem 6.1.
For at most two labels per numerical modulus, the tuple argument gains a single factor 4 in the second moment. The report proves this extension under the same distorted laws, and uses kappa=4 when the period is coprime to 210. An exact rational continuation reaches Theorem 6.1 at prime 167, proving noncoverage in that scope. This labelled extension is an ordinary deduction, not a literal statement of the paper’s distinct-modulus Theorem 7.1. The rational program checks the finite endpoint; it does not machine-verify the measure argument or replace the analytic tail proof.
Section 6, p.17, equations (19)–(20), permits any initial index i_0 and positive kappa satisfying the subsequent second-moment bound. The original surviving-mass quantity mu_(i_0) must be retained. Thus a support-restricted prefix product can be used as kappa at a checkpoint, then enlarged to the all-prime product for subsequent stages. Lemma 6.2, p.18, supplies the recurrence and its positive-denominator condition; Corollary 6.3, p.20, accepts f_k<=g_k. Table 1, p.19, explicitly gives downward-rounded lower bounds g_4>=5.860938, g_5>=9.032082 and g_6>=13.30344. Report348 reuses these published numerical bounds through the smaller rational thresholds 5, 9 and 133/10; it does not claim to recompute that table. Its repeated-label moment input also has the published KKL justification. Neither the table nor that citation is new Lean verification.
Theorem 10.1 of the primary v1, printed pp. 25–27 (statement p. 25, proof pp. 26–27), constructs, for every M>0 and epsilon>0, a finite distinct-modulus family with all moduli at least M, reciprocal sum below one, and uncovered density less than epsilon. Its proof supplies the stronger prime-support property: every constituent prime is at least M. It chooses disjoint sets P_j of such primes and moduli p Q_(j-1), where Q_(j-1) is the product of all earlier prime sets. Thus the moduli are squarefree; the final removal of classes preserves distinctness and the prime restriction.
Taking M above any prescribed cutoff greater than2 gives actual distinct odd near-covers supported entirely on larger primes. This specialization uses the construction, not an inference from large numerical moduli. Report 347, Section 8 combines it with an original-Haar overlap bound to constrain any hypothetical completion retaining every seed class. That completion constraint is a joint application, not a theorem stated in this paper.