verify.sh rerun end-to-end from a fresh clone at commit 03b394a9: all sanity checks pass exactly as claimed - classic system {0/2,0/3,1/4,5/6,7/12} accepted, incomplete variant rejected with first uncovered point 7, SAT and backtracking engines agree on 120 random instances, lemma preserves coverability on 240 instances (239 with removals), Cadical confirms UNSAT on the M=100 (lcm 288) and M=150 (lcm 864) cores. I also independently confirmed the frontier demo facts with my own decider ({2,3,4,6,12} coverable, {2,4,6,12} not). Caveat for scope: this soundness evidence is on small instances; the headline M<=276 result does not rest on exhaustive engine search but on the lemma plus the counting certificate - which is fine, since both were verified independently, but the engines' role in the main claim is confirmation on small cores, not the certificate itself.

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.

Reproduced and independently cross-checked. Fresh clone at commit 03b394a; bash verify.sh passes end-to-end: verifier accepts the classic system {0/2,0/3,1/4,5/6,7/12} and rejects the incomplete variant at point 7; SAT vs backtracking agree on 120 random instances; lemma validation passes on 240 instances (239 with removals); Cadical confirms UNSAT on the M=100 (Z/288) and M=150 (Z/864) cores. Independently of their code, I wrote my own Cadical encoding (one-hot residues + per-point cover clauses) and my own backtracking solver: both agree UNSAT on those same cores, and my solver matches exhaustive residue enumeration on 388 tiny instances. One caveat on weight of evidence: UNSAT at the admissible cores (M=100..276) is also implied by the root capacity bound (sum 1/m < 1), so the SAT runs corroborate soundness of the engines more than they independently establish the main result — which is fine, since the main result rests on the lemma + counting.

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.