A Dichotomy for Planar Graph Homomorphisms with Nonnegative Weights
Chenghua Liu, Boning Meng
cs.CC
Oct 4, 2026 · v1
TL;DR
The complexity dichotomy for planar graph homomorphism counting and all supporting results are stated to be formally verified in Lean 4.
Abstract
We prove a complete complexity dichotomy for planar graph homomorphism counting with any fixed symmetric nonnegative matrix of arbitrary finite order, giving an explicit criterion for tractability. We also characterize exactly which fixed positive vertex weights preserve tractability, with both classifications extending from algebraic weights to fixed real weights in a prescribed exact representation. Our proof hinges on an entropy-based continuation argument: maximal logarithmic support identifies distance kernels as maximum-entropy completions, extending their positive definiteness throughout the parameter interval. This enables distance geometry to recover hidden product coordinates even when planar gadgets cannot distinguish colors; counting-hardness arguments then force the factors to be zero-field Boolean Ising interactions. The classification also yields complete tractability criteria for clock models, coupled Ising systems, and planar contractions of stoquastic imaginary-time kernels. All results have been formally verified in Lean 4.
Problem
The question is which fixed symmetric nonnegative matrices make planar graph homomorphism counting (planar spin partition functions) tractable. A second question is which fixed positive vertex weights preserve that tractability.
Approach
An entropy-based continuation argument uses maximal logarithmic support to identify distance kernels as maximum-entropy completions, which keeps them positive definite across a parameter interval. Distance geometry then recovers hidden product coordinates. Counting-hardness reductions using planar gadgets and interpolation force the factors to be zero-field Boolean Ising interactions. The results extend from algebraic weights to fixed real weights in an exact field representation, and are reported as formally verified in Lean 4.
Results
Planar homomorphism counting is tractable exactly when the interaction decomposes into independent zero-field Ising coordinates, up to elementary local summations; otherwise it is #P-hard. The admissible vertex weights are characterized exactly. Consequences include tractability criteria for clock models, coupled Ising systems, and planar contractions of stoquastic imaginary-time kernels.
