theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.discrete {n : Nat} {σ : Renaming n} {level : Nat} {s t : RefineSt n} (h : Equiv σ level s t) (hs : s.ptn.size = n) (hend : s.ptn[n - 1]! ≤ level) (hp : s.lab.size = n) (hq : t.lab.size = n) (hd : discreteAt s.ptn level n = true) : t.lab = Array.map σ.toFun s.lab

Discrete ordered-cell equivalence determines the whole output label array, including when earlier nontrivial cells used different tie orders.

def Hex.GraphIso.Nauty.Sparse.SpecLeaf.map {n : Nat} (p : Perm n) (leaf : SpecLeaf n) : SpecLeaf n

Transport a specification leaf's vertices, retaining its path codes.

Equations

• Hex.GraphIso.Nauty.Sparse.SpecLeaf.map p leaf = { codes := leaf.codes, label := { perm := p.comp leaf.label.perm } }

theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.map_prepend {n : Nat} (p : Perm n) (code : Nat) (leaf : SpecLeaf n) : map p (prepend code leaf) = prepend code (map p leaf)

theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.map_key {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) (leaf : SpecLeaf n) : key H (map p leaf) = key G leaf

A transported leaf attains the identical sparse key under an isomorphism, including every normalized native adjacency row.

theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.parse_map {n : Nat} (p : Perm n) {lab : Array Nat} {label : Label n} (hp : lab.toList.Perm (List.range n)) (hl : Label.ofArray? n lab = some label) : Label.ofArray? n (Array.map (renamingOf p).toFun lab) = some { perm := p.comp label.perm }

The executed label parser returns the transported typed label when its input array is renamed.