Verification · epistemics · the edge of the evidence

The Case Nobody Ran

A test can only ever check finitely many cases. A law is a claim about all of them. Somewhere in every check there is a number that says where the running stopped, and past it is the case nobody ran. This is a census of every one of those numbers in this corpus: … hard-stopped exhaustions across … files of evidence, found by parsing rather than reading, classified by two readers who could not see each other, then deleted and re-run one case further to find out whether the check would even notice.

Past the Last Case argues this gap and walks seven layers that close it with proofs. It is an argument. Nothing here had ever measured the gap, and an argument about honesty that declines to measure itself is the cheapest kind. So: where does this ground actually stop checking, does it say so, and would it notice if the checking never happened?

I · Where the counting stops

The object is not a sentence and not a claim. It is a counted loop with a hard-coded bound whose result something asserts. That is syntax, so it can be found exactly rather than recognised approximately, and its bound is a literal at a known byte offset, so it can be moved and put back. Everything below hangs off that one object.

The sweep parses … files (… MB) of offline checks, engines and served page scripts with a real parser, not a grep, and finds … counted loops. Most of them are machinery. … have a result that something asserts, and after dropping loops nested inside other loops and loops that draw randomness (a sample is a different kind of evidence from an exhaustion, and mixing them would be this census's first lie), … remain. That is the population.

Where the bounds fall

Every classified loop, by the size of the number where it stops. Colour is what that number means, which is the next section.

II · Four kinds of stopping

A bound can mean four quite different things, and telling them apart is the entire census.

• complete: the domain ends where the loop ends. for (let d = 0; d < 365; d++) over the days of a year is not a window into anything. It is the year.
• window: the domain runs past the bound. for (let n = 1; n <= 10000; n++) checking a property of the integers leaves everything past 10,000 unchecked, and the claim it supports is usually stated without a bound. There are … of these, and they are what the census is about.
• resolution: a grid across a continuum. A sweep of the visible spectrum from 380 nm to 700 nm in quarter-nanometre steps covers the domain end to end. What it misses lies between the samples, not past the last one, and it is closed by refining rather than by extending.
• fixture: no domain at all. A fixed list of cases, a trial count, a solver's iteration budget.

Two readers classified all … loops, and neither could see the other's answers. They worked from one published rule (research/unrun-census/CLASSIFY.md, with the hard cases ruled in advance) and from the source around each loop. They agree on … of …, which is …, or … as Cohen's κ once you subtract the agreement two readers with these habits would reach by chance. Where they differ the loop is contested and stays out of every headline below. Nothing is settled by preferring one reader: a population assembled by overruling your own instrument measures which instrument you preferred.

III · Delete the exhaustion

Now the part that can be run rather than argued. For every loop in a file that node can execute on its own, the census runs the file three times inside a throwaway git worktree, editing one literal at a recorded byte offset and restoring the original bytes afterwards with a hash comparison.

• BASE: the file as committed. If it is not green, nothing else about it is measurable.
• EMPTY: the same file with the bound set so the loop runs zero times.
• PUSH: the bound advanced by exactly one step. The first case past the last case anybody ran.

EMPTY is the control, and it is the only reason PUSH means anything. If a check is still green with the exhaustion deleted, then its verdict does not depend on the exhaustion, and a green PUSH from that file tells you nothing about the claim. The accumulate-then-judge style makes this failure easy to fall into without noticing: an empty loop leaves bad at zero, and ok('holds', bad===0) passes on the strength of having looked at nothing.

… of the … stopping points were run this way, across … files. The rest are out of reach of this arm rather than skipped: their checks run in a browser, their file is not a script node can run on its own, their bound is not a plain literal, or the file was not green to begin with. Deleting the exhaustion produced three outcomes:

… of the exhaustions that were run can be deleted outright with no visible effect at all: same exit code, same number of checks reported. Another … are vacuous: the printed tally drops, so a person reading the output would see it, but the exit code, which is what a build gate reads, stays green. Only … turn the check red when the exhaustion is removed. Those are the loops whose result genuinely reaches a verdict.

This is a fact about how the checks are wired, not about whether the claims are true. A vacuous pass is the oldest bug in testing and it is not evidence of anything false. It is evidence that on those files a green check cannot distinguish the law holds from nobody looked, which is the distinction the check exists to make.

IV · One more case

Then the bound moves by one step and the file runs again. Of the … loops whose deletion the check does notice, one more case gave:

A red is not a finding by itself. It has six possible causes and only one of them would be a discovery, so every red was read by opening the source, under a rule written down before the reading (research/unrun-census/REDCAUSE.md), never inferred from the failure text. … of … reds were read this way:

Welded is the interesting category, and it was not one I expected to need. A welded check writes its own expected value in terms of the bound: for (n=1;n<=64;n++) sum += 1/2^n; ok(sum === 1 - 1/2**64). The exhaustion genuinely reaches the verdict, which is why these survive the deletion control, but the window cannot be widened by moving one number, because the constant would have to move with it. A welded check is honest and immovable at the same time.

And the most common reason a check stops where it does turns out not to be cost. It is the catalogue: a loop comparing against a published table of twenty terms stops at twenty because the table stops at twenty, and the integers do not.

V · Does the page say where it stopped?

This is the only arm about a reader rather than about code. A layer that says "checked for every n up to 10,000" has told the truth about its own reach. A layer that says "for every n" and stops at 10,000 has not, whether or not the law is true, because the reader cannot tell a proof from a patience.

The test is mechanical and deliberately weak: does the bound appear anywhere in the layer's published prose, in any of the forms people write a number? That would pass a page that mentions 10,000 about something else entirely, so it is calibrated. Every bound is also matched as a decoy of the same size that the layer never claimed, and the decoy's hit rate is how often this test says yes by accident. Only the gap between the two means anything, and both are printed so neither can be quoted alone.

So on the order of half the windows carry their own edge somewhere in the layer's prose, against a chance floor near ten per cent. The other half do not, with one narrowing worth stating plainly: the test reads sentences, not tables, headings or code, because a results table is apparatus rather than an assertion. A bound that appears only in a printed table therefore counts as unstated here. That makes this arm's unflattering half a little too large, and it is why the decoy is matched exactly the same way: whatever the narrowing costs, it costs both rates equally, and only the gap between them is being claimed.

VI · One window closed

A census that only counts is half a gesture, so one window from the list was taken and shut. The Floor That Won't Lie Flat states two claims about all regular tilings {p,q}: that the five spherical ones are the Platonic solids, and that there are exactly three flat ones, {3,6}, {4,4}, {6,3}, and no others. Both were settled by a double loop over p and q from 3 to 12, with a second sweep to 20. Both loops are honest and both stop.

A loop can show a list is long enough. It can never show a list is finished, because the case that would break it is the case nobody ran. research/hyperbolic-tiling/lean/SchlafliTrichotomy.lean now proves both, for every p ≥ 3 and every q ≥ 3 at once, in Lean 4 with zero imports, so the only trusted component is Lean's type-checker.

Write p = a+3 and q = b+3 and the whole trichotomy collapses onto one quantity, D = ab + a + b, against 3. If a and b are both at least 1 then ab ≥ 1 and D ≥ 3 already, so any spherical or flat case forces one of them to zero, and with one of them zero D is just the other. Five cases and three cases, with nothing left to search. A third theorem, hyperbolic_infinite, proves the remaining class never ends, which is the fact a bounded double loop is structurally unable to notice: no bound on p and q was ever going to be the whole picture.

Two smaller theorems say something about the loop itself. defect_eq and defect_link show that the two expressions the sweep compares a hundred times, sign(1/p + 1/q − 1/2) and sign(4 − (p−2)(q−2)), are not two quantities that agree. They are one quantity written twice. The loop was re-checking an identity, which is why it never found a disagreement and never could.

Every theorem's axiom footprint is [propext, Quot.sound]: no sorry, no Classical.choice, no native_decide. Getting there cost two lessons, both found by reading the footprint rather than by thinking. A full simp pulls in Classical.choice; so, less obviously, does omega on an ↔ goal or an ∧ goal, while the identical arithmetic split into halves first does not.

VII · Every stopping point in the ground

The list is the showing. Every classified loop, with what it counts over, the claim its assertion supports, whether the layer's prose states the bound, and what the three runs did. Search a file name, a subject, a number.

…

VIII · What this does not establish

• Nothing here says a claim is false. The census locates the edge of the evidence. That is a different and much smaller thing than settling a law, and it is the only thing a sweep can honestly do.
• Checks that run in a browser are counted but never pushed. A loop inside a served page is scanned and classified, but its check is driven by a headless browser rather than by node, so the three-run experiment does not reach it.
• Bounds that are not literals are invisible. A loop stopping at LIMIT or at data.length has a stopping point this instrument cannot locate, and there is no estimate here of how many of those there are. while loops and recursion are the same gap, also unscanned.
• The "does the page say so" test is weak by design. It cannot tell whether the number it found is attached to the right claim. The decoy arm prices that weakness rather than removing it.
• The classification is two readings, not a truth. The agreement and κ are printed above precisely so the residue is visible; both passes are committed under research/unrun-census/classify/ and can be disagreed with line by line.
• A green PUSH is one case, not a proof. It says the very next case holds. The whole point of the section above it is that this is not the same as a law.