arXiv++ Combinatorics

For an edge $uv$ of a finite simple graph $G$, its imbalance is $|d_G(u)-d_G(v)|$, and the imbalance multiset $M_G$ consists of the imbalances of all edges of $G$. Kozerenko and Skochko conjectured that $M_G$ is graphic whenever every edge has positive imbalance. We prove this conjecture. The main ingredient is the following capacity bound: for every set $A$ of $k$ edges, \[ \sum_{e\in E(G)\setminus A}\min\{k,\operatorname{imb}_G(e)\} \ge k\max\{Δ-k,0\}, \] where $Δ$ is the maximum degree of $G$. This bound yields all Erdős--Gallai inequalities directly; a parity computation completes the proof.

We prove the conjecture of Borowiecki and Broere that every finite simple planar graph admits a generalized total coloring with four colors: a proper vertex coloring with four colors together with an edge coloring with four colors in which each edge color class is a forest and no edge receives the color of either endpoint. In fact every proper four-coloring of such a graph extends to an edge coloring of the required kind. The proof combines a component-count inequality for planar graphs whose vertices are partitioned into four independent sets, obtained by completing to a triangulation, with the matroid partition theorem applied to four graphic matroids. A Lean 4 formalization relative to six named background assumptions is described below.

We give a counterexample to Wormald's conjecture. A 16-vertex cubic graph, the disjoint union of $K_{3,3}$ with a 10-vertex bridged graph built from two subdivided copies of $K_4$, has no partition of its edges into two isomorphic spanning linear forests. The obstruction is parity: any such partition would force every monochromatic component to have even order while requiring a five-vertex side of a bridge to be partitioned into such components. Adjoining copies of $K_4$ gives counterexamples in every order $16+4t$. The counterexample is disconnected and leaves the connected case unresolved. The full family is verified in Lean without custom axioms.

For a fixed graph F, the F-degree of a vertex v in a host graph H is the number of subgraphs of H isomorphic to F that contain v, and H is F-irregular if its F-degrees are pairwise distinct. We show that every finite connected graph F on at least three vertices admits a finite connected F-irregular host. For noncomplete F, the proof builds the host from a threshold graph with one deleted edge; when the minimum degree is at least two, a small incidence gadget with distinct weighted column sums separates the remaining exceptional vertices. The construction also yields infinitely many pairwise non-isomorphic finite connected F-irregular hosts for every noncomplete F. The complete-pattern case follows from a theorem of Chartrand, Holbert, Oellermann and Swart. A Lean 4 formalization of Theorem 1.1 is described, taking the published complete-pattern theorem as its sole custom axiom.