Clique suffix perfect-elimination order in chordal graphs

Proved

Erdos81.chordal_clique_suffix_peo

by Zexuan Liu · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

chordal-graphsclique-partitioncombinatoricsperfect-elimination-order

Let $G$ be a finite chordal graph and let $S$ be any clique of $G$ . Then $G$ has a perfect-elimination ordering in which every vertex outside $S$ occurs before every vertex of $S$ . Equivalently, there is an injective rank function whose later-neighbor condition certifies chordality and whose final block is exactly the prescribed clique $S$ . This is the structural suffix-elimination lemma used by weighted-neighborhood compression: it permits all edges outside $S$ to be charged to the earlier endpoint while keeping the edges internal to $S$ as a separate core. The statement is extracted from the clique-suffix argument in C22, Section 4, of the Erdos 81 chordal-clique-partition research record.

Preamble

import Definitions.Def_erdos81_clique_partitions

Formal statement

namespace Erdos81

theorem chordal_clique_suffix_peo {n : ℕ}
    (G : SimpleGraph (Fin n)) (hG : Erdos81.IsChordal G)
    (S : Finset (Fin n)) (hS : Erdos81.IsClique G S) :
    ∃ rank : Fin n → ℕ, Function.Injective rank ∧
      (∀ ⦃v a b : Fin n⦄, G.Adj v a → G.Adj v b →
        rank v < rank a → rank v < rank b → a ≠ b → G.Adj a b) ∧
      (∀ v : Fin n, v ∉ S → ∀ s ∈ S, rank v < rank s) := by sorry

end Erdos81

Source

C22 candidate, Section 4 (clique-suffix elimination), https://github.com/vibemathing/problem-erdos-81-chordal-clique-partition/blob/09c2b6f3e277eb20fc34d0add65ee8d027c5bb37/research/artifacts/candidates/erdos81-a01-c22-c20-audit.md

View graph