We graded the graders

The accepted-but-wrong region has width 2·tol − w and is empty only when tol ≤ w/2 — at which point the grader accepts a sub-interval of the certificate and has become a certificate grader with gratuitous rejections. The ratio of band to certificate, ρ = 2·tol/w − 1, is 562,949 here: the grader will accept a band 562,949 times wider than the proof.

This is the figure that answers the standard remedy. A published bug taxonomy for reward verifiers lists exactly this failure — a loose numeric tolerance accepting a nearby wrong value — and prescribes tightening the tolerance. Four orders of magnitude of tightening take the absolute-tolerance grader from 99.4% to 44.4%, and the only tolerance that reaches zero is one that has stopped being a tolerance.

Soundness is (1 − false-accept) × (1 − false-reject), because either rate alone is gameable: a grader that rejects everything has a perfect false-accept rate and is useless, which is why every run carries controls drawn from INSIDE the enclosures. The exact-match row is the honest opposite failure — it accepts nothing wrong and rejects 24.4% of the submissions that are right, including the midpoint printed at full double precision.

A canary asserts that a value is PROVABLY WRONG. That assertion is the product, so it may not rest on a decimal somebody re-typed: every fact below is read out of a record in certs/ at load time, and the record is sha256-pinned beside it. If a record changes, the battery refuses rather than minting canaries from a stale number. Minting from a fact that is not marked certified throws — it does not degrade.

One of these is not like the others. erdos852.cstar carries the value a real problem thread actually published for the quantity: 0.0752403861777, which sits outside our certificate by 6.09e-13 and inside any ordinary tolerance of it. Every other canary in the suite is constructed. That one is a reproduction — the refutation is here.

Decide whether f > 0 on the whole domain — and support it. HOLDS must ship a dyadic tiling whose every cell carries a verified positive lower bound; FAILS must ship a witness. A bare verdict scores zero however correct it is, because a verdict without evidence is indistinguishable from a lucky guess. Of 12 instances, 10 carry a needle — a notch narrow enough that any coarser grid steps over it — 5 are two-dimensional and 2 are razor-thin. Scoring: +1 correct WITH evidence · 0 correct but unsupported · +0.25 honest UNDECIDED · -1 wrong.

The bluff row is the design. It samples, decides HOLDS, and then dresses its sampling grid as a tiling — a VALID tiling, so it passes the combinatorial check. The one cell holding the needle then refuses to verify, and it scores -6.00: worse than abstaining. Faking the format was never the hard part. The budget-limited sound solver is what makes the abstention reward real rather than decorative — it abstains where it cannot finish and is never wrong.

Invert the polarity. The model is not asked to construct a correct object; it is shown a grader and asked to BREAK it — to produce a value the grader accepts and that is provably wrong. Ground truth is free, because a certified enclosure decides both halves without a human. Every environment in existence trains provers; this one trains verifiers.

Two of the four rungs cannot be broken, for two different reasons: on one the tolerance is NARROWER than the enclosure, so the band of accepted-but-wrong values is empty as arithmetic; on the other the grader compares against the certificate itself, so no such value exists at all. The correct answer there is NO_ATTACK, and claiming a break that does not verify scores worse than saying there is none. A model that has learned "attack whatever you are shown" fails half the ladder — which is the behaviour worth measuring, because an auditor that always finds something is exactly as useless as one that never does.