How claims are graded
Every result on this site carries a grade and a boundary. The grade records how far the evidence actually reaches; the boundary records where it stops. This page states the rules, so that a reader can hold a finding to them rather than infer them from the findings themselves.
Evidence grades
Four grades, applied to the claim as written. The verb has to match the grade: a claim graded MEASURED may not say "proves".
Evidence grades
- PROVEN
- Follows from stated premises inside a named frame; the frame and trusted base are always shown alongside.
- MEASURED
- Empirical, with a stated sample and method.
- OBSERVED
- Witnessed in a specific instance, with no frequency claim.
- OPEN
- A question posed and not answered.
A grade is a statement about the evidence, not about importance. A PROVEN result inside a small frame can say less about the world than an OBSERVED one, and the frame is shown alongside so the two can be told apart.
What a claim carries
A grade on its own would be a label. These fields are what make it checkable. The finding page carries all of them except the trusted base, which is stated on the artifact's own project page against the same result.
| Field | What it records |
|---|---|
| claim | The result itself, stated in one sentence, with the verb matched to the grade. A result is said to be proved only when it is machine-checked inside a named frame, measured only with a stated sample, observed only in a single instance. |
| doesNotEstablish | What the result does not reach. A claim and its limit sit next to each other, in the same weight, so the boundary is not something a reader has to go looking for. |
| trustedBase (project page) | What has to be trusted for the result to stand: a proof kernel and its axioms, a compiler, an assumed transport, or an authored coding scheme. An authored label is part of the trusted base, not part of the evidence. |
| sample | The denominator, and what the result quantifies over. Numbers carry their denominators rather than appearing as "all" or as a bare rate. |
| verifiedAtCommit | The commit in the artifact's own repository at which the claim was checked. It is never the same hash as the site build commit in the footer, and the two are labelled differently. |
| reproductionProvenance | Whether the claim was actually re-executed in the verification pass, or confirmed by reading source at the pinned commit without re-running it. The weaker of the two is stated as the weaker one. |
| independentReproduction | Whether anyone other than the author has reproduced the result. On most findings here this reads "None known.", and author self-reproduction from a clean clone is recorded as what it is rather than counted as independent. |
| reproduceCommand, toolchain, expectedOutput | The command a reader runs, the pinned toolchain it needs, and what a passing run prints. A finding whose result cannot be re-derived from a public clone does not get a page. |
Two kinds of result
The findings index is split, and the split is load bearing. A theorem about an artifact built to have a property is a demonstration of what is constructible, not a discovery about an existing system. Both are worth stating; they are not the same kind of claim, and collapsing them would let a demonstration read as a measurement of the world.
- Results about existing systems. The object was not built by this programme. A library that does not round trip its numbers, or two off-the-shelf judges that disagree with the truth in opposite directions.
- Demonstrations of what is constructible. The object was built to have the property, and the result shows the property can be established at all. A bound proved over every interleaving says what is buildable, not what deployed systems do.
Ordering, and pre-registration
Where an analysis was fixed before the data existed, the ordering is carried by the commit history rather than asserted in the write-up. The pre-registration record holds the registration, its two amendments and a deviations log that records every departure from the registered plan together with its timing, including the departures that weaken a result.
One boundary in that record generalises to everything here: recomputation from committed traces checks arithmetic, and does not check the instrumentation that produced those traces. A number that re-derives is not thereby an independently validated number.
Where a check has no instance
Where a check has no grounded instance, that is stated rather than filled with a borrowed one. The failure taxonomy names one mechanism with no instance at all, and labels it as such rather than dropping it or illustrating it with someone else's example. The open problems are listed for the same reason.
The wording rules these grades sit inside are on the About page.