cert-machine · the third verdict

What the machine would not decide

A verifier that only ever passes or fails is a scorer. The third verdict — this instrument cannot decide, and here is why — is the one a motivated party would never build, so it is the one worth counting. Here is every refusal on record, by kind, each with the denominator it belongs to.

KINDS ARE NEVER MERGED on this page. REFUSED (our instrument declined) is not NEEDS DATA (the claimant published nothing to decide on) is not OPEN (a budget ran out, and the attempt is recorded) is not UNDECIDED (a swept cell that did not close) is not a scope limit (an audit that reached a fragment and says which). There is deliberately no total: one big number would be a bigger number and a smaller fact. Every count below is read from its record at this page's own build.

tl;dr

The finding. On submitted claims, the grader's refusal rate is 13.0% (39 of 301 claims carried nothing parseable to decide). Inside the generation loop it is 1 of 16,943 — a different rate for a different thing, and the two are never added. The largest refusal population in the lab is neither: it is 18,001 swept cells that did not close.
The mechanism. Every instrument here returns one of three things and never converts between them. A refusal is terminal: it is not retried at lower rigour, not downgraded to a probability, and not quietly dropped from the record. Absence of proof is never evidence of absence — the sentence that costs the most and is worth the most.
Check it. node tools/build-report-refusals.js rebuilds this page from the records; every number is read from the file named in its row, and the build refuses a row that cannot name its own denominator.

refusal rate, submitted claims

13.0%

39 of 301 claims on the matmul eval board carried no parseable proposal. 262 were decided: 115 certified, 147 refuted.

refusals in the loop

1 / 16,943

The generation loop's own rate, across 11 families. Narrow by construction — the loop only meets objects it enumerated itself.

undecided cells

18,001

Of 41,367 cells across the two regime maps. Published as holes in the map rather than filled in by interpolation.

kinds, never merged

REFUSED · NEEDS DATA · OPEN · UNDECIDED · SCOPE. Each carries its own denominator; the page has no total on purpose.

§1 · the ledger

Every refusal on record, by kind

kind	where	count	out of	record
REFUSED	the engine loop (keller-fibers)	1 / 16,943	objects certified this build	ledger.json
REFUSED	the matmul eval board	39 / 301	claims submitted	certs/matmul-eval-ledger.jsonl
NEEDS DATA	the kissing ledger, dimension 11	1 / 11	ledger rows	certs/kissing-ledger.json
OPEN	the Erdős #1038 supremum campaign	1 / 7	degrees attempted	certs/sublevel-tao179.json
OPEN	the λ(6) campaign	1 / 10	families in the worklist	certs/lambda56-campaign.json
UNDECIDED	the two-population regime map	9,915 / 21,567	cells swept	certs/mfg2p-regime-map.json
UNDECIDED	the MFG regime map	8,086 / 19,800	cells swept	certs/mfg-regime-map.json
SCOPE	the six-claim AI audit	6 / 6	lanes audited	certs/ai-claims-summary.json

Reading down the kind column is the point. These are five different behaviours that a single "refusals" counter would flatten into one: an instrument declining, a claimant publishing nothing, a budget running out, a sweep cell staying open, and an audit stating its reach. Only the first is a statement about the instrument.

§2 · intake

The refusal rate on claims other people submitted

The matmul eval board takes proposed exact rank-R decompositions from frontier models and decides each one in exact rational arithmetic. Of 364 real-model replies on record: 262 were decided (115 CERTIFIED, 147 REFUTED with the violated equation printed), and 39 were REFUSED because the reply carried no parseable proposal. That is a refusal rate of 13.0% on 301 submitted claims.

Two other outcomes sit in the same ledger and are NOT counted in that rate, because they are not our refusals: 23 replies in which the MODEL declined — it argued the target was impossible, which for the rank-6 ⟨2,2,2⟩ rung is correct and is Winograd's theorem — and 40 replies cut off by OUR OWN output cap, a harness artifact that says nothing about either party. Folding either of those into a refusal rate would inflate it with someone else's behaviour, or with our own plumbing.

why the denominator is stated every time

A refusal rate with no denominator is unfalsifiable, and a refusal count with the wrong denominator is worse than none. Every row on this page names the population it is a fraction of, and the build refuses a row that cannot.

§3 · scope

The audits, and exactly how far each one reached

The sharpest refusal in the lab is not a verdict at all — it is the sentence that says which part of a claim was checked. All 6 lanes of the six-claim AI audit carry one, and 1 of them ends at PARTIAL. A reader who takes "CONFIRMED" off this table without its scope column has been told something the record does not say.

claim	verdict	what was actually checked	named checks
Maxwell's point-charge bound	CONFIRMED	at ε = 1/6 only	17
The Korenblum constant	CONFIRMED	the numerical criterion	15
Erdős Problem #1038	CONFIRMED	the computational fragment	22
Ran–Teng Conjecture 20	PARTIAL	machine-checkable fragment only	38
The Mathieu property for Lie groups	CONFIRMED	supporting identities only	null
The rank-two Poisson conjecture	CONFIRMED	the explicit counterexample	null

§4 · at scale

Refusal as a map, not a footnote

The two mean-field regime maps sweep 41,367 parameter cells and decide each one by an exhaustive box argument. 18,001 of them — 43.5% — did not close at the budget, and they are drawn on the atlas as holes rather than filled in. A map with no holes drawn is a map that interpolated somewhere, and the reader cannot tell where.

The same discipline applies to whole campaigns. The Erdős #1038 supremum ladder closed six degrees and RECORDS the one it attempted and could not finish (deg9 — bnb: box budget exhausted); the λ(6) campaign has 9 of its 10 families closed and publishes the remainder as unfinished rather than waiting for a clean number. An attempted-and-failed row is worth more than a silent gap: it tells the next person where the budget actually broke.

§5 · the rule

What a refusal is not

Not a failure. The instrument behaved correctly. A refusal is the honest output of a decision procedure that met an object outside its reach, and it is recorded with the reason.
Not a soft verdict. A refusal is never retried at lower rigour and never converted into a probability, a confidence, or a "likely". There is no path in this lab from REFUSED to CERTIFIED that does not go through a new exact argument.
Not evidence. Absence of proof is never evidence of absence. That a claim could not be decided here says nothing about whether it is true.
Not deletable. A refusal that vanishes between builds is the failure mode this page exists to prevent: every count above is recomputed from a named record, so a refusal can only disappear by the record changing.
Not a total. The kinds are not commensurable and are never summed. If you want one number from this page, take the refusal rate on submitted claims — 13.0% — and carry its denominator with it.