Forcing a shared degree-three star #
The incidence census below is independent of the finite-order case files. In a graph
with minimum degree at least three and no edge joining two degree-three vertices, it
forces a degree-four vertex with at least two degree-three neighbors whenever the order
is at most 31.
theorem
ACMax.z1_forced_of_le_31
{n : ℕ}
(hn8 : 8 ≤ n)
(hn31 : n ≤ 31)
(G : SimpleGraph (Fin n))
(hm : G.edgeFinset.card = 2 * (n - 2))
(h3 : ∀ (v : Fin n), 3 ≤ G.degree v)
(hs0 : ∀ (v w : Fin n), G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w)
:
On 8 <= n <= 31, a graph in the starved census contains a degree-4 vertex
with at least two degree-3 neighbors.