def Hex.GraphIso.Nauty.Sparse.rowCmp {n : Nat} (a b : List (Fin n)) : Ordering

Compare sorted sparse rows: smaller degree wins, and with equal degrees the row containing the first differing vertex wins.

Equations

• Hex.GraphIso.Nauty.Sparse.rowCmp a b = compare (b.length, b) (a.length, a)

instance Hex.GraphIso.Nauty.Sparse.instTransCmpListFinRowCmp {n : Nat} : Std.TransCmp rowCmp

instance Hex.GraphIso.Nauty.Sparse.instLawfulEqCmpListFinRowCmp {n : Nat} : Std.LawfulEqCmp rowCmp

def Hex.GraphIso.Nauty.Sparse.graphRows {n : Nat} (G : SparseGraph n) : List (List (Fin n))

Canonical sparse storage supplies sorted rows without dense expansion.

Equations

• Hex.GraphIso.Nauty.Sparse.graphRows G = List.ofFn fun (i : Fin n) => (G.nbrs i).toList

theorem Hex.GraphIso.Nauty.Sparse.graphRows_injective {n : Nat} : Function.Injective graphRows

def Hex.GraphIso.Nauty.Sparse.graphCmp {n : Nat} (G H : SparseGraph n) : Ordering

Sparse nauty's row-by-row canonical graph order.

Equations

• Hex.GraphIso.Nauty.Sparse.graphCmp G H = List.compareLex Hex.GraphIso.Nauty.Sparse.rowCmp (Hex.GraphIso.Nauty.Sparse.graphRows G) (Hex.GraphIso.Nauty.Sparse.graphRows H)

instance Hex.GraphIso.Nauty.Sparse.instTransCmpSparseGraphGraphCmp {n : Nat} : Std.TransCmp graphCmp

instance Hex.GraphIso.Nauty.Sparse.instLawfulEqCmpSparseGraphGraphCmp {n : Nat} : Std.LawfulEqCmp graphCmp

structure Hex.GraphIso.Nauty.Sparse.Key (n : Nat) : Type

A sparse leaf key, with a normalized sparse graph and its path codes. This type is distinct from the dense key and its adjacency-row ordering.

• codes : List Nat
• graph : SparseGraph n

def Hex.GraphIso.Nauty.Sparse.instDecidableEqKey.decEq {n✝ : Nat} (x✝ x✝¹ : Key n✝) : Decidable (x✝ = x✝¹)

Equations

• Hex.GraphIso.Nauty.Sparse.instDecidableEqKey.decEq { codes := a, graph := a_1 } { codes := b, graph := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instDecidableEqKey {n✝ : Nat} : DecidableEq (Key n✝)

Equations

• Hex.GraphIso.Nauty.Sparse.instDecidableEqKey = Hex.GraphIso.Nauty.Sparse.instDecidableEqKey.decEq

def Hex.GraphIso.Nauty.Sparse.Key.cmp {n : Nat} (a b : Key n) : Ordering

Codes precede graph comparison; a terminal code uses codeSentinel.

Equations

• a.cmp b = (compare a.codes b.codes).then (Hex.GraphIso.Nauty.Sparse.graphCmp a.graph b.graph)

instance Hex.GraphIso.Nauty.Sparse.Key.instTransCmpCmp {n : Nat} : Std.TransCmp cmp

instance Hex.GraphIso.Nauty.Sparse.Key.instLawfulEqCmpCmp {n : Nat} : Std.LawfulEqCmp cmp

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.Key.cmp_eq {n : Nat} {a b : Key n} : a.cmp b = Ordering.eq ↔ a = b

theorem Hex.GraphIso.Nauty.Sparse.Key.cmp_swap {n : Nat} {a b : Key n} : a.cmp b = Ordering.gt ↔ b.cmp a = Ordering.lt

theorem Hex.GraphIso.Nauty.Sparse.Key.cmp_trans {n : Nat} {a b c : Key n} (hab : a.cmp b = Ordering.gt) (hbc : b.cmp c = Ordering.gt) : a.cmp c = Ordering.gt

def Hex.GraphIso.Nauty.Sparse.Key.Le {n : Nat} (a b : Key n) : Prop

Non-strict comparison used in subtree coverage contracts.

Equations

• a.Le b = ((a.cmp b).isLE = true)

theorem Hex.GraphIso.Nauty.Sparse.Key.le_refl {n : Nat} (a : Key n) : a.Le a

theorem Hex.GraphIso.Nauty.Sparse.Key.le_trans {n : Nat} {a b c : Key n} (hab : a.Le b) (hbc : b.Le c) : a.Le c

theorem Hex.GraphIso.Nauty.Sparse.Key.le_antisymm {n : Nat} {a b : Key n} (hab : a.Le b) (hba : b.Le a) : a = b

def Hex.GraphIso.Nauty.Sparse.Key.max {n : Nat} (a b : Key n) : Key n

Select the greater key, keeping the first argument on a tie.

Equations

• a.max b = if a.cmp b = Ordering.lt then b else a

theorem Hex.GraphIso.Nauty.Sparse.Key.max_mem {n : Nat} (a b : Key n) : a.max b = a ∨ a.max b = b

theorem Hex.GraphIso.Nauty.Sparse.Key.le_max_left {n : Nat} (a b : Key n) : a.Le (a.max b)

theorem Hex.GraphIso.Nauty.Sparse.Key.le_max_right {n : Nat} (a b : Key n) : b.Le (a.max b)

theorem Hex.GraphIso.Nauty.Sparse.Key.max_le {n : Nat} {a b c : Key n} (ha : a.Le c) (hb : b.Le c) : (a.max b).Le c