Solid Grid Graph

A solid grid graph is a connected graph obtained from a nonempty finite set in the integer lattice by joining exactly the pairs of vertices at distance 1, such that every bounded graph face in the natural planar graph embedding is a unit square. Thus the graph has no holes. The grid graph is a rectangular example, but the boundary of a solid grid graph need not be rectangular (Itai et al. 1982, Sheffield 2001).

Every solid grid graph is a simple graph, a planar graph, and a bipartite graph, with maximum vertex degree at most 4. A bipartition is given by the parity of the coordinate sum. Solidity does not imply the existence of a Hamiltonian cycle or a Hamiltonian path. For example, the star graph is solid but has neither.

The Hamiltonian cycle problem for solid grid graphs has a polynomial time algorithm. Sheffield (2001) gives a quadratic algorithm and states that similar results hold for Hamiltonian paths with fixed endpoints. In contrast, deciding the existence of a Hamiltonian path in a general finite induced subgraph of the integer lattice, with unit-distance edges, is NP-complete (Itai et al. 1982).

Zzyzek (2026) reported a polynomial time algorithm deciding whether a solid grid graph has a Hamiltonian path between two specified distinct vertices, together with a Lean formalization of correctness and the cost bound

where is the vertex count and is a separately defined cost function that assigns constant cost to basic finite-set operations. Its correspondence with the algorithm is checked by inspection, and the bound is not a Turing-machine running-time bound. The formal no-hole condition uses connectivity of missing lattice points by king moves. Its equivalence to the bounded-face definition had been checked computationally rather than proved in Lean. The author credits Claude Opus 5.5 with the mathematical argument, algorithm, and formalization. As of Oct. 27, 2026, independent specialist verification of the complete result had not been reported.