← All papers
First page of Coefficientwise Extremality and Rigidity for Independent Sets in Bipartite Graph Covers

Coefficientwise Extremality and Rigidity for Independent Sets in Bipartite Graph Covers

Yusuke Watanabe

math.CO Oct 10, 2026 · v1 cs.DM
All clauses of the main theorems (A–C) on independent sets in bipartite graph covers are formalized in Lean 4 with Mathlib, with a public repository.
Let $G$ be a finite bipartite graph and let $\widetilde G$ be an $M$-fold cover. We compare independent sets of $\widetilde G$ with those of the trivial cover, consisting of $M$ disjoint copies of $G$, after prescribing how many vertices are selected above each vertex of $G$. A conjecture from 2011, motivated by the Bethe approximation, asserts that the trivial cover maximizes every such count. We prove this for every feasible occupation profile whose active graph has treewidth at most two or is chordal bipartite. Equality holds exactly when the restricted cover is flat, meaning that fibre relabelings make it trivial. For $M\ge2$ and positive feasible occupations, a nonflat cover of a connected bipartite graph of treewidth at most two has a deficit of at least twice the coefficient of $p_G^{M-2}$ with every occupation reduced by one. A holonomy-dependent bound improves the factor to three for odd-order holonomy; both uniform constants are sharp. Comparison and rigidity survive finite compositions along an edge or a vertex, and quantitative bounds from one piece propagate to the whole graph, giving results beyond the two original classes. On any bipartite base, the first nonzero homogeneous defect is determined by the shortest cycles with nontrivial holonomy. At singleton occupations, our counts are numbers of DP-colorings of full covers. The dual DP color function on these classes and their finite seam compositions equals the chromatic polynomial, with equality attained precisely by canonical labelings. Dong's chromatic-polynomial inequality then yields the Dual-DP Shameful inequality on the same graph class. The main theorems have been formalized in Lean 4.

A 2011 conjecture motivated by the Bethe approximation asserts that, for a bipartite graph G and any M-fold cover, the trivial cover maximizes the number of independent sets with every prescribed occupation profile (coefficientwise inequality of independent-set polynomials).

The conjecture is proved for occupation profiles whose active graph has treewidth at most two or is chordal bipartite. Treewidth-two cases use overlap kernels in nonnegative Newton cones with spectral slice scalars. Chordal-bipartite cases use simultaneous compression and a nondecreasing product cone. Fibre comparison at an actual edge or vertex extends the results to finite compositions, and the main theorems are formalized in Lean 4 with Mathlib.

The trivial cover is coefficientwise extremal on these classes, with equality exactly for flat covers. Sharp quantitative deficit bounds hold (factor 2, improved to 3 for odd-order holonomy), and the first nonzero defect is determined by the shortest cycles with nontrivial holonomy. Consequences include a dual DP color function equal to the chromatic polynomial and a Dual-DP Shameful inequality.