The method in the words of the method paper: what is read, how it is decided, which arithmetic secures the decision, which certifiers reduce an analytic question to finitely many exact ones, and the discipline, enforced by code that refuses, that guards the code. Every term used on this site is defined here once.
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.
| word | composed of | the witness the row carries |
|---|---|---|
| CERTIFIED | — | a certificate with its falsifier; re-runs without the engine |
| REFUTED | — | the falsifying object, printed |
| REFUSED | — | the reason; for a split refusal, two witnesses and the thresholds |
| PARTIAL | certified + refused | which fragment certified and which core was not reached |
| NEEDS DATA | refused, cause with the claimant | the bytes that would decide the row, named |
| MIXED | certified + refuted, one record | the counts of both, and the items refuted |
| REPAIRED | refuted + certified | the object as printed refuted; the object beside it certified |
| QUEUED | not a verdict | nothing; the row is not counted as decided |
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 10¹⁵ pairs of integer points be decided exactly on a 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.
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.