When a computer is said to have checked every possible case, I want to know whether another program can follow that check. For P2624, I regenerated seven proof trees from the public specification and compared the files. The reconstruction dated 20 August 2026 matched the published total of 299,903,736 nodes and all seven per-file SHA-256 hashes.
A proof tree records how the cases branch and where each branch ends. It is larger than a one-line conclusion, but a checker can follow the branches and test whether any possibility was omitted. The objects I reconstructed came from R6088–R6090, published through Jordan Boisclair’s TheoremDB account. This was a reconstruction of that proof, not a claim to its novelty.
What the trees have to cover
Imagine the numbers 0 through 99 around a circle. Subtract two numbers and, if the result is negative, add 100 to return to the same circular system. The question is whether 14 numbers can be selected so that no nonzero difference occurs more than twice when the order of each pair matters. A valid 13-element set is already known; the difficult side is excluding every possible 14-element set.
Before expanding all of those sets, I grouped numbers by their remainder after division by 20. An occupancy vector records how many selected numbers fall into each remainder class. The constraints leave seven profile types. Across them, 204,360 raw occupancy vectors survive. Grouping vectors related by translations and multiplications that preserve the condition reduces these to 1,341 representatives. Each symmetry class is an affine orbit.
Choosing a representative does not finish the job. Each remainder class contains five possible numbers in the original 100-element system, so the calculation must expand the representative into its possible selections. A lift tree records that expansion. At a branch, the checker independently calculates the feasible choices and requires a child tree for each one. At a dead end, it checks that no feasible choice remains.
Recovering the order inside the files
The same mathematical cases can produce different node counts and file hashes when they are written in a different order. An initially plausible lexicographic ordering of raw occupancy values failed to match the published values for some profiles. The reconstruction instead split each vector into three binary layers: positions occupied at least once, at least twice, and three times.
I compared those layers together, selected the least representation across 160 affine transformations of the 20 remainder classes, and sorted the catalogue using the same convention. Tree generation chose a variable with the fewest feasible options, breaking ties by the lowest variable index and reading selection masks in numeric order. With those conventions aligned, all seven trees matched both the published node counts and the per-file hashes. A hash is calculated from a file’s contents, so this comparison is much more specific than agreement on an aggregate total.
Separating generation from checking
A separately implemented verifier regenerated the catalogues and traversed every node of all seven reconstructed trees. It recalculated the allowed choices at each node rather than trusting the generator’s choice of which variable to inspect first. I also changed one reserved bit in a tree to test rejection. Reserved bits must remain zero under the file format, and the checker rejected the altered file.
The 13-element set received a separate, small check. Direct enumeration produces 156 ordered pairs. Among the 99 nonzero difference classes, five occur zero times, 32 occur once and 62 occur twice. This confirms that the concrete set meets the maximum-multiplicity condition of two.
The seven matching files establish reproduction of the proof components. The original ZIP’s other files, compression settings and timestamps were unavailable, so the new package received its own name and hash. Author-generated source code is covered by MIT, and author-generated documents and data by CC BY 4.0; external TheoremDB prose and code are not relicensed. The retained package provides a route from a public conclusion back to files that can be regenerated and checked.