Chordal graphs and exact edge partitions into cliques
Definitionerdos81_clique_partitionsThis module defines chordality through a perfect-elimination ranking: the later neighbors of every vertex are pairwise adjacent. For finite simple graphs, this is the standard chordal-graph characterization.
An exact edge-clique partition is a finite family of finite vertex sets, each spanning a complete subgraph, such that every graph edge belongs to exactly one family member. Pieces may share vertices but not edges. HasCliquePartitionAtMost G B asks for such a family whose natural-number cardinality, coerced to a real number, is at most .
Edgeless and disconnected graphs are included. Empty or singleton listed cliques are not explicitly forbidden, but they cannot help satisfy an upper bound and contain no graph edge.
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Finset.Card
import Mathlib.Data.Real.Basic
namespace Erdos81
universe u
/-- A finite set of vertices spans a complete subgraph. -/
def IsClique {V : Type u} (G : SimpleGraph V) (C : Finset V) : Prop :=
∀ ⦃u v : V⦄, u ∈ C → v ∈ C → u ≠ v → G.Adj u v
/-- A perfect-elimination presentation of a chordal graph. Later neighbors of
each vertex must be pairwise adjacent. -/
def IsChordal {V : Type u} (G : SimpleGraph V) : Prop :=
∃ rank : V → ℕ,
Function.Injective rank ∧
∀ ⦃v a b : V⦄,
G.Adj v a → G.Adj v b → rank v < rank a → rank v < rank b →
a ≠ b → G.Adj a b
/-- An exact edge partition into complete subgraphs. Each graph edge occurs in
exactly one listed clique. -/
def IsEdgeCliquePartition {V : Type u} (G : SimpleGraph V)
(P : Finset (Finset V)) : Prop :=
(∀ C ∈ P, IsClique G C) ∧
∀ ⦃u v : V⦄, G.Adj u v →
∃! C : Finset V, C ∈ P ∧ u ∈ C ∧ v ∈ C
/-- `G` has an exact edge-clique partition with at most the real-valued bound
`B` pieces. -/
def HasCliquePartitionAtMost {V : Type u} (G : SimpleGraph V) (B : ℝ) : Prop :=
∃ P : Finset (Finset V),
IsEdgeCliquePartition G P ∧ (P.card : ℝ) ≤ B
end Erdos81Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
IsClique. For a type of vertices V, a simple graph G on V, and a finite set C of vertices, C is a clique exactly when every two distinct vertices u and v belonging to C are adjacent in G. IsChordal. A simple graph G on V is chordal exactly when there exists an injective assignment rank of a natural number to every vertex such that, for all vertices v, a, and b, if a and b are both adjacent to v, both have strictly larger rank than v, and a and b are distinct, then a and b are adjacent. IsEdgeCliquePartition. For a simple graph G on V and a finite collection P of finite vertex sets, P is an edge-clique partition exactly when every C in P is a clique, and every edge between vertices u and v belongs to exactly one member C of P, meaning C contains both u and v. HasCliquePartitionAtMost. For a simple graph G on V and a real number B, G has a clique partition with at most B pieces exactly when there exists a finite collection P of finite vertex sets satisfying the preceding edge-clique-partition conditions and whose number of members, regarded as a real number, is at most B. These definitions impose no additional condition on vertices or sets that are not involved in an edge; in particular, the edge conditions are vacuous for a graph with no edges.
Confirmed by the mission captain (proposal self-audit).