Every result on this site is checked by the same small toolchain. This page explains how it works, for a developer or researcher who wants to see the machinery rather than take the word “certificate” on trust. Every code block below is copied from the repository with its source file named in the bar above it, and is verbatim except where a redaction is marked inline in <angle brackets>. Exactly one block carries such a mark, and it stands in for a private file path. Every number traces to a verdict file or a battery output named beside it.
None of the mathematics is ours, and the page says so before showing any of it.
The primitives are textbook material, credited. Interval arithmetic is Moore (1966). The existence-and-uniqueness operator is Krawczyk (1969), building on Moore’s test. The radii-polynomial contraction argument is the van den Berg–Lessard framework over the Banach fixed-point theorem. Exact rational arithmetic reduces fractions with Euclid’s gcd, which is older than the notation used to write it. Even mutation testing — the discipline this shop leans on hardest — is DeMillo, Lipton & Sayward (1978). Nothing on this page is offered as new mathematics, and no priority is claimed for any of it.
What is unusual is the synthesis, and it is unusual on purpose. Four choices, each of which trades something away and says what it traded:
git clone and node and nothing else. The cost is
real and stated in the trade-offs table below.ledger/tools/mutate.js), and anything short of the pair (nonzero, zero) is a
failure, not partial credit.REFUSED and OUT-OF-SCOPE
are outputs, not failures. An enclosure that cannot be established is reported as exactly that,
with its reason — because a wrong enclosure is worse than a refusal, and a silent one is
worst of all.The floor of the stack: an interval library where the exact real answer is trapped between two doubles.
JavaScript gives no access to the FPU rounding mode, so directed rounding is simulated rather than switched on: every IEEE-754 basic operation returns the correctly rounded nearest double, so the exact real result lies within half an ulp of the computed value — and widening each computed bound outward by one ulp therefore encloses it. That is the entire rigor model, stated once in the file header and relied on everywhere downstream. It is conservative by about a factor of two in the last bit, which costs nothing at the accuracy these certificates need.
function nextUp(x) {
if (Number.isNaN(x) || x === Infinity) return x;
if (x === 0) return Number.MIN_VALUE;
_f64[0] = x; _u64[0] += (x > 0 ? 1n : -1n); return _f64[0];
}
function nextDown(x) { return -nextUp(-x); }
/* an interval is a 2-array [lo, hi]; `iv(x)` is the thin (point) interval */
const iv = (lo, hi) => [lo, hi === undefined ? lo : hi];
const ZERO = iv(0), ONE = iv(1);
function add(a, b) { return [nextDown(a[0] + b[0]), nextUp(a[1] + b[1])]; }
function sub(a, b) { return [nextDown(a[0] - b[1]), nextUp(a[1] - b[0])]; }
function mul(a, b) {
const p = [a[0] * b[0], a[0] * b[1], a[1] * b[0], a[1] * b[1]];
return [nextDown(Math.min(p[0], p[1], p[2], p[3])),
nextUp(Math.max(p[0], p[1], p[2], p[3]))];
}The library is not trusted on assertion: eqcert/tests/test-interval.js checks every
export against exact BigInt rational arithmetic on thousands of random operands, and
mutation-tests the widening itself — removing the outward step turns the battery red. The file
header also keeps a confession worth repeating here: the sentence citing that test was false
from the day it was written until 2026-07-28, because the test file did not yet exist, and in
that gap pow silently returned [1,1] for every negative exponent. A cited
test is not a test. The battery exists now, runs first in make check-eqcert, and covers
every export — and the defect is documented in the source rather than scrubbed from it.
If K(X) lands strictly inside X, the map F has exactly one zero in X. Strict interiority is the whole content.
To certify that a numerical candidate x₀ sits next to a true zero of F, the stack evaluates the Krawczyk operator K(X) = x₀ − A F(x₀) + (I − A DF(X))(X − x₀) over a box X around the candidate, in interval arithmetic, with A a plain float approximate inverse that carries no evidentiary weight. If K(X) ⊂ int(X), Banach applies and F has a unique zero in X. The loop below is the operator core: build the box, sweep the interval Jacobian, form each row of K, demand strict interior containment, and grow the box honestly when containment fails.
for (let round = 0; round < maxRounds; round++) {
const X = x0.map((v, i) => iv(I.nextDown(v - rad[i]), I.nextUp(v + rad[i])));
const J = DF(X);
const K = new Array(n);
let ok = true, maxRad = 0;
for (let i = 0; i < n; i++) {
let acc = sub(iv(x0[i]), d[i]);
for (let j = 0; j < n; j++) {
let s = ZERO;
for (let k = 0; k < n; k++) {
const jk = J[k][j];
if (jk[0] === 0 && jk[1] === 0) continue;
s = add(s, mul(iv(A[i][k]), jk));
}
let m = [-s[1], -s[0]];
if (i === j) m = add(ONE, m);
if (m[0] === 0 && m[1] === 0) continue;
acc = add(acc, mul(m, sub(X[j], iv(x0[j]))));
}
K[i] = acc;
if (!interior(acc, X[i])) ok = false;
maxRad = Math.max(maxRad, (acc[1] - acc[0]) / 2);
}
if (ok) return { ok: true, box: X, image: K, maxRad, rounds: round + 1 };The same file carries the radii-polynomial driver for the sequence-space problems, and its header records the sharpest lesson in the stack: until 2026-07-30 the file’s own comment stated the self-map condition p(r) < 0 and the contraction condition κ = Z₁ + Z₂r < 1 as if they were one condition — and the code implemented the documentation faithfully. They part company at the vertex of p, where κ = 1 exactly: existence survives (Brouwer), uniqueness does not. The guard that closes this is quoted in the refusal section below, because its interesting property is what it returns.
Where the question is an identity, no rounding is tolerated at all — the arithmetic is exact integers.
Structural claims — a bracket identity, a determinant equal to 1, a coefficient extracted from
a paper’s displayed formula — are decided in exact rational arithmetic over JavaScript’s
native BigInt, so equality means equality. The fragment below is the entire exact core
of one independent verifier (a Lane B re-check of a published counterexample): a Euclidean gcd,
a normalising constructor, and field operations on reduced pairs. Fourteen lines, no library.
const gcd = (a, b) => { a = a < 0n ? -a : a; b = b < 0n ? -b : b; while (b) { [a, b] = [b, a % b]; } return a; };
function frac(n, d = 1n) {
n = BigInt(n); d = BigInt(d);
if (d === 0n) throw new Error("div0");
if (d < 0n) { n = -n; d = -d; }
const g = gcd(n, d) || 1n;
return [n / g, d / g];
}
const fadd = (a, b) => frac(a[0] * b[1] + b[0] * a[1], a[1] * b[1]);
const fmul = (a, b) => frac(a[0] * b[0], a[1] * b[1]);
const fneg = a => [-a[0], a[1]];
const fzero = a => a[0] === 0n;
const feq = (a, b) => a[0] === b[0] && a[1] === b[1];
The two layers meet at one carefully guarded seam: a rational enters interval arithmetic only through an enclosure proved to contain it — outward double division with a containment check, or exact squaring of endpoint doubles for a square root. The Maxwell verdict below runs its constants (ε = 1/6 and the charge qε = 859/248832, computed exactly from the paper’s equation (1)) through exactly that seam.
The stack’s distinctive verdicts are the negative ones, and they are engineered as carefully as the positive one.
Three refusals are built into the arithmetic itself: interval division throws on a
denominator straddling zero (no finite interval encloses 1/x there), pow refuses
non-integer exponents rather than quietly flooring them, and any such throw inside a certificate
attempt is counted as a certification failure, never a pass. The most instructive refusal
sits at the end of the radii-polynomial driver. The self-map condition has verified, a radius
exists — and the driver still refuses, because the contraction factor is not below one and
uniqueness has not been established:
const kappa = add(iv(Z1), mul(iv(Z2), iv(r)));
if (!(kappa[1] < 1)) {
return Object.assign({
ok: false, r, rMin, rMax, disc, kappa: kappa[1],
why: 'contraction factor Z1 + Z2*r >= 1 at the smallest radius closing p(r) < 0 — ' +
'T is a self-map of the ball but NOT a contraction on it, so existence may hold ' +
'but local UNIQUENESS does not follow (kappa is increasing in r, so no larger ' +
'radius helps)'
}, base);
}The guard’s own header records its measured teeth: before the fix, 84 of 2520 deliberately
near-tangency triples returned ok with κ ≥ 1 (the file quotes the witness triple); in the
regime the shipped certifiers actually run, the discriminant sits about twelve orders of
magnitude from tangency, so this was a loaded trap rather than a live wound — no certificate
in the ledger is affected. The refusal is pinned red-verified by R8 in
eqcert/tests/test-eqcert.js: a constructed triple with p(r) < 0 and
κ ≥ 1 must come back refused, and both shipping certifiers’ operating points must still
certify — a guard that refuses everything is not a guard either.
“The falsifier exists” and “the falsifier works” are two different, unverified claims wearing the same sentence.
A green check is evidence only if the same check demonstrably goes red on a broken tree. One tool is permitted to write that record, and its header comment is the best statement of the discipline in the repository — quoted in full, including the seven steps it executes inside a throwaway git worktree so the live tree is never touched. One line is redacted: the patch argument names a private path, and it is replaced by <the falsifier’s pinned patch>. Nothing else is altered, and the redaction is marked rather than silent because a page arguing for checkability cannot ask you to take its quoting on trust:
* WHAT "RED-VERIFIED" MEANS AND WHY BOTH DIRECTIONS ARE REQUIRED.
* A falsifier's whole job is to be wrong about a broken kernel. If nobody has
* ever actually broken the kernel and watched the falsifier's cmd exit
* non-zero, "the falsifier exists" and "the falsifier works" are two
* different, unverified claims wearing the same sentence. Conversely, a
* falsifier that is ALSO red on the unmodified, correct tree is not strict,
* it is broken — it would report red against anything, the same defect as an
* attack vector that "survives" from a region where nothing varies. So this
* tool runs the cmd twice, patched and clean, and requires the pair
* (nonzero, zero). Anything else is a FAILURE, not a partial credit.
*
* THE SEVEN STEPS (verbatim from ARCHITECTURE.md §5.3):
* git worktree add --detach .work/mutant HEAD
* git -C .work/mutant apply <the falsifier's pinned patch> # stale patch = FAILURE, not skip
* run cmd with cwd .work/mutant # MUST exit NONZERO
* git -C .work/mutant checkout -- . # unpatch
* run cmd again # MUST exit ZERO
* git worktree remove --force .work/mutant
* write last_red = {at, patched_exit, clean_exit, target_sha256, tree_commit}Note what the pair of exit codes buys. The planted mutant flipping red proves the checker is
sensitive to the thing it claims to check; the clean tree staying green proves it is
strict — a checker that is red against everything has no teeth either, the same defect
as an attack that “survives” where nothing varies. There is deliberately no
--skip-stale flag: a mutation patch that no longer applies is a failure, because the
falsifier has not been shown to go red against the tree as it exists today. The recorded
result pins the target file’s sha256, so the moment anyone edits that file, every claim resting
on the record goes stale until the mutation is re-run.
Candidate → Krawczyk box → Hessian sign → disjointness → claim gate → mutation controls. The whole pipeline on one published claim.
In July 2026, Arathoon, Ball & Kvalheim posted a disproof of Maxwell’s conjectured bound on the critical points of an electrostatic potential: five positive charges whose potential has at least 24 nondegenerate critical points, exceeding (5−1)² = 16 (arXiv:2607.27197). Their own verification is floating-point computer algebra — Mathematica and Maple checks, no code artifact shipped. This stack’s independent re-verification pins the paper’s HTML rendering by sha256, extracts the configuration from the displayed formulas alone, and certifies the paper’s own depicted instance ε = 1/6. Per candidate point, one function does all the evidentiary work:
function certifyPoint(cfg, x0) {
try {
const A = inv3(hessF(cfg, x0));
if (!A) return { ok: false, why: 'float Hessian singular — no approximate inverse' };
const res = krawczyk(X => gradIv(cfg, X), X => hessIv(cfg, X), x0, A, { radCap: 1e-6 });
if (!res.ok) return res;
const H = hessIv(cfg, res.box);
const det = det3Iv(H);
const tr = add(add(H[0][0], H[1][1]), H[2][2]);
return {
ok: true, box: res.box, rounds: res.rounds,
rad: Math.max(...res.box.map((b, i) => Math.max(b[1] - x0[i], x0[i] - b[0]))),
det, detOk: !contains(det, 0), traceOk: contains(tr, 0),
idx: classifyIndex(H, det),
};
} catch (e) {
return { ok: false, why: 'interval refusal: ' + e.message };
}
}Float Newton produces 24 candidates from the paper’s Lemma 2 seeds — carrying no evidentiary weight. Each candidate then gets a Krawczyk box (existence + local uniqueness), an interval Hessian determinant over the whole box excluding zero (nondegeneracy), and a harmonicity witness (zero must lie in every trace interval — real teeth against a wrong distance power). All 276 box pairs must be pairwise disjoint, so 24 boxes mean 24 distinct points. Then one gate states the claim:
const CLEAN = certifyAll(CFG, CAND, false);
say(CLEAN.nOk === 24, `Krawczyk certifies existence + local uniqueness in all 24 boxes (got ${CLEAN.nOk})`);
say(CLEAN.nDet === 24, `interval det Hess excludes 0 on all 24 certified boxes (got ${CLEAN.nDet}) — nondegeneracy`);
say(CLEAN.nTrace === 24, `harmonicity witness: 0 in trace Hess interval on all 24 boxes (got ${CLEAN.nTrace})`);
say(CLEAN.disjointOk, `all ${24 * 23 / 2} box pairs disjoint; min coordinate gap ${CLEAN.minGap.toExponential(2)}`);
say(CLEAN.holds, 'CLAIM GATE: 24 disjoint certified nondegenerate critical points => 24 > 16 = (5-1)^2');Measured, from the verdict of record (research/challenges/laneb-maxwell/VERDICT.md):
| quantity | value | meaning |
|---|---|---|
| run | node verify.js · exit 0 · 20 checks PASS · wall 0.1 s | Node 24, Apple Silicon; only imports are the eqcert stack |
| instance | ε = 1/6 · qε = 859/248832 exactly | the paper’s own Figure 1 value; charge from eq. (1), computed in exact rationals |
| certified boxes | 24 of 24 · radii 1.5e-13 … 5.5e-12 | Krawczyk existence + local uniqueness per box |
| nondegeneracy | 24 of 24 · min |det Hess| 1.3e-6 | interval determinant excludes 0 on every box; the minimum (at the origin) equals the (125/2048)ε⁶ prediction to 3 digits |
| distinctness | all 276 pairs disjoint · min gap 1.37e-3 | nine orders of margin between box size and spacing |
| structure | Morse totals {index 1: 10, index 2: 14} | Sylvester sign intervals per box; matches the paper’s Remark 2 accounting |
| mutation M1 | 1 of 24 certify | sign of the ε⁵ term of eq. (1) flipped — the bifurcated family reorganizes |
| mutation M2 | rejected by disjointness | one candidate duplicated: all boxes still certify individually — the counting has teeth, not just the enclosures |
| mutation M3 | 0 of 24 certify | ε⁵ term dropped: Hess V(0) becomes the exact zero matrix, origin refuses |
Scope, stated the way the verdict states it. This certifies ONE epsilon, not the paper’s “for all sufficiently small ε”; AT LEAST 24 critical points, not an exact count; and it does not audit the paper’s lemmas as theorems — their point list only seeded Newton. The authors’ CAS checks are a verification, so no claim is made to the first verification of anything. What the certificate adds is an enclosure a third party can re-run from a terminal, with mutation controls proving the pipeline can say no.
Against the classical tools, stated without hedging in either direction.
| dimension | this stack (eqcert, JS/Node) | Arb / MPFI (C) | Lean 4 + mathlib | C++ suites (CAPD, kv) |
|---|---|---|---|---|
| speed | interpreter overhead accepted; the shipped verifiers run in ≤ seconds because the problems are kept small | wins by orders of magnitude; arbitrary precision | not the point | wins by orders of magnitude |
| scope | rational functions, integer powers, enclosed exp/log/cos; finite-dimensional Krawczyk; no rigorous ODE integrator | full special-function library, ball arithmetic | anything formalizable, at formalization cost | rigorous ODE/PDE integration, dynamical systems machinery |
| trust base | IEEE-754 correct rounding of + − × ÷ √ plus a ~130-line arithmetic file you can read in one sitting | large, mature, well-tested C codebase | a proof kernel — the deepest axiomatic grounding available | large, mature C++ codebase |
| install friction | git clone + node, nothing else: no compiler, no CAS licence, no package manager | C toolchain + deps | elan + mathlib cache (gigabytes) | C++ toolchain + CMake + deps |
| audit one claim | one file, self-contained; prints the sha256 of what it read; its checker is mutation-tested in both directions | library call inside your program; you audit your program | kernel-checked, definitionally airtight; auditing means reading the formalization | library call inside your program |
| negative verdicts | REFUSED / OUT-OF-SCOPE are structured outputs with reasons | NaN-like ball blowup; caller interprets | a proof fails to compile | exception or divergence; caller interprets |
The verdict line: the classical tools win on scale and axiomatic depth, and it is not close — nobody should re-implement Arb in JavaScript, and nothing here approaches a kernel-checked proof. This stack wins on friction and auditability: the distance from “I doubt this” to a red or green terminal is one clone and one command, and the checker in the middle is small enough to read and proven able to go red. Both sides of that trade are deliberate.
Both directions of one certificate, from the public repository, in about a minute.
These two commands were re-run from a fresh shallow clone on 2026-08-05 before being quoted
here. Node only — no API key, no GPU, nothing installed. The clean run prints
"verdict": "CERTIFIED"; the planted-mutant run prints "verdict": "REFUSED"
with "refuse_reason": "max residual 1/5 exceeds ε=0" — the same checker,
demonstrating on demand that it can say no.
git clone --depth 1 https://github.com/carlostoledo1891/mfg-lab
cd mfg-lab/technical-reports/alien-science
node dual-client.js --fixture heldout-ccs-es # -> "verdict": "CERTIFIED"
node dual-client.js --fixture heldout-ccs-es --plant-mutant # -> "verdict": "REFUSED"Golden files beside it pin the expected JSON of both commands, so a disagreement between your terminal and this page is a finding, not an argument. For what the certificates on this site can and cannot prove — and what is refused — the standard is stated once, at /certificates. The results themselves live under /technical-reports, and the defects this toolchain has caught in its own earlier versions are published at /defects.