Papers With

← All papers
First page of A construction of F-irregular graphs

A construction of F-irregular graphs

James Alexander Schreib

math.CO Sep 7, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
A Lean 4 formalization of the main existence theorem is developed, using the published complete-pattern theorem as its sole custom axiom.
Abstract
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.
Problem

For a fixed graph F, the F-degree of a vertex counts subgraphs isomorphic to F containing it, and a host is F-irregular if these degrees are distinct. Whether every finite connected F on at least three vertices admits a finite connected F-irregular host was conjectured in 1987.

Approach

The complete-pattern case reduces to a known theorem via component restriction. For noncomplete F, a host is built from a threshold graph with one deleted edge, ordering most vertices by neighborhood inclusion. Two displaced vertices are handled by local automorphism comparisons, and remaining exceptional vertices are separated with an incidence gadget having distinct weighted column sums. Theorem 1.1 is formalized in Lean 4, taking the complete-pattern theorem as the only custom axiom.

Results

Every finite connected graph F on at least three vertices admits a finite connected F-irregular host with at least two vertices, and for noncomplete F there are infinitely many pairwise non-isomorphic such hosts. The Lean development is checked by the kernel with statements confirmed by hand against the paper.