Graceful 4-coloring of planar graphs is NP-complete

A graceful $k$-coloring of a graph is a proper vertex coloring with colors $1,\dots,k$ such that, at every vertex, the incident edges receive distinct differences of their endpoint colors. Cyriac Antony, Laavanya D. and Devi Yamini S. proved that deciding graceful $k$-colorability is NP-complete for planar graphs when $k\ge 5$, and for $k=4$ on graphs of maximum degree three, and they left open the complexity of graceful 4-colorability of planar graphs. We prove that this problem is NP-complete, even for planar graphs of maximum degree three (inputs, as in their formulation, may be disconnected). The hardness comes from the reduction of Édouard Bonnet, Dibyayan Chakraborty and Julien Duron, who proved that deciding whether a cubic planar graph has a perfect matching cut (a perfect matching that is exactly the set of edges leaving some vertex set) is NP-hard; we apply their construction to every instance. What we add is an exact correspondence: for every finite cubic graph $H$, the graph obtained by subdividing each edge of $H$ twice has a graceful 4-coloring if and only if $H$ has a perfect matching cut. This equivalence is proved in Lean from the definitions. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Written proof, with Lean and computer checks; not yet reviewed by experts. Produced by AI models under the author's direction.