How a claim becomes a certificate

The inputs are claims and the bytes they rest on: constants, constructions, bounds, formal statements, printed tables, operating numbers — each pinned by the digest of the file that states it. The claimant’s program is never run in the trust path. What finishes within a day runs on a laptop; the formal challenges of a release ran on hosted runners; the largest kissing configurations ran on one rented GPU whose kernel first had to reproduce the laptop’s answers on smaller cases. Every decision writes a record: the inputs by path and SHA-256, the verdict, the witness, the scope, the machine, the time, and the second implementation’s reading where one exists. Every number on this site and in the papers is read from such a record at build time, and a page refuses to build when a record stops supporting a sentence.

A box is a product of closed intervals with rational endpoints; a printed number is the box its digits allow. A claim is a box B and a predicate φ whose functions have interval extensions — maps that provably contain the true range on every box. It is read in one of two ways: universally, as a mathematical statement that holds for every point of B; or epistemically, as an engineering number that holds at one unknown true input inside the declared envelope B.

The claim is CERTIFIED when the enclosures show φ on every box of a finite cover of B; REFUTED when they show its negation — at one proved point under the universal reading, on all of B under the epistemic one — with the falsifying object printed; REFUSED otherwise, with the reason, and, where two points of B have been proved to satisfy and to violate φ, with both witnesses and the thresholds that would decide. The verdicts are sound under the inclusion property of the extensions. A refusal is terminal: never retried at lower rigour, never turned into a probability, never dropped from the record. The only path from REFUSED to CERTIFIED is a new exact argument or the bytes the claimant had not yet published.

The register composes the three words into words that say what they are made of; none is a fourth verdict, and the kinds of refusal are never summed.

Exact rationals where a tie must be decided or the object is rational: reduced fractions of arbitrary-precision integers, doubles converted losslessly, linear systems solved by exact elimination that reports a singular matrix rather than a small pivot. Exact integers in floating-point hardware where the data are integer vectors: a product is exact as long as no partial sum can leave the range the format holds exactly, a bound checked against the data before anything runs and written into the record — which is what lets 9.72 × 10¹⁵ pairs of integer points be decided exactly on one GPU.

Outward-rounded intervals on doubles where the quantity is transcendental or the data are long: each computed endpoint is stepped one unit in the last place outward, so the true value lies inside, on the strength of the correctly rounded operations IEEE-754 mandates. No library function is trusted: elementary and special functions are truncated series with their remainders enclosed; long sums use compensated summation with an outward error bound; derivatives come from forward differentiation over the same arithmetic, so the derivative a proof uses is an extension of the function the proof is about. A malformed operand or an indeterminate result is refused by exception, never decided.

None of the certifiers is new; the assembly is, with the rule that each refuses rather than guesses. The Krawczyk operator proves that a box holds exactly one zero of a system, or refuses with “no contraction”. A negative-definite Hessian on a box with one critical point proves a unique maximiser — a fitted distribution, a time-horizon estimate. The corners of a multilinear form decide an inequality over a whole box. Sturm chains count real roots exactly; exact LP duality and Farkas certificates decide feasibility; sums of squares in exact rationals certify positivity; covering relations composed to an exact spectral argument bound an entropy. Each certifier ends in decisions of the kind §2 covers, and each is calibrated on a case with a known answer before it decides anything new.

• Screens prune, never admit. Floating point decides only what is worth certifying; a certifier is the only authority, and a screen that loses a planted known answer refuses the run.
• Red controls must fire. A red control is a deliberately wrong variant of a test that must be rejected; a battery whose red controls do not all fire fails, whatever its other checks say.
• Calibrate before you decide. A new machine, arithmetic or kernel decides nothing until it has reproduced a decision already made by an old one; a pre-registration states what a paid run will measure and at what cost it stops.
• Pin the bytes. Every claim is decided against a byte sequence named by path and SHA-256 and re-hashed at decision time; a page refuses to build when a pinned input, a verifier version or a battery has changed under it.
• Independence from the claimant. The decision is re-derived from the published statement and bytes. The precise form is that the system shares no code with the claimant: two of its own instruments reuse its own code across a producer–checker line, and the paper says which.
• Second implementations. Where a verdict is the product, a second program written from the specification in another language and arithmetic re-derives it. These are same-author checks and are counted apart from re-derivations by other parties.
• Records re-run. A record is re-derived, not believed: in the reader’s browser by the bytes that wrote it, and by the rerun kit from the standard library alone.
• Honest counting. A claim with no record gets no row; a correction added beside a refuted claim is never counted among the audited rows; a queued row is not decided; refusal kinds are never merged into one total.

• Certificate. What a CERTIFIED verdict carries: the inputs pinned by digest, the cover, the enclosures, and a statement of what would make it fail. It re-runs without the engine.
• Enclosure. An interval proved to contain the true value, by exact arithmetic or outward rounding; never a point and never an estimate.
• Verdict. One of three words — CERTIFIED, REFUTED, REFUSED — each with its witness; the register’s composed words (PARTIAL, NEEDS DATA, MIXED, REPAIRED) say what they are made of.
• Witness. The object that justifies a verdict: a certificate, a falsifying point or equation, the two points of a split refusal.
• Red control. A deliberately wrong input that a check must reject before the check counts.
• Battery. A program of checks with its red controls that exits non-zero when any fails; the control build runs every battery and refuses on a red one.
• Register. The public ledger of published claims decided here, one row per claim, each derived from a record.
• Pinned bytes. A file named by path and SHA-256 at decision time; a changed digest refuses the page that cites it.
• Refusal. A verdict, not an absence of one: the instrument did not reach a decision, and says why. NEEDS DATA is the refusal whose cause lies with the claimant.
• Independent. From the claimant: no code shared with the party whose claim is decided, and every certificate re-runnable with no engine present.
• Standing. What a mark in a figure, or a number in text, rests on, drawn in its stroke or its underline: decided (an exact decision backs it; solid, or plain in text), computed (float, a fit, a forecast, a number someone printed; dashed), chosen (one member of a set the data admit, picked by something that is not the data; dotted), and refused (no mark at all: the void). A mark takes the weakest standing on its path. Standing is not a verdict: a refutation proved here is drawn solid. The rules, each with the finding that taught it: the visual grammar.
  decided

  exact arithmetic backs it

  computed

  float, or a number someone printed; nothing decided it

  chosen

  one member of a set the data admits

  refused

  no mark — the void is drawn
• Premise grade. Where the checking of a model that a number rests on stopped, strongest first. validated checked against observations of the thing itself, held out, with the number. compared checked against a model that keeps more of the physics, with the number; not against the thing itself. verified the code reproduces an exact solution of its own equations; not measured against the thing itself. assumed adopted from a source, chosen, or read; no machine here checked it. A conclusion is as checked as its weakest premise, and the page that states it names that premise. A grade is never a probability.

• 9 October 2026. The erratum of 2026-10-09: the control page counted closed forms refuted by a FLOAT comparison (Math.sqrt, Math.pow, Math.exp, a midpoint times a rational) as refutations, and the engine ledger counted REJECT — which included enclosures that STRADDLE the bar — as decisions. The numbers as published are pinned in certs/erratum-2026-10-09.json (closed forms then counted refuted: 54,628,275; by the exact rule now: 54,647,578, of which 21 by exact arithmetic); the full account is in the build log.

Earlier defects, every one caught by a red control, a calibration, an impossible number or a byte pin, are counted in how the bugs were found; refusals of every kind, each with its own denominator, in refusals on record.

• The method paper (draft v0.10; not peer-reviewed) and the other papers, every number a macro from a record.
• The build log: every family, instrument, battery and certificate at this commit — the record under this page.
• The rerun kit: the command that re-derives each record of the register, with the standard-library verifier where one exists.
• The instruments: the same arithmetic in the browser, each page saying what decides its headline number.
• The visual grammar: how every mark on these pages says what it rests on, the rules and the findings behind them, and the module to draw them.
• Cite: Toledo, C. (2026). cert-machine: independent exact certification of machine-generated mathematics, v2026.10.27. doi:10.5281/zenodo.23698128 (concept DOI 10.5281/zenodo.22225860).