For even d, the discriminant of f_d = (∏(x−j))′ is a perfect square exactly at d = 4k(k+1) — proved, and re-proved as exact integer identities during this build with its planted falsifiers required to fire. Around it: a certified bracket for the constant c in the #290 density sum, assembled in exact rationals from pinned Galois densities — reproduced here byte-for-byte from the cited page's own programs, then TIGHTENED by running the same lifted instrument past the old horizon.
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)² (Altmann–Awtrey–Cryan–Shannon–Touchette 2020, non-monic factor restored); 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}, 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.
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..90. 30 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. One closure deserves its own sentence: d = 168 is an EXCEPTIONAL degree (4k(k+1) at k = 6, square discriminant by the theorem above), and the cited page explicitly left its Galois group undetermined — the squeeze has now closed it (survivor ES0), pinning the last exceptional density in range.
Under one assumption — for every even d ≥ 122, 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, both below 10⁻¹⁰⁰ at l = 61), and c is pinned to 34 digits, re-derived during this build:
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 even d ≥ 122; it is certified only through the pinned horizon, and the unconditional statement remains the bracket of §3 — the two are never conflated.
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, ~14 s), node narrowing.js (the bracket), node tools/run-erdos290-tail-ext.js (the continuation) from the repository.