A Two-Hole Obstruction in a 173-Mark Restricted Difference-Basis Shell

We prove a finite-shell obstruction for a restricted difference-basis feasibility problem at length 9999. The shell fixes 112 marks and selects exactly 61 additional marks from 490 admissible positions, giving 173 marks in total. For a specified set of 186 critical differences, every feasible shell state leaves at least two of those differences uncovered. The theorem is certified by an exact rational dual certificate for the full finite model. The certificate has objective 21/20, and integrality of the uncovered-difference count yields H ≥ 2. A companion pseudo-Boolean refutation derives the same contradiction from the hypothesis H ≤ 1. The reproducibility package contains the exact pseudo-Boolean instance, cutting-planes proof, rational certificate, an independent shell-to-OPB encoding verifier, an exact rational-dual verifier, a pseudo-Boolean algebra/package verifier, and a preserved external VeriPB replay log. The frozen public OPB and proof hashes were checked before replay, and VeriPB 0.3a0 returned “Verification succeeded.” with exit code 0. The result is deliberately scoped to the stated finite shell. It does not establish global nonexistence of all 173-mark restricted difference bases of length 9999.