A Four-Connected Graph without a Legal System
Qiuyu Chen
cs.DM
Sep 11, 2026 · v1
math.CO
TL;DR
The main results, including the amalgam restriction theorem and properties of the 33-vertex construction, are formalized in Lean in a public GitHub repository.
Abstract
In a 2021 paper, Jankiewicz, Norin, and Wise asked whether there exists a finite $4$-connected graph of girth at least four and nonnegative Charney–Davis curvature such that no $4$-connected ordinary subgraph admits a legal system. We construct such a graph by starting from the hexagonal prism and attaching three $K_{3,4}$-based caps along pairwise disjoint induced $4$-cycles. The key structural input is a restriction theorem showing that a legal system on an induced-$4$-cycle amalgam restricts to each side, so the obstruction carried by the negatively curved prism survives the attachments. The resulting $33$-vertex graph is $4$-regular and $4$-connected, has girth four and Charney–Davis curvature one, and, by $4$-regularity, is its own unique $4$-connected ordinary subgraph.
Problem
Jankiewicz, Norin, and Wise asked whether there is a finite 4-connected graph of girth at least four with nonnegative Charney–Davis curvature such that no 4-connected ordinary subgraph admits a legal system (their Problem 5.2).
Approach
A restriction theorem shows that a legal system on an amalgam along an induced 4-cycle restricts to a legal system on each side. Starting from the hexagonal prism, whose negative 2-curvature rules out a legal system, three K_{3,4}-based caps are attached along pairwise disjoint induced 4-cycles. A lemma shows that a 4-regular connected graph is its own unique 4-connected ordinary subgraph. The main results are formalized in Lean.
Results
The construction gives a 33-vertex, 4-regular, 4-connected graph of girth four and Charney–Davis curvature one with no legal system. This answers the 4-connected question of Jankiewicz–Norin–Wise.
