A 43-vertex 4-chromatic unit-distance graph in the plane with girth 5

We exhibit a set of 43 points in the Euclidean plane whose unit-distance graph has 83 edges, girth 5 and chromatic number 4. The smallest previously known 4-chromatic unit-distance graph of girth 5, due to Hochberg and O'Donnell (1996), has 45 vertices. The new graph is 4-critical, has trivial automorphism group and exactly 2n−3 edges; it is a Laman graph and its unit-distance realisation is infinitesimally rigid. The coordinates are algebraic numbers, specified as the unique real solution of an explicit system of 82 quadratic equations inside an explicit rational box. Existence and uniqueness of the realisation are certified by an exact rational contraction-mapping certificate (independently re-checked with interval Krawczyk arithmetic). Non-3-colourability is certified by exhaustive search and by a DRAT proof verified with drat-trim. Files: the preprint (PDF) and a supplementary archive. The archive contains the edge list, the exact polynomial system and rational isolating box, the certificate, the criticality witnesses, the CNF formula and DRAT proof, two independent verification scripts, and the LaTeX sources.