Joining a rooted clique forest by one connector

The new node none is joined to every original root. Original parent edges are unchanged. The resulting graph is a tree, including for an empty forest. Strict rank descent proves connectivity; a maximal-rank vertex on a putative cycle would have two different lower neighbours, contradicting unique parenthood.

def SimpleGraph.CliqueTree.connectorParent {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) : Option ι → Option ι

Parent in the connected augmentation; the connector is its own parent.

Equations

• T.connectorParent none = none
• T.connectorParent (some i) = T.parent i

def SimpleGraph.CliqueTree.connectorRank {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) : Option ι → ℕ

The connector has rank zero and original nodes have their rank shifted by one.

Equations

• T.connectorRank none = 0
• T.connectorRank (some i) = T.rank i + 1

theorem SimpleGraph.CliqueTree.connectorParent_rank_lt {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) {x : Option ι} (hx : x ≠ none) : T.connectorRank (T.connectorParent x) < T.connectorRank x

Every original node has a strictly lower parent in the augmentation.

def SimpleGraph.CliqueTree.connectorGraph {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) : SimpleGraph (Option ι)

The undirected parent graph, with each root joined to a new connector.

Equations

• T.connectorGraph = { Adj := fun (x y : Option ι) => x ≠ none ∧ T.connectorParent x = y ∨ y ≠ none ∧ T.connectorParent y = x, symm := ⋯, loopless := ⋯ }

theorem SimpleGraph.CliqueTree.connectorGraph_adj_parent {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) (i : ι) : T.connectorGraph.Adj (some i) (T.parent i)

An original node is adjacent to its augmented parent, even if it is a root.

@[simp]

theorem SimpleGraph.CliqueTree.connectorGraph_adj_none_some {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) (i : ι) : T.connectorGraph.Adj none (some i) ↔ T.parent i = none

Exactly the original roots are adjacent to the connector.

@[simp]

theorem SimpleGraph.CliqueTree.connectorGraph_adj_some_some {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) (i j : ι) : T.connectorGraph.Adj (some i) (some j) ↔ T.parent i = some j ∨ T.parent j = some i

Adjacency between original nodes is exactly their original parent relation.

theorem SimpleGraph.CliqueTree.connectorGraph_reachable_connector {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) (x : Option ι) : T.connectorGraph.Reachable x none

Every node reaches the connector by repeatedly following its parent.

theorem SimpleGraph.CliqueTree.connectorGraph_connected {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) : T.connectorGraph.Connected

The connector joins all roots into a single connected graph.

theorem SimpleGraph.CliqueTree.connectorParent_eq_of_adj_of_rank_le {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) {x y : Option ι} (hxy : T.connectorGraph.Adj x y) (hy : T.connectorRank y ≤ T.connectorRank x) : T.connectorParent x = y

A neighbour with no larger rank must be the unique augmented parent.

theorem SimpleGraph.CliqueTree.connectorGraph_isAcyclic {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) : T.connectorGraph.IsAcyclic

No cycle can have two different neighbours of its maximal-rank vertex.

theorem SimpleGraph.CliqueTree.connectorGraph_isTree {V : Type u_1} {ι : Type u_2} {G : SimpleGraph V} (T : G.CliqueTree ι) : T.connectorGraph.IsTree

Connecting the roots of a clique forest produces a genuine tree.