The hardest instance of PCP(w): Zhao's table, the value 12 at w=7, and the extremal subclass at w=10

Abstract

PCP(w) is the set of Post correspondence instances with two tiles, each tile a pair of nonempty binary words of length at most w. Ling Zhao's 2002 search tabulated, for w ≤ 6, the largest shortest-solution length over the class — the values 2,4,6,8,10 — and recorded Lorentz's conjecture that the maximum is always attained by the instance (1ⁿ0 / 1), (1 / 01ⁿ) with n=w-1, whose optimum is 2n=2w-2. We prove that this family has shortest solution exactly 2w-2 at every width and that its optimal solution is unique; we turn two of the three unsolvability filter types Zhao attributes to Lorentz, and a divisibility law for solution lengths, into theorems; we make every cell of Zhao's published table an exhaustive theorem inside a fixed depth window; we exhibit an instance of PCP(7) whose shortest solution has length exactly 12, the value the conjecture predicts at the first width Zhao did not compute; and we settle the conjecture, inside that same depth window, on the extremal subclass — both tiles maximally imbalanced, which is where the conjectured maximiser lives — for every w ≤ 10, one width beyond every exhaustive computation over the full class that we know of. Lorentz's conjecture itself remains open. Every theorem and proposition below is machine-checked in Lean 4; the two upper bounds that are not — the full class at w=7,8,9, and the extremal subclass at w=11 — are labelled as external computations where they appear.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-08-30 15:34 UTC

   File fingerprint

   31607ffc340965f057af3ed2e81dd24522a4a8eea79c1fae4c988531543762a9