Devlog #31 - Proving Par: 230 Levels With Exactly One Best Answer

Every one of Fourfold's 230 boards has a shortest solution, and that shortest solution is unique. Not "we could not find a better one". Proved, per board, on every build.

This devlog is about why that was possible at all, because when we scoped it we assumed it would be the thing that killed the project.

The problem

A Fourfold level is a start board S, a target board T, and a number k - par. To ship it you need two facts:

1. The minimum number of taps taking S to T is exactly k.
2. There is only one way to do it in k.

Fact 2 is what makes the game honest. If two different tap sets both hit par, then "the best answer" is a lie and the puzzle has no single right solution - which quietly undermines every hint, every star rating and the entire Journal.

Both facts look like search problems. Search the space of tap sets, find the smallest, check nothing else matches it. On a 30×30 board the space is astronomically large. That is normally where this kind of pipeline dies.

Why it isn't a search

Here is the part that makes the whole game feasible.

A solution is not really a sequence of taps - by Dhar's abelian property, order does not matter, so a solution is just a count per cell: how many times each cell was tapped. Call that vector x. The board arithmetic then says T = S + Δx for the graph Laplacian Δ, over the integers, subject to the result staying legal.

The useful structure is this: the set of feasible topple-count vectors is closed under componentwise minimum. If x works and y works, then the vector taking the smaller of the two at every cell also works.

That is a strong property. A set closed under componentwise min, and bounded below, has a unique least element - take the min of everything in it. And because taps are counted with non-negative weights, the least element is also the one with the smallest total. So the minimum is not something you search for. It is something you compute, directly, by driving each coordinate down until it cannot move - the same shape of computation as Dhar's burning test.

Par comes out exactly, first try, in near-linear time.

Uniqueness follows from the same object. Once you have the least element, another distinct solution of the same total size would have to disagree somewhere while not being reducible - and closure under min rules that out unless the disagreement itself forms a valid alternative, which reduces to a set closure you can test directly rather than enumerate.

The derivation is written out properly in core/solver.ts. It is about forty lines of code and it is the reason this game exists.

What that bought us

The whole 230-level campaign regenerates and re-verifies in well under a second. Generation is: build a random recurrent board S (start from the maximal stable board and add grains, which keeps it recurrent), apply k taps to get T (which stays recurrent), then prove the minimum from S to T is exactly k and unique. Reject otherwise.

Because step three is cheap, the reject rate does not matter. We can afford to be fussy about difficulty curve, board topology and visual legibility, and throw away everything that does not qualify.

It also means the daily board can be generated on a phone. No server, no content delivery, no "today's puzzle failed to download". The generator and the PRNG are bit-identical between the TypeScript and Kotlin implementations, and the engine test suite pins that to a fixture - so a player on Android and a player in a browser get the same board on the same date with nothing fetched by either.

Verified, not asserted

Four claims, four tests, run on every push:

93 engine tests. If any of them go red, the level pack does not ship - the Pages deploy runs verify before it runs the build, so a pack that has not been re-proved cannot reach production.

That last table is also, roughly, the design document. Which is the point.