Reconstruction Conjecture — A cycle from two internally-disjoint paths

Gluing two paths p, q : G.Walk u w (with distinct endpoints, no shared edges, and disjoint interiors) into a single cycle p.append q.reverse : G.Walk u u. This is how the separator argument forms its cycle: p is a shortest path through one component of G − S, q through another.

Main result

• SimpleGraph.Walk.isCycle_append_reverse — under edge-disjointness and interior (support.tail) disjointness, p.append q.reverse is a cycle.

theorem SimpleGraph.Walk.isCycle_append_reverse {V : Type u_1} {G : SimpleGraph V} {u w : V} {p q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hne : u ≠ w) (hedj : p.edges.Disjoint q.edges) (hsupp : p.support.tail.Disjoint q.reverse.support.tail) : (p.append q.reverse).IsCycle

A cycle from two internally-disjoint paths. If p q : G.Walk u w are paths with u ≠ w, no shared edges, and disjoint interiors (support.tail), then p.append q.reverse is a cycle.