Reconstruction Conjecture — Geodesics are chordless

The linchpin of the induced-cycle-extraction machinery: a shortest path (a walk whose length realizes the graph distance) has no chord — no edge joins two of its vertices that are more than one step apart along the walk. Equivalently a geodesic is an induced path. This is what forces the cycle glued from two shortest paths (through two components of G − S) to be chordless, hence an induced cycle.

Main results

• SimpleGraph.Walk.geodesic_not_adj_of_lt — on a geodesic p, if i + 1 < j (and j ≤ p.length) then p.getVert i and p.getVert j are non-adjacent.
• SimpleGraph.Walk.geodesic_not_adj_of_lt' — the symmetric statement.

theorem SimpleGraph.Walk.geodesic_not_adj_of_lt {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : p.length = G.dist u v) {i j : ℕ} (hij : i + 1 < j) (hj : j ≤ p.length) : ¬G.Adj (p.getVert i) (p.getVert j)

A geodesic is chordless. If p is a shortest u–v walk (p.length = G.dist u v) and i + 1 < j ≤ p.length, then p.getVert i and p.getVert j are not adjacent: a chord would shortcut p (take to i, the chord edge, drop from j) into a strictly shorter u–v walk, impossible.

theorem SimpleGraph.Walk.geodesic_not_adj_of_lt' {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : p.length = G.dist u v) {i j : ℕ} (hij : i + 1 < j) (hj : j ≤ p.length) : ¬G.Adj (p.getVert j) (p.getVert i)

The symmetric form of geodesic_not_adj_of_lt.