发表机构
Institute of Software, Chinese Academy of Sciences; University of Regensburg（中国科学院软件研究所; 雷根斯堡大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文为带非负权重的平面图同态计数问题建立了完整复杂性二分法，并刻画了保持可处理性的顶点权重，通过熵延拓和距离几何证明，所有结果已在 Lean 4 中形式化验证。
AI 中文摘要
我们证明了对于任意固定阶数的对称非负矩阵，平面图同态计数问题具有完整的复杂性二分法，并给出了可处理性的明确判据。我们还精确刻画了哪些固定的正顶点权重保持可处理性，这两个分类都从代数权重扩展到指定精确表示中的固定实数权重。我们的证明基于一个熵驱动的延拓论证：最大对数支持将距离核识别为最大熵完备化，从而将其正定性推广到整个参数区间。这使得距离几何能够在平面小工具无法区分颜色时恢复隐藏的乘积坐标；计数困难性论证则迫使因子为零场布尔伊辛相互作用。该分类还为时钟模型、耦合伊辛系统以及随机虚时核的平面收缩提供了完整的可处理性判据。所有结果已在 Lean 4 中正式验证。
英文摘要
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.
Comments29 pages. Lean 4 formalization: https://github.com/liuchliuch/planar-homomorphisms-lean
