Five pull requests to the constants registry, decided where decidable

The registry's C₁a is the largest constant with max (f∗f) ≥ C (∫f)² over non-negative f on [−¼, ¼]; any explicit f is an upper bound. Atris's f has 65,536 equal steps with 13-digit rational heights; for a step function the autoconvolution is piecewise linear with its breakpoints on the grid, so its supremum is a grid value — computed here as one exact integer product (the heights packed into a big integer, multiplied, unpacked) and maximised over every shift: 645423412969467179759478160871915520/429496729600000035389440000000000729 = 1.502743486709583379743219592078…, the claimant's own fraction to the last digit, below 1.5027435 by 1.32 × 10⁻⁸. C₁b likewise: h on 114,688 steps with Σh = n/2 exactly and 0 ≤ h ≤ 1, correlated with 1 − h: 0.380858550316428560109786189090…, below 0.38085856. The registry's entries were 1.502862 and 0.380868.

Replayed for the registry, 2026-10-18. When the maintainer merged #225 he marked its two rows and the two EinsteinArena rows beside them with the asterisk, as replayed only by the submitting team's own checker. All four are decided here by two implementations that share no code with each other or with the claimants — instruments/optq/stepfun.py (Python, Fraction and int) and instruments/optq/stepfun-exact.js (JavaScript BigInt), run by tools/replay-stepfun.js — from the pinned bytes, against the bounds the registry prints, read from its pinned pages: every one CERTIFIED, with the same fraction in both. CodexProLong's heights are refused as published (Σh − n/2 = 1.92 × 10⁻¹³, not 0); scaled down to Σh = n/2 exactly, the repair the platform's own verifier makes in floating point, they certify the bound. The EinsteinArena heights are read as the doubles the JSON numbers denote, as the platform parses them; an earlier record here read the same text as exact decimals and got 0.38085857485785830932…, which certifies the bound too. Five red controls come out wrong in both implementations: a bound 10⁻¹⁵ below the exact value and a doubled height are REFUTED; a negative height, a height above one and CodexProLong's heights as published are REFUSED.

• C₁a · Atris [A2026] 65,536 steps: the registry prints ≤ 1.5027434868; the exact value is 1.50274348670958337974… — CERTIFIED
• C₁a · AgentDiscover [EA2026] 65,536 steps: the registry prints ≤ 1.5027435320; the exact value is 1.50274353195395969900… — CERTIFIED
• C₁b · Atris [A2026] 114,688 steps: the registry prints ≤ 0.3808585504; the exact value is 0.38085855031642856010… — CERTIFIED
• C₁b · CodexProLong [EA2026] 3,584 steps, scaled to Σh = n/2: the registry prints ≤ 0.3808585749; the exact value is 0.38085857485785830914… — CERTIFIED

A single law μ on Z² gives C₃c ≥ H(X−Y)/max(H(X), H(Y), H(X+Y), H(X+2Y)); this certificate mixes two laws across the digits of a base-55 expansion, 39041372760532870645 digits from a 51-point law and 60958627239467129355 from a 47-point law. The entropies add digit by digit only if the map from digit values to L(X,Y) is injective, which holds when every |L(x,y)| on both supports is at most (55−1)/2 = 27 — checked: the maximum is 27. Each per-law entropy is an interval with directed rounding at 128 bits (no code of the claimant's; the single-law instrument that decided C₃b and C₃c in September, with the mixture by rational weights on top); ρ ∈ [1.674894211307116228764343737060, 1.674894211307116228764343737061], above 1.674894211307116. The claimant's flint and PARI checkers print the same 16 digits. A second implementation, tools/verify_twolaw.py — the Python standard library alone, decimal at 120 digits, sharing no code with the first — decides it again: ρ ∈ [1.67489421130711622876434373706095, 1.67489421130711622876434373706096], and its three red controls fire (the smallest 30-digit claim above ρ is REFUTED; base 53, where (53−1)/2 < 27, is REFUSED for injectivity; a weight one unit off is REFUSED).

• C₂₀a ≥ 8 (CERTIFIED). X = E − 1 with E standard exponential: E[Eᵏ] = k!, so E[(E−1)⁴] = 9, E[(E−1)²] = 1, mean 0, and Var(X²) = 8; independent copies add variances, giving Var(|X|²) = 8n in every dimension against the registry's bound C n. The density e^{−t} is log-linear, hence log-concave. The registry held 2.
• C₂₀c ≥ √3 (CERTIFIED). The uniform law on [−√3, √3] has variance 1 and is log-concave; the half-line A = (−∞, 0] has μ(A) = ½ and boundary measure 1/(2√3), so its inverse Cheeger ratio is √3 — computed in Q(√3) through squares (1/3 and 3). The registry held √(π/2).
• C₂₃b ≤ ½ (CERTIFIED by reading). each step is a standard inequality applied correctly — the parity of a sum of n terms ±1 for odd n; trace of G − nI zero since diagonal entries equal n; the Frobenius norm bound from n(n−1) odd entries of absolute value >= 1; Bhatia--Davis (the variance of numbers in [λ_min, λ_max] with mean n is at most (λ_max − n)(n − λ_min)); the last two lines are algebra. A reading, held as such
• C₂₈a ≤ 9 (CERTIFIED, by the earlier record). OpenAI's BorsukNine is the Lean development this repository rebuilt and checked under two kernels on 2026-10-10 (certs/openai-math-kernel.json; the statement read MATCHES against the paper's claim). The PR adds nothing to decide and its wording agrees with the theorem.
• C₁₆a ≥ 2.156224 (CERTIFIED 2026-10-16, given the Parseval normalisation, read; refused as not attempted the day before). The registry's L is max over δ ≥ 1 of 4πΘ(δ) − ln δ − ln(1 + ln δ), with Θ(δ) the largest |u(0)|² over zero-mean u on the torus with ‖∇u‖² = 1 and ‖Δu‖² = δ; the torus is 2π × 2π, fixed by BDZ2013 (2.4) and (3.14), whose numerical 2.15627 is the registry's own row. The PR's u is the truncated BDZ conditional extremal, c_k = 1/(|k|²(|k|² + 41/5)) over 0 < |k|² ≤ 4000², a real zero-mean trigonometric polynomial, so Parseval gives ‖∇u‖² = 4π² S₁, ‖Δu‖² = 4π² S₂, u(0) = S₀, and after normalising, L ≥ S₀²/(π S₁) − ln δ − ln(1 + ln δ) with δ = S₂/S₁ — provided δ ≥ 1. Every sum is finite (no tail). Computed here with no code of the claimant's: r₂(n) from a sieve over the octant (50,265,328 points, equal to Gauss's circle count), each term's floor and ceiling at scale 2²⁰⁰, π by Machin in integers, the logarithms from the decimal module's correctly rounded ln widened one unit each way. δ ∈ [3.9318098247, 3.9318098248] ≥ 1; the bound ∈ [2.15622475379391336304, 2.15622475379391336305], width 1.4325148E-52 — above 2.156224 (the claimant prints 2.1562247…). The registry held (β + π)/π ≈ 1.82283. One note for the claimant: his cutoff-50 figure (2.15174) is not what μ = 41/5 gives here (2.151390); his 200, 800 and 4000 figures agree.
• C₇₀a ≥ 1.201927 (CERTIFIED 2026-10-16, given the four-step chain below, read; refused as not attempted the day before). The registry's C₇₀ is the least C such that every pair of centrally symmetric convex bodies in every dimension has a linear u with |det u| = 1 and |u(B₁) + B₂|^{1/n} ≤ C(|B₁|^{1/n} + |B₂|^{1/n}); a pair that no such u improves below c is a lower bound. The PR's pair is the cube of side a and the ball of radius r. Read and holding: u(B₁) is a parallelotope of volume aⁿ; Steiner's formula writes |u(B₁) + rB| through its intrinsic volumes; for a zonotope V_j is the sum of its j-face parallelotope volumes; Szász's inequality on the Gram matrix bounds the product of those volumes below by a^{n·C(n−1, j−1)}; AM–GM over the C(n, j) faces gives V_j ≥ C(n, j) aʲ. So the cube is already in its worst position and C₇₀ ≥ (Σ_j C(n, j) aʲ κ_{n−j} r^{n−j})^{1/n}/(a + κ_n^{1/n} r). The number at n = 300,000, a/r = 13/1000 computed here by outward-rounded decimal recurrences (κ_m = κ_{m−2}·2π/m from κ₀ = 1, κ₁ = 2; the binomials and tʲ step by step; the n-th roots through correctly rounded ln and exp): [1.20192714257250284496, 1.20192714257250284497], width 1.7E-48 — above 1.201927. At n = 2 the same code equals the closed form √(t² + 4t + π)/(t + √π). The registry held the trivial 1.

Mosaic Intelligence's submission is 104 files. Its scorer (verify/record_score.py) runs the assembly's verify.py and checks 12 gates — _report_ok, anchor_ok, cover_ok, coverage_ok, criterion_ok, frozen_ok, line_ok, lint_ok, record_lines_ok, rh_ok, script_ok, torus_ok — printing "TOTAL CHECKS RUN: 168846" (its own count; the scorer was never run here). The two mathematical checkers (python-flint arb; mpmath.iv) evaluate auxiliary quantities on frozen coefficient tables — walls, clocks, norms, debits, Taylor leaves — and compare rationals, hashes and box covers. No function in the 5 scripts evaluates ζ, H_t or the 690,988-term Dirichlet polynomial; the torus floor, the separator at X and the Polymath15 error constants enter as 63 frozen outputs whose proofs cite banks 713, 729, 744, 745, 755, 767, 774, 786, 791 — an internal memory that is not in the bundle. The anchor Λ ≤ 3/16 is the claimant's own 2026-07 row, merged into the registry without review. So the package certifies that its parts fit together as declared; whether the parts are true is not in the submission, and this page refuses rather than guesses. The route itself (collision exclusion with an exterior polydisc floor carried by a "circular heat" lemma) is coherent on reading; the first independent check to run would be the torus-floor inequality on T⁴ by an interval cover, then the separator at x = X for t ∈ [0, 3/16] including y = 0, then the error constants from Polymath15 Theorem 1.3 — each hours to days.

• The registry's definitions. Taken as written at 2c1968cd; whether 1b's interval of length 2 matches the literature's normalisation is the registry's business.
• The two reading rows. 23b is a proof read, not a computation; 28a rests on the earlier kernel record. Both are marked so. 16a and 70a are each a computation plus a reading: the number is enclosed, the derivation (Parseval; Steiner, Shephard's zonotope formula, Szász, AM–GM) is read, not re-proved.
• Mosaic's mathematics. Refusal is a verdict on the evidence submitted, not on Λ; Mosaic's three earlier certificates (C₃b, C₃c, C₇₁) were all true when decided here in September.
• Same-author second implementation. The Kronecker product is checked against schoolbook multiplication on random sequences and on closed-form functions (the constant function gives exactly 2; the half-step exactly 1); the claimants' printed values are the outside check.

Decided 2026-10-18. Two family-1 constants entered the registry with asterisked bounds from step functions. Both are decided here from the pinned bytes, against the bounds the registry prints, by two implementations that share no code with each other or with the claimants' verifiers (kept as text, never run): instruments/optq/autocorr.py (Python, every lag summed term by term) and instruments/optq/stepfun-exact.js (JavaScript BigInt, Kronecker products). Each gives the same fraction in both, and it is the claimant's own fraction.

• C₁c ≥ 0.4103287 — CERTIFIED. Barnard–Steinerberger's constant is the smallest C with min over t ∈ [0, 1] of ∫f(x)f(x+t)dx ≤ C(∫f)²; rozetyp's step function (K = 6,144, 6,148 integer weights) has its autocorrelation linear between multiples of 1/K, so the minimum is a grid value: 0.41032871754918741449…, the stated fraction exactly. A misprint: the page and the claimant's README give its decimal as 0.41030287175…; it is 0.41032871754…. The bound column is right. The earlier K = 3,072 certificate holds too: 0.410302117239… ≥ 0.4103021.
• C₁d ≤ 1.463071582607559 — REFUTED as printed; C₁d ≤ 1.4630715826075594 CERTIFIED. The signed third autocorrelation constant; the certificate is a 300-cell signed function given in the body of pull request 224 (its digest matches the bytes only with CRLF line endings, as pinned). Its exact ratio is 1.4630715826075593274614…, the stated fraction exactly — and that is above the bound printed in the table and the README, 1.463071582607559. An upper bound must round up: the certificate shows C₁d ≤ 1.4630715826075594, not the printed number. What is refuted is that this certificate gives the printed bound; nothing here says the constant is above it.

Red controls, which must come out wrong in both implementations: a C₁c bound 2·10⁻¹⁵ above the exact value and a C₁d bound 10⁻¹⁵ below it are REFUTED; a negative weight and a C₁d function changed to integral zero are REFUSED. Record certs/autocorr-replay.json; re-derive with node tools/replay-autocorr.js (both, about two minutes) or --check.

Decided 2026-10-19. The registry's newest asterisk: C₈₆ ≤ 1.8117251 (R. Pinho, pull request 227, merged 2026-10-18), the Schur–Siegel–Smyth trace constant, from a 629-cell step measure on [1/20, 1037/200] and eleven integer polynomials with rational weights — the construction of Talebizadeh Sardari–Orloski with seven more polynomials. The claimant states six finite conditions, the hypotheses of Smith's sufficiency criterion [Smi24] and the arithmetic of the bound; given the published chain (the minimum principle, Smith's theorem), read and cited, they give the bound. The six are decided here from the pinned bytes by two implementations that share no code with each other or with the claimant's checker (kept as text, never run): instruments/optq/c86.py (Python: Fraction, and its own float-series logarithm rounded outward) and tools/replay-c86.js (JavaScript: eqcert's BigInt rationals and interval library). CERTIFIED in both.

• Exact (E1, E2, E3, E6). Densities non-negative, edges increasing, the support inside [1/20, 1037/200]; each polynomial primitive, irreducible over ℤ (no integer root, no monic integer quadratic factor within the Mignotte bound — enough for degree ≤ 5) and totally real (a Sturm count equal to the degree); Σ b_Q deg Q = 6638236823/8000000000 < m = 39999999999997/40000000000000; and ∫x dμ / m = 144938007612277893/79999999999994000 = 1.811725095153609541…, the certificate's own fraction, below the printed 1.8117251.
• Enclosed (E4). ∫ log|Q| dμ for each of the eleven Q as a closed form in g(u) = u ln|u| − u at the edges, the roots enclosed to 2⁻⁸⁰ by Sturm bisection: every integral is positive, the smallest lower end 9.999 × 10⁻⁵ (the claimant reports ≈ 10⁻⁴ each).
• Enclosed (E5). f = U_μ − Σ b_Q log|Q| ≥ 0 on every cell of the support, by adaptive bisection: on each box the two cell-edge terms (an infinite slope at the edge) and any −b ln|Q| with Q vanishing on the box are bounded by their exact monotone ranges, the smooth rest by a second-order Taylor form at the midpoint. Proved on 3,658 boxes (JavaScript) and 3,658 (Python), depth ≤ 8, the smallest certified lower bound 2.313 × 10⁻⁸ and 2.313 × 10⁻⁸ (the claimant's arb bisection: 6,218 subintervals, 7.4 × 10⁻⁸).
• Not decided. The extension of E5 from the support to ℂ (the minimum principle), the resultant argument that makes μ/m arithmetic, and Smith's theorem itself [Smi24] — published mathematics, read and cited by the claimant and here. The replay is of the certificate's finite conditions, which is what the asterisk is about.

Red controls, which must come out wrong in both implementations: densities scaled by 0.98 (f dips below zero: REFUTED by a box with f < 0), weights scaled by 1.3 (E3), extra mass in the first cell of the support (E4 and E6), the bound lowered by 10⁻¹² (E6), x² − 3x + 1 replaced by (x − 1)(x − 2) and by x² + 1 (E2). Pins: the certificate at commit 116a58f (sha256 722a287b74a9…), the registry's 86a page and README at 46dbf036. Record certs/c86-replay.json; re-derive with node tools/replay-c86.js (both, about ten minutes) or --check (the JavaScript decider and the red controls, about two minutes).

Decided 2026-10-19. Two asterisked upper bounds for C₈₂, the essential minimum of the Zhang–Zagier height h(α) + h(1 − α): C₈₂ ≤ 0.2534449 (R. Pinho, pull request 229) and C₈₂ ≤ 0.2535744749068227 (Épi, September 2026). Both are Doche's limit-point construction [Doc01b]: integer polynomials R_j with multiplicities and S_i with rational exponents give, with T(z) = z(1 − z), B = (log M(Q∘T) + ∫₀¹ max(0, log|A∘T| − log|Q∘T|) dt) / deg Q, and C₈₂ ≤ B. B is decided here from the pinned bytes by two implementations that share no code with each other or with the claimants' checkers (kept as text, never run): tools/replay-c82.js (JavaScript: Gaussian integers for the roots, eqcert's outward-rounded intervals) and instruments/optq/c82.py (Python: integers, and doubles with a priori rounding-error bounds). Both rows CERTIFIED in both, given Doche's theorem that B bounds C₈₂, read.

• Exact. Every factor has integer coefficients; every denominator is monic up to sign with a positive integer multiplicity; every exponent is a rational ≥ 0; deg A = Σ q_i deg S_i < deg Q (999,999,992 for the certificate); every numerator is coprime to every denominator (gcd 1 modulo a prime that divides neither leading coefficient).
• Roots, certified. Each composed factor P∘T (degree up to 84) has its 2,058 roots enclosed: approximations refined in Gaussian integers at 2⁻¹⁹² (JavaScript) or 2⁻²⁰⁰ (Python), then Gershgorin's theorem on the Weierstrass matrix with the corrections computed exactly — every disk isolated, the radius below 5.0 × 10⁻¹⁶ after rounding to doubles.
• The integral. On [0, ½], doubled (the coefficients are real), on dyadic panels: a zeroth-order bound from |u(t) − u(t_c)| ≤ πw, and where every root is away from the panel a second-order Taylor form with |g″| ≤ 4π² Σ |w_k| |r_k| / dist². 13,318 panels for the certificate (JavaScript), 13,364 (Python).
• [Pin26]. B ∈ [0.2534446872487, 0.2534446875146] (JavaScript) and [0.2534446872487, 0.2534446875146] (Python), below the printed 0.2534449 by about 2 × 10⁻⁷. The claimant's own certified value 0.25344468733… lies inside both enclosures.
• [Epi26]. B ∈ [0.2535689301873, 0.2535689304235] and [0.2535689301873, 0.2535689304235]: the construction gives 0.2535689…, about 5.5 × 10⁻⁶ below the printed 0.2535744749068227 — the row is a valid but weaker bound than its own construction, the safe side, as the row's comment already notes. The claimant's copy of Épi's construction is byte-for-byte the same numbers.
• Controls. doche2001 CERTIFIED (B ≈ 0.25443616 against 0.25444); grinsztajn2026 CERTIFIED (B ≈ 0.25362692 against 0.2536331090204145); mutated-v3 REFUTED (B ≈ 0.26306769 against 0.2534449) — Doche's and Grinsztajn's constructions reproduce their published bounds, and the claimant's planted failure is refuted.
• Not decided. Doche's theorem — that B bounds C₈₂ — is read, not re-derived; the claimant's README proves it directly (Uⁿ − Wⁿ over the primes, Jensen's formula, coprimality), and its hypotheses are the exact checks above.

Red controls, which must come out wrong in both implementations: Épi's construction against 0.25356, below its B: the certificate's B is shown to be at least the bar (REFUTED); a numerator factor equal to a denominator factor (exponent 1/2): U and W are not coprime (REFUSED); a denominator factor with its coefficients doubled: not monic up to sign (REFUSED); every exponent doubled: deg A no longer below deg Q (REFUSED); a denominator factor squared into one polynomial: its roots are double and cannot be isolated (REFUSED); an exponent written as a JSON float (0.5): not an exact rational (REFUSED). Pins: the certificate at commit 69d8964 (sha256 b33626f367b6…), Épi's construction at 97fa6a42 (sha256 e85e26fa7122…, the digest its own result file names), the registry's 82a page and README at 46dbf036. Record certs/c82-replay.json; re-derive with node tools/replay-c82.js (both, minutes) or --check (the JavaScript decider, about a minute).

Decided 2026-10-27. The registry's rule since 2026-10-26 asks a second party to confirm a replay before a mark comes off; the contributor who confirmed ours on C₃₁ had filed two certificates of their own, for the Ramsey-multiplicity constants of K₅ (#277) and K₆ (#279), with no second party. Each is a step graphon — 192 blocks of equal measure with red values R_ij/2²⁰ for K₅; the 1,024 blocks of Z₂¹⁰ with a red value depending only on the Hamming distance for K₆ — and the claim is its monochromatic density t(K,W) + t(K,1−W), an exact rational that bounds the constant from above by the standard random colouring. Both densities are decided here by two implementations that share no code with each other or with the claimant's evaluators (kept as text): instruments/optq/graphon_k5.py and graphon_k6.py (Python Fraction: the K₅ count as a trace on each pair's common support; the K₆ count by translation, the row classes of four vectors, binomials for the fifth and the S₄ quotient) and instruments/optq/graphon-second.js (JavaScript: the K₅ count modulo ten 25-bit primes lifted by the Chinese remainder theorem; the K₆ reduction derived again in BigInt). CERTIFIED, both, given the standard random-colouring argument that the density bounds the constant, read.

• C₈₉b ≤ 0.0016870052 — CERTIFIED. The K₅ density is 0.0016870051344094195654…, the fraction the page states to the last digit (10721871642517…/63555655070790…, both implementations); the printed bound is that value rounded up at ten places. 592 s in JavaScript, 87 s in Python.
• C₈₉c ≤ 0.7422548616 * 2^-14 — CERTIFIED. The K₆ density × 2¹⁴ is 0.7422548615936250610698…, the fraction the page states exactly; the printed bound is it rounded up and nearest at ten places. 12.5 s in JavaScript, 24.4 s in Python.

Controls: raising one block-pair value by 2⁻²⁰ moves each density in both implementations; a printed bound one unit below the K₅ value at its last place fails; the constant graphon W ≡ ½ gives 2⁻⁹ and 2⁻¹⁴ exactly; and the published 192-vertex graph of Parczyk, Pokutta, Spiegel and Szabó (Zenodo 6602512, pinned) read as a 0/1 graphon gives their published K₅ value 2320651/1358954496. Pins: the certificates at 98b6ee34 (the K₅ folder byte-identical to the 82a6e4de the page cites), the 89b and 89c pages from the pull-request branches (they are not on the registry's main branch). Record certs/graphon-replay.json; the battery re-derives the K₆ value and the five controls at every run and re-combines the K₅ integers.

Decided 2026-10-27, as the second party. maximusrufus, who re-ran three of our records, filed the enclosure 2.1562247706 ≤ C₁₆ ≤ 2.1562256466 (#246, merged asterisked on 2026-10-26): a lower certificate from one trial polynomial, and an upper certificate of 84 boxes in δ with a tail bound, a convexity argument and numpy checkers. Under the registry's rule a mark comes off only on a second party's confirmation; nothing of theirs had been re-decided by anyone.

Gaps, at the pin.

• The checkers test a tolerance, not the printed inequality. The lower checker accepts |L − claimed| < 10⁻⁹ and the upper accepts U ≤ claimed + 10⁻⁹; neither prints VERIFIED for the inequality against the printed digits. Both inequalities are decided here against the digits directly.
• The certifiers are not in the repository. The checkers name certify_c16_upper.py and certify_c16_lower.py; neither is published. The asymptotic bound g they use was re-derived here by hand and agrees with the checker's formula.
• Two float fields slip by 10⁻¹² against their own rationals. The rounded-down lower float sits 10⁻¹² below its rational and the upper float 10⁻¹² above; both slips fall on the safe side.
• The registry's numerical row lies above the upper end. The page keeps a numerical value ≈ 2.15627 [BDZ2013]; any value printing as 2.15627 is at least 2.156265, above the upper end 2.1562256466 that #246 claims (PARTIAL here, below).

What was decided. Two implementations that share no code with each other or with the claimant — tools/replay-c16.js (JavaScript, this repository's outward-rounded interval kernel) and instruments/optq/c16.py (Python, exact rationals and directed decimal rounding) — decided every finite claim written down before either decider existed (corpus/optconst-queue/c16-2026-10-27/claims.json).

• C₁₆ ≥ 2.1562247706 — CERTIFIED, given the Parseval normalisation for that explicit function, read. The trial polynomial (|k|² ≤ 4000², μ = 1221/10000, 50,265,328 lattice points, checked against Gauss's count) gives exactly 2.15622477064423579…; the printed bound is its floor at ten places.
• C₁₆ ≤ 2.1562256466 — PARTIAL. The finite core is CERTIFIED by both: the 84 boxes tile [1, 4.9·10⁸] exactly, every box's supremum is at or below the printed digits, and the asymptotic bound at the last box's end is 2.05869178083391…. The boxes in fact support 2.1562256458 (box 31); the printed bound is conservative by about 8·10⁻¹⁰. The step from the finite boxes to the constant is analysis, read and re-derived by hand in the claims file, not computed, so the end is PARTIAL by this repository's rule.

What the upper end rests on, in the order the bound travels through it:

1. assumed
   The weighted Cauchy–Schwarz bound F ≤ B_μ on each box an inequality between infinite sums; three lines, re-derived here; no machine checked it (claims.json, UR1)
2. assumed
   The tail of S₁ beyond the partial sum, through Catalan's constant bounds on an infinite sum; (A) rests on a classical identity, (B) on an integral comparison; both re-derived here. The value of G and π are computed, not read; no machine checked it (claims.json, UR2)
3. assumed
   The asymptotic bound g beyond the last box the claimant's g is stated in the checker with its derivation in certify_c16_upper.py, which is NOT in the repository; re-derived here from the write-up's 'μ = 1/(δ ln δ)' and found to be the same function; no machine checked it (claims.json, UR4)

The finite core under them is exact, in two implementations; the weakest premise is assumed: on this ladder a proof read and re-derived by hand is where the checking stopped, since no machine checked it. That is why this end is PARTIAL, and why the lower end, which crosses none of these steps, is CERTIFIED.

Red controls, which must come out wrong: C_16 <= 2.1562256457, one unit in the tenth place below the bound the boxes support (2.1562256458); C_16 >= 2.1562247707 from the same trial polynomial (the printed lower bound one unit up); box 31 (μ = 0.12206997134993264) with its printed bound 2.1562256465510825 replaced by 2.1562256407485436, below the lower end of its endpoint maximum 2.1562256407495; box 40 removed from the tiling of [1, D0]; a mutant decider with S1(μ) taken as its partial sum over |k| <= 2000 alone (the UR2 tail omitted) certifies C_16 <= 2.1562240, below the certified lower end 2.1562247706 — caught by the crossing; the full decider cannot close box 31 on the same claim (REFUSED). Pins: the registry at e95af44b, the certificates at b3728b85. Record certs/c16-replay.json; re-derive with node tools/replay-c16.js (both, about four minutes) or --check (the JavaScript decider, about a minute).

Decided 2026-10-27, as the second party. The same contributor's K₄ bound, C₈₉ ≤ 0.0301388794 (#255, merged asterisked), is a step graphon with 3,840 blocks of equal measure and red values in 2⁻²⁰ℤ; the claim is its monochromatic K₄ density, an exact rational.

Gap, at the pin. The registry's README lists C₈₉'s best upper bound as 0.0301388857 ([Kos2026], #264), while the constant's own page carries the smaller 0.0301388794 ([SK2026], #255): the README cell does not show the page's best row.

• C₈₉ ≤ 0.0301388794 — CERTIFIED. The density is 0.0301388793132559…, the fraction the page states exactly (272208384594…/903180180540…); the printed bound is that value rounded up. Two implementations that share no code with each other or with the claimant's evaluators (kept as text) agree on both integers and on every one of the 3,840 blocks at all nine primes: instruments/optq/graphon_k4.c (C: every block, no symmetry, modular, threaded, on one rented 32-vCPU pod in 120 minutes of kernel time) and instruments/optq/graphon-k4-second.js (JavaScript: exact integers, one term per orbit of ordered block pairs under seven block permutations, each verified exactly before use; about a minute on the laptop).

Controls: perturbing one block value moves the density; a printed bound one unit below at its last place fails; the constant graphon W ≡ ½ gives its known value; the published 768-vertex graph of Parczyk, Pokutta, Spiegel and Szabó read as a 0/1 graphon gives their published K₄ value; blocks 0 and m−1 re-derived without the symmetry agree. Record certs/graphon-k4.json with the pod's residues verbatim in certs/graphon-k4-blocks.txt; node tools/replay-graphon-k4.js --check re-lifts them and re-derives block 0 in seconds.

• Cited by a registry, 2026-10-18. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): A fourth asterisk removed — C₃c's two-law certificate — on our replay, merged by T. Tao (pull request #230). In their words: “by C. Toledo, 17 Oct 2026; asterisk removed.” (the source, pinned)
• Cited by a registry, 2026-10-26. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): Four more asterisks removed on our replay — the C₁a and C₁b step-function rows (Atris; EinsteinArena's AgentDiscover and CodexProLong) — merged by T. Tao (pull request #232) minutes after he stated the second-party rule; the two pages cite the replay as [T2026b]. In their words: “by C. Toledo, 18 Oct 2026; asterisks removed.” (the source, pinned)
• Cited by a registry, 2026-10-26. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): Two more asterisks removed on our replay — C₁c and C₁d — merged by T. Tao (pull request #243), the C₁d bound now printed rounded up, above the value first printed; the two pages cite the replay as [T2026]. In their words: “by C. Toledo, 20 Oct 2026; asterisks removed, and the $C\_{1d}$ bound printed rounded up” (the source, pinned)

Each credit is quoted from a snapshot pinned by sha256 (corpus/recognition.json); each re-run is a row of corpus/external-reruns.json. Neither is a peer review.