Tree-like closed walks

A closed walk of G at v is tree-like when it lifts to a closed walk at the root of Godsil's path tree T(G, v). The lift is deterministic: keeping the current simple path as a stack, each step either extends it by a vertex not on it or returns to the previous vertex; any other step fails. A closed walk whose edges span an acyclic subgraph is tree-like.

Main definitions

• SimpleGraph.liftSeq: the deterministic lift of a vertex sequence, as an optional stack.
• SimpleGraph.Walk.IsTreeLike: the lift of the walk returns to the root.

Main results

• SimpleGraph.Walk.nil_isTreeLike: the trivial walk is tree-like.
• SimpleGraph.liftSeq_eq_pathSupport_of_acyclic: on an acyclic subgraph the lift follows the unique paths.
• SimpleGraph.Walk.isTreeLike_of_acyclic: a closed walk with acyclic edge support is tree-like.

References

• C. D. Godsil, Matchings and walks in graphs, J. Graph Theory 5 (1981) 285–297.

def SimpleGraph.liftSeq {V : Type u_1} [DecidableEq V] : List V → List V → Option (List V)

Deterministic lift of a sequence of visited vertices into the path tree, threading the current simple path (stack, from root to current vertex). For each next vertex c: if c ∉ stack push it (EXTEND); else if c is the penultimate vertex of stack pop the last (RETREAT to parent); else fail. Returns the final stack, or none if some step is neither extend nor retreat.

Equations

• SimpleGraph.liftSeq [] x✝ = some x✝
• SimpleGraph.liftSeq (c :: rest) x✝ = if c ∈ x✝ then if x✝.dropLast.getLast? = some c then SimpleGraph.liftSeq rest x✝.dropLast else none else SimpleGraph.liftSeq rest (x✝ ++ [c])

theorem SimpleGraph.liftSeq_cons {V : Type u_1} [DecidableEq V] (c : V) (rest stack : List V) : liftSeq (c :: rest) stack = if c ∈ stack then if stack.dropLast.getLast? = some c then liftSeq rest stack.dropLast else none else liftSeq rest (stack ++ [c])

Definitional unfolding of liftSeq on a cons.

def SimpleGraph.Walk.IsTreeLike {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {v : V} (w : G.Walk v v) : Prop

A closed walk is tree-like (Godsil's path-tree class) iff its deterministic lift, started at the root path [v], returns to the root path [v] (a closed walk at the root of T(G,v)).

Equations

• w.IsTreeLike = (SimpleGraph.liftSeq w.support.tail [v] = some [v])

@[instance_reducible]

instance SimpleGraph.instDecidableIsTreeLike {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {v : V} (w : G.Walk v v) : Decidable w.IsTreeLike

Equations

• SimpleGraph.instDecidableIsTreeLike w = id inferInstance

theorem SimpleGraph.Walk.nil_isTreeLike {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (v : V) : nil.IsTreeLike

The empty walk lifts trivially: its only visited vertex is the root, the lift never moves, and the stack stays [v].

Below the girth: every closed walk lifts (the remaining sub-lemma)

Below the (extended) girth the walk's edge-support is acyclic (a forest). On a forest the lift always succeeds: the deterministic stack stays equal to the unique forest-path from the root to the current vertex, so each step is forced to be EXTEND (edge away from root) or RETREAT (edge back toward root, hitting the penultimate vertex). A closed walk returns the stack to [v].

The core inductive invariant is liftSeq_eq_pathSupport_of_acyclic: matching liftSeq's List V stack to the graph-theoretic unique forest-path. The key step — acyclicity forcing each RETREAT to the penultimate vertex — is isolated in eq_penultimate_of_acyclic (build a cycle from the would-be chord and contradict H.coe.IsAcyclic).

theorem SimpleGraph.Subgraph.coe_isAcyclic_mono {V : Type u_1} {G : SimpleGraph V} {H₁ H₂ : G.Subgraph} (hle : H₁ ≤ H₂) (h : H₂.coe.IsAcyclic) : H₁.coe.IsAcyclic

A subgraph of an acyclic (coerced) subgraph is acyclic: pull a cycle back along the injective inclusion H₁.coe →g H₂.coe.

theorem SimpleGraph.not_isCycle_of_toSubgraph_le {V : Type u_1} {G : SimpleGraph V} {x : V} {H : G.Subgraph} (C : G.Walk x x) (hC : C.IsCycle) (hle : C.toSubgraph ≤ H) (hac : H.coe.IsAcyclic) : False

A cycle of G whose edges all lie inside a subgraph H lifts to a cycle of H.coe, so an acyclic H.coe admits none. Lift C first to its own subgraph (mapToSubgraph, injective via toSubgraph.hom), then along the injective inclusion C.toSubgraph ↪ H.

theorem SimpleGraph.eq_penultimate_of_acyclic {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {root a c : V} {H : G.Subgraph} (sp : G.Walk root a) (hsp : sp.IsPath) (h : G.Adj a c) (hv : c ∈ sp.support) (hcsub : G.subgraphOfAdj h ≤ H) (hspsub : sp.toSubgraph ≤ H) (hac : H.coe.IsAcyclic) : c = sp.penultimate

The acyclicity key step. In an acyclic ambient subgraph H containing a simple path sp : root → a and the edge a ~ c, if c lies on sp then c must be the penultimate vertex of sp (its neighbour along the path). Otherwise the sp-segment from c to a together with the closing edge a~c would form a cycle inside H, contradicting hac.

theorem SimpleGraph.Walk.support_dropLast_getLast?_eq_penultimate {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil) : p.support.dropLast.getLast? = some p.penultimate

For a non-nil walk, the last entry of its support with the endpoint dropped is the penultimate vertex (getLast? of support.dropLast).

theorem SimpleGraph.liftSeq_eq_pathSupport_of_acyclic {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {root a b : V} (p : G.Walk a b) (sp : G.Walk root a) (hsp : sp.IsPath) (hacyc : (p.toSubgraph ⊔ sp.toSubgraph).coe.IsAcyclic) : ∃ (sq : G.Walk root b), sq.IsPath ∧ liftSeq p.support.tail sp.support = some sq.support

Invariant. If the ambient is acyclic, running liftSeq on the tail of a path p's support, started from the vertex list of a simple path sp from the root to p's source, returns the vertex list of the simple path from the root to p's target. (Forest unique-path bookkeeping: each step extends or retreats the unique root-path; this is where the List ↔ graph-path friction lives.)

theorem SimpleGraph.Walk.isTreeLike_of_acyclic {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {v : V} (w : G.Walk v v) (hacyc : w.toSubgraph.coe.IsAcyclic) : w.IsTreeLike

A closed walk whose edge-support is acyclic is tree-like: take sp = nil (root path [v]) in the invariant; the returned simple path from v to v is nil, support [v].