inductive DirectedCycles.DirectedWalk {V : Type u_1} (G : Digraph V) : V → V → Type u_1

A directed walk in a digraph $G$ from vertex $u$ to vertex $v$: either the empty walk at $u$, or a step along a directed edge followed by another walk.

• nil {V : Type u_1} {G : Digraph V} {u : V} : DirectedWalk G u u
• cons {V : Type u_1} {G : Digraph V} {u v w : V} (h : G.Adj u v) (p : DirectedWalk G v w) : DirectedWalk G u w

def DirectedCycles.DirectedWalk.length {V : Type u_1} {G : Digraph V} {u v : V} : DirectedWalk G u v → ℕ

The length (number of edges) of a directed walk.

def DirectedCycles.DirectedWalk.support {V : Type u_1} {G : Digraph V} {u v : V} : DirectedWalk G u v → List V

The list of vertices visited by a directed walk, in order.

def DirectedCycles.DirectedWalk.append {V : Type u_1} {G : Digraph V} {u v w : V} : DirectedWalk G u v → DirectedWalk G v w → DirectedWalk G u w

Concatenation of two directed walks meeting at a common vertex.

def DirectedCycles.DirectedWalk.cast {V : Type u_1} {G : Digraph V} {u v u' v' : V} (hu : u = u') (hv : v = v') : DirectedWalk G u v → DirectedWalk G u' v'

Recast a directed walk along propositional equalities of its endpoints.

theorem DirectedCycles.DirectedWalk.length_cast {V : Type u_1} {G : Digraph V} {u v u' v' : V} (hu : u = u') (hv : v = v') (p : DirectedWalk G u v) : (cast hu hv p).length = p.length

Casting along endpoint equalities preserves the length of a directed walk.

structure DirectedCycles.DirectedWalk.IsCycle {V : Type u_1} {G : Digraph V} {u : V} (p : DirectedWalk G u u) : Prop

A directed walk from a vertex to itself is a cycle if it has positive length and visits each vertex at most once (no repeated vertices apart from the start/end).

• pos_length : p.length > 0
• support_nodup : p.support.tail.Nodup

def DirectedCycles.HasDirectedCycleDivisibleBy {V : Type u_1} (G : Digraph V) (k : ℕ) : Prop

The digraph $G$ contains a directed cycle whose length is divisible by $k$.

def DirectedCycles.outDegree {V : Type u_1} (G : Digraph V) [Fintype V] [DecidableRel G.Adj] (v : V) : ℕ

Out-degree of a vertex $v$ in a digraph: the number of vertices $w$ with $v \to w$.

def DirectedCycles.inDegree {V : Type u_1} (G : Digraph V) [Fintype V] [DecidableRel G.Adj] (v : V) : ℕ

In-degree of a vertex $v$ in a digraph: the number of vertices $w$ with $w \to v$.

def DirectedCycles.IsRegular {V : Type u_1} (G : Digraph V) [Fintype V] [DecidableRel G.Adj] (d : ℕ) : Prop

A digraph is $d$-regular if every vertex has in-degree and out-degree both equal to $d$.

def DirectedCycles.IsSuccessorLabeling {V : Type u_1} (G : Digraph V) (k : ℕ) [NeZero k] (f : V → ZMod k) : Prop

A successor labeling $f : V \to \mathbb{Z}/k\mathbb{Z}$ assigns each vertex $v$ an out-neighbor $w$ whose label is $f(v) + 1$; following such successors produces a cycle of length divisible by $k$.

noncomputable def DirectedCycles.consWalk {V : Type u_1} (G : Digraph V) (seq : ℕ → V) (hadj : ∀ (n : ℕ), G.Adj (seq n) (seq (n + 1))) (m : ℕ) : DirectedWalk G (seq 0) (seq m)

Build the directed walk along the first $m$ steps of a vertex sequence whose consecutive elements are adjacent.

theorem DirectedCycles.consWalk_length {V : Type u_1} (G : Digraph V) (seq : ℕ → V) (hadj : ∀ (n : ℕ), G.Adj (seq n) (seq (n + 1))) (m : ℕ) : (consWalk G seq hadj m).length = m

The walk consWalk G seq hadj m has length $m$.

theorem DirectedCycles.mem_consWalk_support {V : Type u_1} (G : Digraph V) (seq : ℕ → V) (hadj : ∀ (n : ℕ), G.Adj (seq n) (seq (n + 1))) (m : ℕ) (v : V) : v ∈ (consWalk G seq hadj m).support ↔ ∃ i ≤ m, v = seq i

Membership characterization: $v$ is in the support of consWalk G seq hadj m iff $v = $ seq i for some $i \le m$.

theorem DirectedCycles.consWalk_support_nodup {V : Type u_1} (G : Digraph V) (seq : ℕ → V) (hadj : ∀ (n : ℕ), G.Adj (seq n) (seq (n + 1))) (m : ℕ) (hinj : ∀ (i j : ℕ), i ≤ m → j ≤ m → seq i = seq j → i = j) : (consWalk G seq hadj m).support.Nodup

If seq is injective on indices $\le m$, then the support of consWalk G seq hadj m has no duplicate vertices.

theorem DirectedCycles.consWalk_tail_nodup {V : Type u_1} (G : Digraph V) (seq : ℕ → V) (hadj : ∀ (n : ℕ), G.Adj (seq n) (seq (n + 1))) (m : ℕ) (hm : 0 < m) (hinj : ∀ (i j : ℕ), 1 ≤ i → i ≤ m → 1 ≤ j → j ≤ m → seq i = seq j → i = j) : (consWalk G seq hadj m).support.tail.Nodup

Tail-version of consWalk_support_nodup: if seq is injective on indices $1 \le i \le m$, then the tail of the walk's support has no duplicates (used for proving the cycle property).

theorem DirectedCycles.DirectedWalk.support_cast {V : Type u_1} {u v u' v' : V} {G : Digraph V} (hu : u = u') (hv : v = v') (p : DirectedWalk G u v) : (cast hu hv p).support = p.support

Casting along endpoint equalities preserves the support of a directed walk.

theorem DirectedCycles.cycle_of_successor_labeling {V : Type u_1} (G : Digraph V) [Fintype V] [DecidableRel G.Adj] [DecidableEq V] [Nonempty V] (k : ℕ) [NeZero k] (f : V → ZMod k) (hf : IsSuccessorLabeling G k f) : HasDirectedCycleDivisibleBy G k

A successor labeling $f : V \to \mathbb{Z}/k\mathbb{Z}$ yields a directed cycle in $G$ whose length is divisible by $k$, obtained by following successors from any starting vertex.

theorem DirectedCycles.successor_labeling_exists {V : Type u_2} (G : Digraph V) [Fintype V] [DecidableRel G.Adj] [DecidableEq V] [Nonempty V] (k δ Δ : ℕ) [NeZero k] (hδ : ∀ (v : V), δ ≤ outDegree G v) (hΔ : ∀ (v : V), inDegree G v ≤ Δ) (hbound : ↑k ≤ ↑δ / (1 + Real.log (1 + ↑δ * ↑Δ))) : ∃ (f : V → ZMod k), IsSuccessorLabeling G k f

LLL-based existence of a successor labeling: if minimum out-degree $\delta$ and maximum in-degree $\Delta$ satisfy $k \le \delta / (1 + \log(1 + \delta\Delta))$, then a random labeling yields a successor labeling with positive probability (Theorem 6.4.3, Alon-Linial).

theorem DirectedCycles.hasDirectedCycleDivisibleBy_of_degree_bound {V : Type u_1} (G : Digraph V) [Fintype V] [DecidableRel G.Adj] [DecidableEq V] [Nonempty V] (k δ Δ : ℕ) (hk : k ≥ 1) (hδ : ∀ (v : V), δ ≤ outDegree G v) (hΔ : ∀ (v : V), inDegree G v ≤ Δ) (hbound : ↑k ≤ ↑δ / (1 + Real.log (1 + ↑δ * ↑Δ))) : HasDirectedCycleDivisibleBy G k

Combining successor_labeling_exists and cycle_of_successor_labeling: any digraph with minimum out-degree $\delta$ and maximum in-degree $\Delta$ satisfying the LLL bound has a directed cycle of length divisible by $k$.

theorem DirectedCycles.exists_nat_le_div_one_add_log (k : ℕ) (hk : k ≥ 1) : ∃ d ≥ 1, ↑k ≤ ↑d / (1 + Real.log (1 + ↑d * ↑d))

Existence of a degree $d \ge 1$ (here taken to be $25k^2$) satisfying the LLL bound $k \le d / (1 + \log(1 + d^2))$, used to convert the bound into a concrete regularity hypothesis.

theorem DirectedCycles.exists_regular_degree_hasDirectedCycleDivisibleBy (k : ℕ) (hk : k ≥ 1) : ∃ (d : ℕ), ∀ (V : Type) (G : Digraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [DecidableEq V] [Nonempty V], IsRegular G d → HasDirectedCycleDivisibleBy G k

Theorem 6.4.1 (Alon-Linial 1989): for every $k \ge 1$ there exists $d$ such that every $d$-regular digraph contains a directed cycle of length divisible by $k$.

def DirectedCycles.HasCycleDivisibleBy {V : Type u_1} (G : SimpleGraph V) (k : ℕ) : Prop

A simple graph $G$ contains a cycle whose length is divisible by $k$.

theorem DirectedCycles.eulerian_orientation_gives_cycle {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [Nonempty V] [DecidableRel G.Adj] (d : ℕ) (hreg : G.IsRegularOfDegree (2 * d)) (k : ℕ) : (∀ (H : Digraph V) [inst : DecidableRel H.Adj], IsRegular H d → HasDirectedCycleDivisibleBy H k) → HasCycleDivisibleBy G k

Bridge from the directed to the undirected setting: any $2d$-regular simple graph admits an Eulerian orientation that is $d$-regular as a digraph, so existence of a directed cycle of length divisible by $k$ in the orientation yields an undirected cycle of the same length.

theorem DirectedCycles.exists_even_regular_hasCycleDivisibleBy (k : ℕ) (hk : k ≥ 1) : ∃ (d : ℕ), ∀ (V : Type) (G : SimpleGraph V) [inst : Fintype V] [DecidableEq V] [Nonempty V] [inst_3 : DecidableRel G.Adj], G.IsRegularOfDegree (2 * d) → HasCycleDivisibleBy G k

Corollary 6.4.2 (undirected version of Alon-Linial): for every $k \ge 1$ there exists $d$ such that every $2d$-regular simple graph contains a cycle of length divisible by $k$.