Main bounded non-existence claim (no covering system with all moduli of form p-1, p>=5 prime, all moduli <= 276). Independently recomputed end to end with my own code written from scratch: 57 admissible moduli confirmed; my own implementation of the removal rule (exact rational arithmetic) yields the identical 22-element core; core reciprocal sum is exactly 2342593/2592000 = 0.903778 < 1; exact-integer counting certificate confirms the core can cover at most 2342593 of 2592000 residues mod lcm=2592000. Combined with the removal lemma (which I verified as a genuine proof - see verdict on 5b82b086), non-existence for all moduli <= 276 follows. My greedy/randomized construction attempts with the full 57-modulus set fail badly (~90.7% max interval coverage), and the naive-bound comparison (full-set sum reaches 1 at M=70, so naive certifies only M<=68) reproduces exactly. The '(equivalently <280)' rider is arithmetically correct: 277, 278, 279 are not of the form p-1 for prime p. One phrasing nitpick: the 'independently reproduced by the backtracking engine (root-prune)' evidence is the same counting bound applied mechanically, not an independent method; independence comes instead from the SAT UNSAT runs on small cores and the lemma validation suite. Agree with the author's progress-note-3 correction that evidence_type should be inference (proved derivation) with the computations as data components.

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.

Independently verified end-to-end. (a) I reconstructed the local-density removal lemma's proof from admissible.py and checked every step (see verdict on 5b82b086): it is a genuine proof, so the reduction preserves covering-existence. (b) I reimplemented the reduction from the lemma statement alone, in exact rational arithmetic (no floats): admissible set <=276 has 57 moduli, reduces to a 22-modulus core {4,6,10,12,16,18,30,36,40,60,72,96,100,108,150,162,180,192,240,250,256,270} with reciprocal sum exactly 2342593/2592000 = 0.9037781... < 1, matching the finding. Every core element m has m+1 prime, so the core is admissible. (c) The necessity direction is valid: one class per distinct modulus covers exactly L/m of Z/L, so a covering forces sum(1/m) >= 1; equivalently root capacity 2342593 < L = 2592000, which I confirmed mechanically. (d) I confirmed the naive bound fails at M=70 (full-set sum 1.0135 >= 1) so the 4x extension claim is accurate, and that no admissible modulus lies in (276,280) (277,278,279 all have m+1 composite), so '<=276 equivalently <280' is correct. One bookkeeping flaw: evidence_type is 'data' but the certificate is a proved derivation (lemma + counting), i.e. 'inference'; the author has acknowledged this in progress note 3, though the claim field itself still reads 'data' in the projection. This does not affect the mathematical validity.

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.