Neighbours in a cycle graph

For m ≥ 2, Mathlib's SimpleGraph.cycleGraph m joins two elements of Fin m exactly when they differ by one and records the neighbour set of a vertex as the pair {v - 1, v + 1}; for m ≥ 3, it computes the degree to be two. This file derives the weaker fact valid for every nonzero m that an adjacent vertex is the successor or predecessor, and shows that there are at most the two neighbours v + 1 and v - 1; when m ≥ 3, they are distinct and really are neighbours.

Main results

• TauCeti.eq_add_one_or_eq_add_one_of_cycleGraph_adj: adjacent vertices differ by one.
• TauCeti.eq_or_eq_or_eq_of_cycleGraph_adj: no vertex has three pairwise distinct neighbours, that is, every degree is at most two.
• TauCeti.cycleGraph_adj_add_one: on at least three vertices a vertex is adjacent to its successor.

theorem TauCeti.eq_add_one_or_eq_add_one_of_cycleGraph_adj {m : ℕ} [NeZero m] {u v : Fin m} (h : (SimpleGraph.cycleGraph m).Adj u v) : v = u + 1 ∨ u = v + 1

Adjacent vertices of a cycle graph differ by one.

theorem TauCeti.eq_or_eq_or_eq_of_cycleGraph_adj {m : ℕ} [NeZero m] {i j j' j'' : Fin m} (h : (SimpleGraph.cycleGraph m).Adj i j) (h' : (SimpleGraph.cycleGraph m).Adj i j') (h'' : (SimpleGraph.cycleGraph m).Adj i j'') : j = j' ∨ j' = j'' ∨ j'' = j

No vertex of a cycle graph has three pairwise distinct neighbours: every degree is at most two.

theorem TauCeti.cycleGraph_adj_add_one {m : ℕ} [NeZero m] (hm : 3 ≤ m) (v : Fin m) : (SimpleGraph.cycleGraph m).Adj v (v + 1)

Consecutive vertices of a cycle graph on at least three vertices are adjacent.