Source and certificate. Hough's numerical calculations occur on printed pp. 377–379 of the published paper. The source reports PARI/GP calculations. This compilation supplies a separate standard-library checker, verify_hough2015.py. No downloaded program is executed and no floating-point value decides a check. From the repository root, run

uv run --no-sync python library/covering_systems/hough_2015_solution_minimum_modulus_problem_covering_systems/evidence/verify_hough2015.py

It prints one line per named obligation and a summary line before the JSON certificate, whose exit_code equals the process exit status; any failed comparison exits nonzero, including under python -O. The interval arithmetic uses only the Python standard library; the check harness comes from the root tools package of the repository environment. Expected runtime is about ten seconds.

Statement. Put $M=10^{16}$, $\sigma=19/100$, $\delta=43/50$, $q_j=(j+1)^3-j^3$ and $S_n=\sum_{e^n<p\le e^{n+1}}(p-1)^{-3}$. The certificate establishes

and for the three integers $n=11,12,13$,

The last bound is stronger than the source's stated Lemma 7 bound. It retains the factor $0.88$ that Appendix A already proves for $n\ge14$. The scalar checks include

and every endpoint comparison used in the infinite-tail proof.

Complete proof of the finite certification. Set $D=2^{128}$. The checker represents a nonnegative real number by a pair of integers $(l,u)$ certifying $l/D\le x\le u/D$. A rational $a/b$ is enclosed by $\lfloor aD/b\rfloor$ and $\lceil aD/b\rceil$. Addition and subtraction use endpoint arithmetic; subtraction rejects any negative lower endpoint. Positive multiplication rounds $l_1l_2/D$ downward and $u_1u_2/D$ upward. The reciprocal, allowed only when $l>0$, rounds $D^2/u$ downward and $D^2/l$ upward. These follow from monotonicity on the nonnegative real line. A claimed strict inequality is accepted only when the left upper numerator is strictly smaller than the right lower numerator. Meeting or overlapping endpoints cause failure.

For $x\ge0$ rational, the exponential is enclosed using its positive Taylor series. After term $x^j/j!$, the remaining sum is at most

because the successive ratios of remaining terms are at most $x/(j+2)$. Terms and this tail bound are exact fractions. The checker continues until the tail is less than $D^{-2}$, then rounds the partial sum down and the partial sum plus tail up. For $a\ge b>0$ it similarly encloses

using the first omitted term divided by $1-z^2$ as an upper bound on the omitted tail. The identity follows by integrating the geometric series for $1/(1-z^2)$ from $0$ to $z$.

For a positive integer $a$ and rational exponent $r/s>0$, the checker forms the integer $N=a^rD^s$ and finds its integer $s$th root $h$, explicitly checking

Then $h/D\le a^{r/s}<(h+1)/D$. The integer root routine begins above the root and applies integer Newton descent

The inner floor does not change the final floor. The corresponding real Newton expression is at least $N^{1/s}$ by the arithmetic-geometric mean inequality. Thus the new integer is never below $\lfloor N^{1/s}\rfloor$. Whenever $x$ exceeds that integer root, $N<x^s$ forces a strict integer decrease. It terminates at the root, and the direct endpoint check is mandatory in any case. This provides the enclosures of $p^{81/100}$ and $M^{19/100}$; inversion gives the negative powers in the Rankin product.

The exponential enclosures certify the following exact prime cutoffs. The lower and upper endpoints have the same integer part in each case.

The checker sieves every integer through $1202604$. Starting with all integers at least $2$ unmarked, for each unmarked $p\le\sqrt{1202604}$ it marks the multiples $p^2,p^2+p,\ldots$. A marked number is composite. Conversely every composite has a least prime divisor at most its square root, and is marked when that prime is reached; no prime is marked. The unmarked list is therefore exactly all the primes through the cutoff. There are $93117$ of them, including $6048$ at most $e^{11}$. The output pins the entire ordered list by a SHA256 hash.

Differentiating the geometric series, or multiplying by $(1-z)^3$, gives the exact rational identities

Thus all finite products except the explicitly enclosed fractional powers use rational factors. The checker multiplies or sums every required prime factor with the outward operations above. It checks both the original and strengthened cubic-tail bounds for all three bands, and all initial and scalar inequalities. The checker passes all $23$ strict comparisons. Its JSON result contains the actual integer endpoints and positive margins, so the conclusion does not rest on rounded decimal displays or on the source's reported PARI run.

Proof scope. This is an ordinary finite computational certificate with an accompanying correctness proof, not a Lean or kernel check. The infinite prime bands are proved analytically in Lemma 7 relative to the exact Rosser–Schoenfeld input. The numerical checker pins the precise parameters; it does not read the paper and does not purport to verify the entire article by execution.

Bears on. Problem 2.