Documentation

Reconstruction.Chordal

Reconstruction Conjecture — Chordal Graphs #

This module begins the chordal-graph structure layer for rung 3 of the separator-decomposition programme. Chordal graphs are entirely absent from Mathlib (confirmed by source audit), so the definition and its basic closure properties are built from scratch here.

A graph is chordal if it has no induced cycle of length ≥ 4. The key formalization observation: a SimpleGraph.Embedding (↪g) is a RelEmbedding, so it not only preserves but reflects adjacency — therefore cycleGraph n ↪g G is exactly an induced n-cycle in G, and "no induced C_n for n ≥ 4" is the clean definition.

Main definitions #

Main results #

Staged targets (stated as Prop, not proved) #

Both are classical (Dirac 1961) but genuinely hard to formalize (they need cycle/chord analysis and a perfect-elimination induction), and are the real Mathlib-gap content; they are recorded here as the precise next targets.

References #

source
def SimpleGraph.IsChordal {V : Type u_1} (G : SimpleGraph V) :
Prop

A graph is chordal if it contains no induced cycle of length ≥ 4. An induced n-cycle is exactly an embedding cycleGraph n ↪g G (a graph embedding is a RelEmbedding, hence reflects non-adjacency too).

Equations
Instances For
    source
    theorem SimpleGraph.IsChordal.map {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (h : G.IsChordal) :
    H.IsChordal

    Chordality is an isomorphism invariant. An induced cycle in H would, composed with e⁻¹, give an induced cycle in G.

    source
    theorem SimpleGraph.IsChordal.induce {V : Type u_1} {G : SimpleGraph V} (S : Set V) (h : G.IsChordal) :
    (SimpleGraph.induce S G).IsChordal

    Chordality is hereditary. An induced cycle in G.induce S includes into G as an induced cycle, so if G has none then neither does G.induce S.

    source
    theorem SimpleGraph.isChordal_of_card_le_three {V : Type u_1} {G : SimpleGraph V} [Fintype V] (h : Fintype.card V ≤ 3) :
    G.IsChordal

    A graph on at most three vertices is chordal: an induced n-cycle for n ≥ 4 would embed Fin n into the vertex type, forcing n ≤ |V| ≤ 3. (A sanity check that the definition behaves on small graphs.)

    source
    theorem SimpleGraph.isChordal_bot {V : Type u_1} :
    ⊥.IsChordal

    The empty graph is chordal: it has no edges, so no cycle — in particular no induced ≥ 4-cycle — can embed (a cycleGraph edge would reflect to a ⊥-edge). A validation that the definition handles the edgeless case.

    source
    theorem SimpleGraph.IsChordal.deleteVert {V : Type u_1} {G : SimpleGraph V} (v : V) (h : G.IsChordal) :
    (G.deleteVert v).IsChordal

    Deleting any vertex preserves chordality (deleteVert is induce). This is the recursion step of a perfect elimination ordering: delete a simplicial vertex and recurse on the still-chordal remainder.

    Simplicial vertices: the base cases #

    IsSimplicial lives in Reconstruction.CliqueSeparator. These are the cases where a simplicial vertex is immediate — the base of the perfect-elimination induction, and the complete-graph case of Dirac's theorem.

    source
    theorem SimpleGraph.isSimplicial_of_subsingleton_neighborSet {V : Type u_1} {G : SimpleGraph V} {v : V} (h : (G.neighborSet v).Subsingleton) :
    G.IsSimplicial v

    A vertex whose neighbourhood has at most one element is simplicial (a ≤ 1-element set is vacuously a clique). In particular isolated vertices and leaves are simplicial.

    source
    theorem SimpleGraph.top_isClique {V : Type u_1} (s : Set V) :
    ⊤.IsClique s

    Every set of vertices is a clique in the complete graph.

    source
    theorem SimpleGraph.isSimplicial_top {V : Type u_1} (v : V) :
    ⊤.IsSimplicial v

    Every vertex of the complete graph is simplicial; so DiracSimplicial holds for complete graphs, and the genuine content is the non-complete case.

    source
    def SimpleGraph.DiracSimplicial (V : Type u_3) [Fintype V] :
    Prop

    TARGET — Dirac 1961. Every finite chordal graph on a nonempty vertex set has a simplicial vertex. The inductive base of perfect elimination orderings; hard to formalize (needs cycle/chord analysis).

    Equations
    Instances For
      source
      def SimpleGraph.DiracCliqueSeparator (V : Type u_3) :
      Prop

      TARGET — Dirac 1961. A non-complete chordal graph has a separator that induces a clique. This guarantees the clean-clique-separation hypothesis of the reassembly engine is always available for chordal graphs, and is the structural input for rung 3.

      Equations
      Instances For
        source
        def SimpleGraph.MinimalSeparatorClique (V : Type u_3) :
        Prop

        The crux behind Dirac. In a chordal graph an inclusion-minimal separator induces a clique. (Two non-adjacent vertices of a minimal separator would, via shortest paths through two different G − S components, yield an induced ≥ 4-cycle, contradicting chordality.) From this, both DiracSimplicial and DiracCliqueSeparator follow by induction on the components of G − S.

        Proved as SimpleGraph.minimalSeparatorClique in MinimalSeparatorClique.lean, via the induced-cycle-extraction machinery (Geodesic, InducedCycle, CycleFromPaths, MinimalSeparator).

        Equations
        Instances For