Reconstruction Conjecture — Chordless cycle ⟶ cycleGraph embedding (the bridge)

Converts a chordless closed walk (a cycle whose only adjacencies among its vertices are the cyclically-consecutive ones) into the embedding cycleGraph n ↪g G that IsChordal forbids. This is the bridge between the classical "induced cycle" produced by the separator argument and the embedding-based definition of chordality.

Main results

• SimpleGraph.cycleGraph_adj_val — a .val-level characterization of cycleGraph n adjacency (consecutive or wrap-around), the keystone.
• SimpleGraph.inducedCycleEmbedding — a chordless IsCycle walk of length n ≥ 4 yields cycleGraph n ↪g G.

theorem SimpleGraph.cycleGraph_adj_val {n : ℕ} (hn : 4 ≤ n) (i j : Fin n) : (cycleGraph n).Adj i j ↔ ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i ∨ ↑i = 0 ∧ ↑j = n - 1 ∨ ↑j = 0 ∧ ↑i = n - 1

Value-level characterization of cycleGraph n adjacency for n ≥ 4: two vertices are adjacent iff their indices are consecutive or wrap around the cycle. This eliminates the opaque modular Fin subtraction once and for all.

theorem SimpleGraph.inducedCycleEmbedding {V : Type u_1} {G : SimpleGraph V} {u : V} {n : ℕ} (hn : 4 ≤ n) (p : G.Walk u u) (hp : p.IsCycle) (hlen : p.length = n) (hchord : ∀ (a b : Fin n), G.Adj (p.getVert ↑a) (p.getVert ↑b) → (cycleGraph n).Adj a b) : Nonempty (cycleGraph n ↪g G)

The bridge. A chordless IsCycle walk of length n ≥ 4 — chordless in the sense that the only G-adjacencies among its n vertices p.getVert 0, …, p.getVert (n-1) are the cyclically-consecutive ones (hchord) — yields a graph embedding cycleGraph n ↪g G, i.e. an induced n-cycle. This is exactly the object IsChordal forbids, so producing one for n ≥ 4 contradicts chordality.

theorem SimpleGraph.inducedCycleEmbedding_of_paths {V : Type u_1} {G : SimpleGraph V} {x y : V} (hxy : x ≠ y) (P Q : G.Walk x y) (hP : P.IsPath) (hQ : Q.IsPath) (hPlen : 2 ≤ P.length) (hQlen : 2 ≤ Q.length) (hPchord : ∀ (i j : ℕ), i + 1 < j → j ≤ P.length → ¬G.Adj (P.getVert i) (P.getVert j)) (hQchord : ∀ (i j : ℕ), i + 1 < j → j ≤ Q.length → ¬G.Adj (Q.getVert i) (Q.getVert j)) (hcross : ∀ (i j : ℕ), 0 < i → i < P.length → 0 < j → j < Q.length → ¬G.Adj (P.getVert i) (Q.getVert j)) (hedj : P.edges.Disjoint Q.edges) (hsupp : P.support.tail.Disjoint Q.reverse.support.tail) : Nonempty (cycleGraph (P.length + Q.length) ↪g G)

Two-arc induced cycle. Glue two internally-disjoint chordless arcs P, Q : x → y (each a shortest path, hence chordless: no chord between non-consecutive vertices; plus no edge between the two interiors) into an induced cycle cycleGraph (|P| + |Q|) ↪g G. This is the form the separator argument feeds: P runs through one component of G − S, Q through another, so they share only x, y, have no cross-edges, and x ≁ y.