The Order Is the Claim

A sort returns exactly the numbers it was given. Every last one of them, unchanged. So a ranking asserts nothing at all with its values and everything with its arrangement, and a check that reads a number off the screen and finds it correct has, in the strictest sense, checked nothing about the ranking. Break the table below without touching a digit, and watch which of five checks notices.

Yesterday this site changed the last digit of every number 763 of its pages render and re-ran their own checks. Around five in six stayed green, but of the checks that actually drive a browser, around seven in eight noticed, which reads as reassurance. It was measured with a mutation that moves digits. This page moves no digits.

Companion film · Nothing Was Taken Away · 3:30 · sound on. A film is 5,040 frames in one arrangement and its soundtrack is 9,261,000 samples per channel in one arrangement. Both hold their whole content in an order and neither loses anything at all when that order is reversed, which is this page's thesis with the deliverable standing in for the ranking. So the film does not illustrate a reversal, it commits one on itself. Eight seconds in the middle are exactly their own reverse: the gate hashes the rendered frames and requires all 95 pairs either side of the centre to be byte for byte the same frame, and cuts the same eight seconds out of the finished soundtrack and requires s[i] = s[n-1-i] at every sample. Both come back exact. The clock along the bottom of the frame is switched off across the span, because a monotone clock is the one thing a palindrome cannot carry, and the film says that on screen rather than hiding the removal.

The soundtrack is this page's argument in one stated constant: pitch is the divisor count, 110 Hz at nought divisors and a whole tone for each one after. Nothing else about a row is audible, so the instrument has exactly the sensitivity the claim has. Ranked as claimed, the divisor column never rises and neither does the line; rendered bottom to top it is the same twenty-four notes and never falls; and permuted only inside blocks of equal d, where this page never said which row comes first, it is not merely similar but sample-identical, at a difference of zero. Then the pairing the film runs on: all twenty-four pitches struck together is a chord, which is a multiset with no order in it whatever, and the same six seconds played backwards has the same magnitude spectrum to about a hundred-billionth of its peak, because reversing a real sequence conjugates its transform and moves only the phase. A chord is to a sound what the permutation check is to this ranking: a correct reading of the half a reversal cannot touch.

Every figure on screen is derived rather than typed, from this page's own engine.js, this page's results block and the committed run records; not one digit is written into a caption. The build's gate (research/the-order-is-the-claim/film/film-facts.mjs, 66 checks) measures every audible claim off the finished soundtrack with a negative control beside it, and check-encoded.mjs measures them again out of the compressed audio the file ships with, where the exact sample equalities become approximate and it prints how far the codec moved them rather than quietly measuring the lossless copy.

A ranking, and seven ways to be wrong about it

Below is every integer from 2 to 200, ranked by how many divisors it has, most first. That is the page's whole claim, stated in those words and no others. Five checks watch the table. Pick a defect and see who moves.

size of the ranking

defect in the engine (the screen faithfully shows what was computed)

defect in the display only (the engine is right, the screen is not)

rank	n	d(n)

showing the first 14 of 0 rows; the checks run on all of them.

Three of those seven defects are in the engine and four are only in the display, and the distinction matters more than it looks. When the engine is wrong the screen is honest: it shows you, faithfully, a false answer. A check that compares the screen against the engine sees nothing wrong, because there is nothing wrong between them. That asymmetry has a shipped companion here, The Engine and the Eye, which measured it on the value axis. This is the same asymmetry on the arrangement axis.

All of it at once

Every defect against every check, computed in your browser as this page loaded. Nothing below is a picture of a result. It is the result.

Rows in red are defects that make the page lie about its stated claim. Rows in green change the arrangement without contradicting anything the page said, because the page claims a ranking by divisor count and says nothing about which of two equal rows comes first. A red light on a green row is a check asserting more than the page ever promised.

The two halves of correct

The standard correctness condition for a sorting routine has two clauses, and the reason it has two is that either one alone is trivially satisfiable. A routine that returns a list of zeroes is perfectly sorted. A routine that returns its input untouched is perfectly a permutation of it. Only together do they say anything, and this is why sorting is the example every proof-assistant tutorial reaches for: it is the smallest program whose specification people reliably write down by half.

The bench above is that fact made operable. The permutation check is green on every row of the truth table, including all of the ones where the page is lying to you, and it is not a badly written check. It is a correctly written check of the half of the specification that the arrangement defects cannot touch. The failure is not in how carefully it was written but in what it was pointed at.

What makes this worth more than a lesson in sorting is that the same split runs through almost every check anyone writes about a rendered page. A readout, a total, a label, a count: those are values, and a check that reads them is checking the half that a permuted list leaves entirely intact.

So we went and measured our own

On 12 August every page on this site was loaded in a browser with a script that changed the last digit of every number the page wrote, and each page's own checks were re-run against it. Exactly 108 of them went red: those checks had demonstrated, under the easiest possible version of the defect, that they can see what a page puts in front of a reader.

That population is the whole of this experiment. Not a sample, not a selection, not a set of pages that looked promising. The 108 pairs of check and page that the previous run had already proved were watching the screen. The question asked of them is the one the digit probe could not ask: not can you see the screen, but can you see what the screen means.

The mutation is a probe injected as the first thing in the document, patching every path by which a script puts an element into the page, so that each element lands at the other end of its parent. A loop that appends rows renders them backwards. Nothing else changes: not a digit, not a label, not a class, not an attribute, and not which value sits beside which name. The placebo is the same script at the same place with one byte different.

And a second question had to be answered before the first one could mean anything, because reversing a list is only a lie where the order was a claim. A row of filter chips is not ranked; neither is a grid of cells. So a third probe mode records which containers the permutation would move and moves nothing, and the true page is then walked to ask, of exactly those containers, whether their arrangement is measurably a claim: three or more children of one tag, none of them a control a reader operates, with some column of numbers monotone and not constant, or their text in alphabetical order. Most are not. That is the honest reason the narrow figure below is smaller than the wide one, and the narrow one is the answer.

That test errs in both directions and the limits below say by how much, because an adversarial audit of this page on the night it shipped found it doing so. It had been described in exactly the words above and implemented without the one-tag clause, which let fourteen containers through that the description never admitted; and the promise about controls was a promise, not a line of code, so rows of buttons and lists of dropdown options were being counted as rankings. Both are enforced now. What cannot be enforced is the other direction: a list ordered by editorial judgement, or by any quantity the page never prints, reads as unordered to any test of this kind, and the repair described further down turned up precisely that case.

What we cannot say from this

Two of them fixed the same night, and proved fixed

A sentence claiming a fix is cheap, so the two blind layers whose pages put the most ordered arrangement in front of the probe were each given a family that reads the rendered sequence, and both were then put back under the permutation on their own. The Encoding Your Text File Admits To ranks seven analyser candidates by score, reproduces Unicode's Table 3-7 in the order the standard prints it, and its check asserted every one of those values and none of those orders. Hostage Sublime walks a curated list of layers and ends, deliberately, on itself; reversed, it opened on itself instead. Both now go red under the permutation and green under the placebo, recorded in order-fix1.json and order-fix2.json, and their verdict in the sweep above is left as it was measured, because the sweep is a photograph of the corpus before the repair and not after it.

One thing the repair turned up that the aggregate cannot. The probe reverses cells inside a row as well as rows inside a table, so the assertion that caught it read the score column arriving in the rank column's position and running bottom to top at the same time. Any check that reaches a cell by its position is exposed twice over, and the second exposure has nothing to do with sorting.

Check it

The bench on this page is engine.js next to this file, imported by the page and by its verifier so there is only one copy. Every figure the corpus section prints, in its data block and in its sentences alike, is written there by fill-order-page.mjs and re-derived from the committed run records by verify-the-order-is-the-claim.mjs, which also drives this page in a browser, sets each defect, and requires the five lights to answer the way the truth table above says they will. The page's central claim is falsifiable by the page's own check.

# the instrument must pass its own control before any number it produces is read
node research/verifier-independence/order-control.mjs

# the sweep, over the population the previous experiment defined
node research/verifier-independence/order.mjs --shard 0 --of 3 --out order-0.json

# this page
node verify-the-order-is-the-claim.mjs

The control is not a formality. It builds a page with two tables, one assembled by appendChild and one by an innerHTML join, and requires that under the permutation a value check stays green and an order check goes red. The first time it ran it failed on the second table: the probe was reversing its own scratch buffer and then reversing it back, a perfect silent no-op that would have read, page after page, as a corpus with nothing to permute. That is what a control is for.