Counting the Fixed Points of Binary Belief Propagation: Generic Degree, Syzygies, and Real Solutions
Yusuke Watanabe
math.AC
Oct 27, 2026 · v1
cs.IT math.AG math.CO
TL;DR
Main theorems on the generic BP degree, edge-incidence ring resolutions, and minimum real fixed-point counts are formalized in Lean 4 with Mathlib, with Lean source released.
Abstract
How many fixed points does belief propagation have on a binary pairwise model? Over complex parameters, the admissible equations of a finite loopless multigraph form an algebraic family whose generic degree we determine: it is a graph state sum over edge sets without vertices of degree one, each vertex of positive degree contributing one less than its degree. We give two geometric realizations of this state sum. The first is the total Betti number of a universal edge-incidence ring constructed without parameters. Its full graded Betti table is the state sum, its Tor algebra is natural for noncontracting graph maps, the alternating numerator recovers the graph polynomial of Watanabe and Fukumizu, and an Artin reduction by a regular sequence realizes the one-variable specialization, corrected for tree components. The second lies in the actual family: at the strong-field boundary each state factor is a ramification index, and at sufficiently strong field the state charts exhaust the admissible complex fiber. For fixed nonzero real couplings, every Eulerian message-sign sector contains a real fixed point at every external field, and strong fields attain this lower bound: one admissible real fixed point per element of the binary cycle space and one positive fixed point. For graphs of maximum degree at most three, this minimum equals the number of minimal module generators of the edge-incidence ring. One state decomposition connects the complex degree, graded syzygies, and an attained minimum real count. The degree, selected ring and resolution statements, and the real counts are formalized in Lean 4.
Problem
The question is how many fixed points belief propagation has on a binary pairwise model over a finite loopless multigraph. Two cases are considered: generic complex parameters and fixed real couplings.
Approach
The generic degree is expressed as a graph state sum over edge sets with no degree-one vertices. This sum is realized in two ways: as the total Betti number of a parameter-free edge-incidence ring, computed via the geometric syzygy method on products of projective lines, and as ramification indices at the strong-field boundary of the BP family. Real solutions are analyzed through Eulerian message-sign sectors using a maximum principle for vertex ratios. The main theorems are formalized in Lean 4 with Mathlib through explicit chart, biproduct and Čech models.
Results
The generic number of admissible complex fixed points equals the state sum Q(G), which is also the full graded Betti table of the ring. For fixed nonzero real couplings, the minimum real count over external fields is 2^ν(G), with exactly one positive fixed point. For maximum degree at most three, this minimum equals the number of minimal module generators of the ring.
