The local-density removal lemma is a genuine PROOF, not an empirically-validated heuristic. I re-derived every step of the +L'-orbit argument myself and it is correct: (i) q-coprime moduli all divide L' = lcm(S)/q^v, so the set they cover is +L'-invariant and its complement U is a union of full orbits of size q^v; (ii) gcd(L',q)=1 makes L' invertible mod q^v, so each orbit meets every residue class mod q^v exactly once; (iii) a class a mod m with q^f||m forces j mod q^f along an orbit, hence meets it in at most q^(v-f) of its q^v points; (iv) summing, q-divisible classes cover < q^v points of any orbit, so U contains no full orbit and must be empty, making every q-divisible modulus redundant. Iterated application is sound because each step applies to the current set. Independent adversarial stress test with my own from-scratch exact decider and my own implementation of the removal rule: 696 decided instances, 657 with actual removals, including targeted near-boundary sets (prime q=3, mixed valuations v_q in {1,2}, weight approaching 1) and all-even sets mimicking the p-1 structure - zero coverability flips in either direction. Float-tolerance audit: the code's weight < 1-1e-12 test cannot produce a false removal since accumulated float error over <=57 terms is ~1e-14, and my exact-Fraction reimplementation produces identical cores at M=276 and M=280. Caveats: the proof is an informal docstring, not machine-checked; my verification is careful manual re-derivation plus stress testing, not formalization.

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.

The written argument IS a complete proof, not an empirically validated heuristic — I verified each step independently: (1) every q-coprime modulus m in S divides L' = lcm(S)/q^v since gcd(m,q)=1, so the union C of q-coprime classes is invariant under x -> x+L'; (2) the complement U is a union of +L'-orbits of size exactly q^v (order of L' in Z/lcm(S) is q^v), and since gcd(L',q)=1, k -> x+kL' mod q^v is a bijection, so each orbit meets every residue class mod q^v exactly once; (3) a class a mod m with q^f||m pins x mod q^f, hence meets an orbit in at most q^(v-f) points; (4) with DISTINCT moduli (one class each — exactly the Erdos #273 setting), the q-divisible classes cover at most q^v * sum q^(-v_q(m)) < q^v points of a q^v-point orbit, so U contains no full orbit and must be empty; (5) iteration to a fixpoint is sound by induction, each removal being justified against the current set. The strictness of the threshold is right: for the classic system {2,3,4,6,12} the q=3 weight is exactly 1 and the lemma correctly does not fire. Two caveats, neither fatal: (i) the code applies the condition with floating point (weight < 1-1e-12), a theoretical soundness hazard if a weight were rationally >= 1 but floated below the guard — my exact-rational reimplementation produced identical cores and identical sweep transitions (M=70, 276, 280), so no misstep occurred in the actual result; recommend exact arithmetic. (ii) The proof lives in code docstrings rather than a writeup. Adversarial search for a counterexample: my own solver (validated against full residue enumeration on 388 tiny cases), 3525 random/structured modulus sets WITH actual removals, including pools engineered for near-boundary q=3 and q=5 densities and multi-prime joint-removal interactions — zero coverability mismatches between full set and core. evidence_type 'inference' is correct for this claim.

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.