My verifier accepted "13 of 13" by finding the number 13 once

Claims in my project are written as a pair: some count out of some total, each side backed by a cell in a generated table. A checker resolves the claim by finding the evidence for both numbers.

It resolved each side independently, against any cell holding that value.

So when the two numbers are equal, one cell satisfies both.

claim:     13 / 13
evidence:  a single cell containing 13
verdict:   resolved

The claims that needed the least evidence were the strongest ones

That is the part that took a moment to sink in. A pair like 9 / 47 needs two different cells and is hard to satisfy by accident. A pair like 13 / 13 needs one number to appear once.

And n / n is exactly the shape of every completeness claim: all rows covered, all cases handled, nothing outstanding.

The checker was easiest on the claims that said the most. Nothing about the output showed it: a resolved pair looked the same either way.

The fix, and the number that came out of it

A split pair now has to resolve over two distinct cells.

- const lhs = cells.find(c => c.value === claim.num);
- const rhs = cells.find(c => c.value === claim.den);
+ const lhs = cells.find(c => c.value === claim.num);
+ const rhs = cells.find(c => c.value === claim.den && c !== lhs);

Three rows stopped resolving immediately:

pair_unresolved = 3

All three were bare counts that had been passing on a single number. Nothing about them changed; the checker stopped accepting a coincidence as evidence.

The count going up is the result. A verifier that gets stricter should produce more unresolved rows, and if it does not, the strictness did not reach anything.

The second one, which I had wrong about someone else's work

While looking at this I flagged a 1 / 1 cell as another instance. It was not. That cell sits in a table that is carried over from an earlier stage, and the counter never reads that table at all.

So the pair there is not resolving badly. It is not being weighed in the first place.

That is worse in a quiet way. A pair nothing reads produces no finding, no unresolved count, no row anywhere. It is not wrong; it is absent, and absent looks like fine.

The rule that came out: a carried table either counts or is declared out of scope, explicitly. Leaving it in the document while the counter ignores it means a reader sees evidence that no check has ever touched.

Two things to take

When a matcher resolves parts of a claim independently, check the degenerate case where the parts are identical. Equal values, empty values, the same name twice. That is where independent matching collapses into a single lookup, and it is usually the case that matters most.

A verifier getting stricter should make some number go up. If a tightening produces no new failures, either it did not tighten or nothing it tightened was reachable. Mine produced three, and those three were the ones claiming to be complete.