Someone asked, in an open GitHub issue, what number to put in the OEIS for Erdős problem #290 — and guessed its third digit. That digit is now PROVED. The constant is 0.546…, with no assumption of any kind, where every previous horizon could pin only 0.54…. It took closing 250 consecutive degrees of a computation nobody had run past d = 120.
Take P(x) = ∏_{j=0}^{d}(x−j) and f_d = P′, degree d. For EVEN d = 2l, recentring at d/2 makes f_d even: f_d(x + l) = h(x²) for a degree-l polynomial h. Four exact facts finish it: h(0) = (−1)^l (l!)²; the published composition law disc(h(x²)) = (−1)^l 2^{2l} · lead(h) · h(0) · disc(h)² (the non-monic composition law — Cullinan, The discriminant of a composition, which carries the leading coefficients explicitly; its hypotheses hold here since Res(h, x²) = h(0)² = (l!)⁴ ≠ 0); lead(f_d) = d+1; and disc(h) ≠ 0 by Rolle. Substituting:
so disc(f_d) is a perfect square exactly when d+1 is — that is, exactly at d = 4k(k+1). (Odd d are out of scope and need to be: there d/2 is a rational root, δ = 1, and that is where the log 2 that carries 83% of c comes from.) The build re-checks every line as an exact integer identity and requires the planted falsifiers — an index-from-1 misdefinition, a dropped non-monic factor — to FAIL. Until 2026-08-03 the source lab stated this law as a conjecture with 24 controls; it is a theorem.
c = Σ_d δ(f_d)/(d(d+1)), where δ(f_d) is the density of primes p for which f_d has a root mod p. Odd d contribute exactly log 2 (proved). Each even d = 2l contributes δ · 1/(2l(2l+1)) with δ pinned EXACTLY where the Galois group is determined — hyperoctahedral at all even d ≤ 120 except {8, 24, 48, 80, 120} (the exceptional d = 4k(k+1) in that range, each settled individually) — and the honest interval [0,1] everywhere else. Nothing is estimated: every pinned δ is an exact rational, every unpinned δ costs the full width of its weight, and the bracket can therefore only shrink as knowledge grows (the build asserts the recorded narrowing is monotone).
This build first REPRODUCES the cited page's pipeline byte-for-byte: the lifted narrowing program is re-run and must emit the identical record (it did: same bytes, sha-checked), landing on the cited [0.829113767875, 0.833228924528] at knowledge horizon l = 60.
Each pinned degree removes its own weight from the unknown tail, so the bracket can only shrink — and this is what that looks like when every point is recomputed in exact rationals at build time. Left of the shaded edge is the cited page's horizon; everything right of it is this repository running the same lifted instrument further.
The entire remaining width at l = 60 is the unpinned tail Σ_{l>60} 1/(2l(2l+1)). This repository ran the cited page's own five-candidate squeeze — the lifted galois-exceptions.js, byte-identical, nPrimes = 400, early exit — over l = 61..310. 250 degrees closed to a unique certified survivor — none refused. Result:
Each closed degree also extends the evidence base of §4's assumption: every one is a new even degree at which the group is verified to be one of the two allowed candidates. The extension record is certs/erdos290-tail-ext.json; a degree absent from it contributed nothing but honest width.
Some closures deserve their own sentence. The EXCEPTIONAL degrees past the cited horizon — d = 4k(k+1), square discriminant by the theorem of §1, the degrees the cited page could not reach and left with their Galois group undetermined — are 168 (k = 6), 224 (k = 7), 288 (k = 8), 360 (k = 9), 440 (k = 10), 528 (k = 11). The squeeze closed EVERY one of them (survivor ES0), so every exceptional density through l = 310 is now an exact rational.
Read this section as history. On 2026-08-31 van Doorn posted arXiv:2609.00104, which proves that liminf (b(a)−a)/log a = 1/(1+c) EXACTLY — a human write-up of a proof discovered with ChatGPT 5.6-Sol Pro. Theorem 8 is therefore no longer a two-sided interval, and the upper-endpoint sharpening this section describes no longer improves anything. What survives is better: the certified bracket on c above is now the numeric value of a constant that is known exactly, and to our knowledge it remains the sharpest published enclosure of it — the new paper states only "approximately 0.546" and makes no effort to compute it precisely. The reasoning below is left standing because it was correct when posted and because the lower endpoint 1/(1+c) is exactly what the new theorem singles out.
The bound this page set out to sharpen was one half of a pair. Van Doorn's Theorem 8 read 0.54 < liminf (b(a)−a)/log a < 0.61, with Lemma 31 supplying the lower endpoint 1/(1+c), Lemma 30 the upper endpoint 1/(2c), and Lemma 32 supplying 0.82 < c < 0.85. Both published constants are those two expressions rounded to two decimals — so the same constant c governs both, and a certified bracket for c moves both ends of the published interval, not one.
The upper endpoint costs nothing extra. 1/(2c) DECREASES in c, so it is fed by the bracket's certified LOWER endpoint — and the lower endpoint charges the unpinned tail zero, so no tail lemma, no assumption about the groups above the horizon, and no further degree enters it at all. Dividing the same bracket the other way, with outward rounding:
Setting the two together, Theorem 8 becomes 0.546083759260 < liminf < 0.602107563430 — the published interval narrowing from width 0.07 to 0.0560. Honesty about where that comes from: most of the upper-endpoint gain was already available at the cited horizon, which gives 0.603053548709; the continuation of §3 moves it the rest of the way. The published 0.61 is conservative mainly because 0.82 is a conservative reading of c, not because the horizon was short. Both numbers above carry the same Lemma 32 dependency as everything else on this page, and neither carries the §4 assumption.
Below d = 62 the lifted kernel needs no assumption: it carries the paper's hyperoctahedral range and the exceptional densities at d = 8, 24 and 48 as exact rationals. Under one assumption about everything above it — for every even d ≥ 62, Gal(f_d) is either S_l⁺ or its index-2 subgroup, which is true at every degree where the group has been determined — the tail telescopes with two explicitly-carried error terms (the index-2 allowance 1/(2^l l!) and the alternating-series deviation), and c is pinned to 34 digits, re-derived during this build:
That boundary is not asserted here, it is READ OFF the enclosure: the whole width of the interval above is the sum of the carried allowances, largest at l = 31 where one term costs 1.45e-47 — which caps this enclosure at 46 decimals no matter how large the cutoff, of which the record publishes 34. The derived constant 1/(1+c*) = 0.546229310400104587… (exact rational division of the enclosure) is the OEIS-shaped output. The assumption subsumes irreducibility of f_d for those degrees; it is certified only through the pinned horizon, and the unconditional statement remains the bracket of §3 — the two are never conflated.
The same telescoping run against THIS build's horizon instead of the cited kernel's — node tools/erdos290-cstar-precision.js — starts its assumption at d = 622 rather than d = 62, and the enclosure lengthens accordingly; that tool carries its own calibration against the kernel at the old horizon and writes the OEIS b-files.
This page supersedes the one cited in the erdosproblems #290 comment (posted 2026-08-04); that page and its programs are preserved BYTE-IDENTICALLY, hash-pinned through this repository's lift provenance, in the repository (the citation paths 301 here). Its self-contained programs — the theorem checker with its planted falsifiers, the narrowing pipeline, the five-candidate squeeze, the vendored exact-rational arithmetic — live beside it in the repository and are exactly what this build re-ran. To repeat it yourself: node theorem.js (the proof), node narrowing.js (the bracket), node tools/run-erdos290-tail-ext.js or, sharded across cores, node tools/run-erdos290-tail-shard.js (the continuation past l = 60) from the repository.