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

Retain an attaining label while comparing the full sparse keys.

Equations

• Hex.GraphIso.Nauty.Sparse.SpecLeaf.max G a b = if (Hex.GraphIso.Nauty.Sparse.SpecLeaf.key G a).cmp (Hex.GraphIso.Nauty.Sparse.SpecLeaf.key G b) = Ordering.lt then b else a

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

theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.key_max {n : Nat} (G : SparseGraph n) (a b : SpecLeaf n) : key G (max G a b) = (key G a).max (key G b)

def Hex.GraphIso.Nauty.Sparse.SpecLeaf.best {n : Nat} (G : SparseGraph n) (first : SpecLeaf n) (rest : List (SpecLeaf n)) : SpecLeaf n

The first greatest leaf in enumeration order.

Equations

• Hex.GraphIso.Nauty.Sparse.SpecLeaf.best G first rest = List.foldl (Hex.GraphIso.Nauty.Sparse.SpecLeaf.max G) first rest

theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.best_mem {n : Nat} (G : SparseGraph n) (first : SpecLeaf n) (rest : List (SpecLeaf n)) : best G first rest ∈ first :: rest

theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.best_bound {n : Nat} (G : SparseGraph n) (first : SpecLeaf n) (rest : List (SpecLeaf n)) (leaf : SpecLeaf n) : leaf ∈ first :: rest → (key G leaf).Le (key G (best G first rest))

def Hex.GraphIso.Nauty.Sparse.specBest {n k : Nat} (G : Sparse.Colored n k) : SpecLeaf n

A reachable maximum of the complete finite sparse tree. Nonemptiness supplies the initial candidate without an arbitrary fallback.

Equations

• Hex.GraphIso.Nauty.Sparse.specBest G = Hex.GraphIso.Nauty.Sparse.SpecLeaf.best G.graph ((Hex.GraphIso.Nauty.Sparse.rootLeaves G).head ⋯) (Hex.GraphIso.Nauty.Sparse.rootLeaves G).tail

def Hex.GraphIso.Nauty.Sparse.canonSpecKey {n k : Nat} (G : Sparse.Colored n k) : Key n

The sparse declarative maximum, in sparse nauty's own key order.

Equations

• Hex.GraphIso.Nauty.Sparse.canonSpecKey G = Hex.GraphIso.Nauty.Sparse.SpecLeaf.key G.graph (Hex.GraphIso.Nauty.Sparse.specBest G)

def Hex.GraphIso.Nauty.Sparse.canonSpecLabel {n k : Nat} (G : Sparse.Colored n k) : Label n

A labelling attaining the sparse declarative maximum.

Equations

• Hex.GraphIso.Nauty.Sparse.canonSpecLabel G = (Hex.GraphIso.Nauty.Sparse.specBest G).label

theorem Hex.GraphIso.Nauty.Sparse.specBest_mem {n k : Nat} (G : Sparse.Colored n k) : specBest G ∈ rootLeaves G

theorem Hex.GraphIso.Nauty.Sparse.canonSpecKey_bound {n k : Nat} (G : Sparse.Colored n k) {leaf : SpecLeaf n} (h : leaf ∈ rootLeaves G) : (SpecLeaf.key G.graph leaf).Le (canonSpecKey G)

theorem Hex.GraphIso.Nauty.Sparse.canonSpecLabel_attains {n k : Nat} (G : Sparse.Colored n k) : (canonSpecKey G).graph = G.graph.relabel (canonSpecLabel G).perm

theorem Hex.GraphIso.Nauty.Sparse.canonSpecKey_eq {n k : Nat} (G : Sparse.Colored n k) {leaf : SpecLeaf n} (hm : leaf ∈ rootLeaves G) (hb : ∀ (other : SpecLeaf n), other ∈ rootLeaves G → (SpecLeaf.key G.graph other).Le (SpecLeaf.key G.graph leaf)) : canonSpecKey G = SpecLeaf.key G.graph leaf

A reachable upper bound is exactly the declarative maximum.