Gavril's characterization of finite chordal graphs

For the converse, prune leaves of the host tree until some represented subtree is a singleton. Its vertex is simplicial. Repeating this argument on any finite subfamily gives a perfect elimination order through the existing PEO engine.

The theorem formalized here is F. Gavril, "The intersection graphs of subtrees in trees are exactly the chordal graphs", JCT B 16 (1974), 47–56, doi:10.1016/0095-8956(74)90094-X. No recognition algorithm or runtime bound is claimed.

theorem SimpleGraph.SubtreeRepresentation.isChordal {V : Type u_1} {G : SimpleGraph V} [Finite V] (R : G.SubtreeRepresentation) : G.IsChordal

Any finite graph represented exactly by subtrees of a finite tree is chordal.

theorem SimpleGraph.isChordal_iff_nonempty_subtreeRepresentation {V : Type} {G : SimpleGraph V} [Finite V] : G.IsChordal ↔ Nonempty G.SubtreeRepresentation

Gavril's characterization: finite chordal graphs are exactly finite-tree subtree graphs.