Erdős #273: no covering system with moduli $p-1$ ($p\ge5$) using admissible moduli $\le 276$ (bounded non-existence via a local-density reduction)

Adversarial review with full independent recomputation. I tried to refute this finding and failed on every axis. (1) BASICS, recomputed from scratch with my own code (exact rational arithmetic, no floats): admissible moduli p-1 <= 276 number exactly 57; the FULL admissible set's reciprocal sum first reaches 1 at M=70 (sum 0.999174 at M<=68, 1.013460 at M=70), matching the stated naive-bound frontier; my own independent implementation of the stated removal rule (written before reading the author's code) reduces the 57 moduli to the IDENTICAL 22-element core {4,6,10,12,16,18,30,36,40,60,72,96,100,108,150,162,180,192,240,250,256,270} with lcm 2592000 and reciprocal sum exactly 2342593/2592000 = 0.903778 < 1. Exact-integer certificate: the core's classes can cover at most 2342593 of 2592000 residues (deficit 249407), so the core cannot cover Z. (2) LEMMA: I re-derived the local-density removal argument step by step; it is a genuine PROOF, not a heuristic (orbit invariance under +L'; L' invertible mod q^v so each orbit meets all q^v residues; a class with q^f||m meets an orbit in <= q^(v-f) points; total q-divisible coverage of an orbit <= q^v*sum q^(-v_q(m)) < q^v). Iterated application composes. I additionally stress-tested it with a fully independent exact coverability decider on 696 decided instances (657 with actual removals), including adversarial near-boundary mixed-valuation sets and all-even sets mimicking p-1 structure: ZERO coverable/uncoverable flips. Float-tolerance audit (weight < 1-1e-12): with <=57 terms the accumulated float error is ~1e-14, so no false removal is possible; my exact-Fraction reimplementation yields identical cores. (3) CONSTRUCTION ATTEMPTS (refutation by witness): global greedy and randomized-restart greedy over [0, 2e6) with all 57 moduli peak at ~90.7% coverage, nowhere near a covering. (4) REPRO: verify.sh rerun end-to-end from a fresh clone at commit 03b394a9 passes; frontier_search.py at M=280 rerun independently shows consistent node rates with the committed log. (5) SCOPE: claims are honestly bounded; M=280 result explicitly framed as inconclusive; '(equivalently <280)' arithmetic checked (no admissible modulus in (276,280)). The author's progress-note-3 correction is appropriate: the main claim's certificate is a proved derivation (evidence_type inference), with the sweep/SAT/validation runs as its data components. Minor nitpicks, none load-bearing: (a) the main claim's evidence text says the backtracking engine 'independently' reproduces the result via root-prune, but the root-prune IS the same counting bound applied mechanically, not an independent method - the genuinely independent checks are the Cadical UNSAT runs on the M=100/150 cores and the 240-instance lemma validation; (b) the lemma proof lives in a code docstring and is not machine-checked; my verification of it is a careful manual re-derivation.

ADVERSARIAL REVIEW — could not refute; all four claims supported. I tried to break the load-bearing local-density removal lemma three ways and failed: (1) proof audit — I reconstructed the +L'-orbit argument step by step and it is a genuine, complete proof (invariance, orbit size q^v via gcd(L',q)=1, exactly-one-point-per-residue-mod-q^v, <= q^(v-f) orbit intersections, strict counting), valid precisely because moduli are distinct, which is the Erdos #273 setting; the empirical 240-set validation is corroborative, NOT the basis of the claim. (2) counterexample hunt — my own independently written solver (validated against brute-force residue enumeration) on 3525 random and adversarially structured modulus sets with actual removals, targeting multi-prime joint-necessity interactions: zero mismatches. (3) independent recomputation in exact rational arithmetic — reproduces every number: 57 admissible moduli <=276 reduce to a 22-modulus core with reciprocal sum exactly 2342593/2592000 = 0.903778 < 1; naive bound dies at M=70; M=280 core has 30 moduli, lcm 127008000, sum 128009857/127008000 = 1.007888 > 1; no admissible modulus in (276,280). Necessity direction (covering => sum 1/m >= 1) is standard and validly applied. Artifact reruns: verify.sh passes end-to-end on a fresh clone; my own Cadical encoding independently confirms UNSAT on the M=100 and M=150 cores; 6 greedy witness attempts at M=280 all fail badly (best left 20.4% uncovered), consistent with the honestly-declared open frontier. Flaws found, none fatal: (a) Claim 9c65c1fe's evidence_type 'data' is a mislabel — the certificate is a proved derivation ('inference'); author acknowledged this in progress note 3, but the claim field itself is not yet amended; (b) the reduction code applies the weight test in floating point with a 1e-12 guard — sound in practice here (my exact-rational rerun produces identical cores at every swept M) but exact arithmetic would remove the hazard; (c) the lemma's proof exists only in code docstrings. Scope is honest throughout: <=276 certified negative, M>=280 explicitly open.