The machine

Generation is crowded. Judgement is not. This machine decides mathematical claims — other people's and its own — in exact arithmetic, and publishes the refusals beside the verdicts. Five rules do all the work — the first is the one everything else pays for — and each is a measurement rather than a promise.

It is one system with two faces. The same certifiers feed the reports — 62 pages, each re-deriving its record at build, refused by the gates below when a number moves — and the instruments — 20 pages where the same arithmetic runs in the reader's tab and every mark says what decided it; 7 of those run a battery in this build's test as well. Neither face illustrates the other; both are read off the records this page counts.

• A fast check may only rule things out. Floating point screens by the million and is never allowed to admit anything: of 819,152 objects enumerated, 16,943 reached an exact decision, and nothing reached a verdict without exact arithmetic behind it. A rounding error can cost time here and can never cost truth.
• Both verdicts are theorems. CERTIFIED means the statement was re-derived from whole numbers; REFUTED means a falsifying witness exists and it is printed. 54,628,296 closed forms have been refuted exactly — the value provably outside a certified enclosure — and zero discoveries have been claimed from that search.
• The third verdict is real, and it is counted with a denominator. An instrument that cannot decide says so. On claims other people submitted to the eval board the refusal rate is 13.0% of 301; inside the generation loop it is a different rate for a different thing, and the two are never added. Every refusal in the lab is counted by kind at the refusals ledger, which deliberately has no total.
• Every run carries forgeries that must fail. Deliberate near-misses are planted before anything real is graded — including one wrong by a billionth, invisible to any tolerance — and if one passes, the run aborts. 85 of 87 batteries were executed during this build, not remembered. Every genuine bug this project has found was caught that way; none by reading code.
• Independence is independence from the CLAIMANT. When this machine decides someone else's claim it does not run their code, and their code is never in the trust path — 18 published claims decided that way so far. It does not mean every checker is a clean-room rewrite of every producer: the two places code crosses that line are both ours and both disclosed in the limits.

Nothing in this section exists. It carries no numbers because there are none, and it is here so that the difference between what this machine does and what it intends is legible without asking. Each line moves into the table above on the day it has a record behind it.

• An exact-witness gym. The four rungs already exist as separate instruments — rank-R matmul schemes, bilinear products over F2, spherical codes, certify-or-refute a constant. What is missing is the packaging: one environment, one harness, a published pass-rate table, and the hack rate printed beside it. The rungs are built; the wrapper is not.
• A benchmark of the graders. Re-decide the exactly-checkable keys of public benchmarks and publish the error rate per source. CORRECTION, 2026-09-03: an earlier version of this line said nobody benchmarks the graders. That is false, and a literature pass found it out — verifier false-accept and false-reject rates are measured in the 2026 RLVR literature, including on deployed code-RL suites, and benchmark answer-key errors have their own papers. What is not in that literature, so far as this pass reached, is an adversarial set whose members are PROVABLY wrong rather than believed wrong: everyone else mutates a reference answer, and a certified enclosure refutes a value outright. That narrower thing is what remains to build here.
• An open-frontier environment. Every mathematics environment trains against problems with known answers. The one worth building has none: the reward is beating the current certified record, and the record ratchets when a rollout beats it — kissing numbers, matmul ranks, explicit constants. It cannot be graded without exact certification, which is the whole reason to attempt it here. Nothing of it is built beyond the ledger that would hold the records.

Everything above decides. Nothing above shows — and a chart is an assertion too. Charts and graders both assert things, and neither distinguishes what the data forces from what the renderer or the tolerance chose. The same sentence covers both halves of this machine, which is why the second half is not a side project.

Nine instruments carry it. Two of them draw a certificate from the shelf in §8 at its own resolution — the covering that forced an Erdős lower bound, shaded so the bright seams are where the argument nearly ran out, and the weights the linear programme chose inside those boxes. Five decide their headline number in exact integer or rational arithmetic. One is floats throughout and leads with that.

The grammar they are drawn in is four standings on a lattice — refused < chosen < computed < decided — combining by minimum, so a mark’s standing is the weakest standing on its path to the pixel. Three consequences follow and none is a judgement call: the arithmetic demotes and never the author, so a float step takes decided to computed automatically; refused is absorbing; and an argmax over a non-unique optimum yields chosen. Stroke carries it, never colour, so it survives greyscale — and where a figure’s marks all share a standing the channel is free, which is a rule found by porting four pages rather than by reasoning.