def Hex.GraphIso.Nauty.Sparse.FollowsPerm {n : Nat} (G : SparseGraph n) (store : Array Int) (base : Nat) (root : RefineSt n) (level : Nat) (current : RefineSt n) : Prop

A native saved-target history whose endpoint may differ from the current label order inside cells, as happens after sibling recovery.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.FollowsPerm.refl {n : Nat} (G : SparseGraph n) (store : Array Int) (level : Nat) (st : RefineSt n) : FollowsPerm G store level st level st

theorem Hex.GraphIso.Nauty.Sparse.FollowsPerm.setLab {n : Nat} {G : SparseGraph n} {store : Array Int} {base level : Nat} {root current : RefineSt n} (h : FollowsPerm G store base root level current) (lab : Array Nat) (hc : cellsPerm current.ptn level lab current.lab) : FollowsPerm G store base root level { lab := lab, ptn := current.ptn, active := current.active, queue := current.queue, cellstart := current.cellstart, cellend := current.cellend, indexed := current.indexed, hits := current.hits, marks := current.marks, vmarks := current.vmarks, stamp := current.stamp, numcells := current.numcells, longcode := current.longcode }

Reordering a recovered parent's cells preserves its recorded descent.

theorem Hex.GraphIso.Nauty.Sparse.FollowsPerm.set_after {n : Nat} {G : SparseGraph n} {store : Array Int} {base level : Nat} {root current : RefineSt n} (h : FollowsPerm G store base root level current) {slot : Nat} (hs : level ≤ slot) (value : Int) : FollowsPerm G (store.set! slot value) base root level current

theorem Hex.GraphIso.Nauty.Sparse.FollowsPerm.leaf {n : Nat} {G : SparseGraph n} {store : Array Int} {base level : Nat} {root current : RefineSt n} (h : FollowsPerm G store base root level current) (hr : RefineSt.Ready G base root) (hc : RefineSt.Ready G level current) (hd : discreteAt current.ptn level n = true) : ∃ (leaf : RefineSt n), ∃ (path : List (Nat × Nat)), DescPath G base root path level leaf ∧ Targets store base (List.map Prod.fst path) ∧ leaf.lab = current.lab ∧ leaf.ptn = current.ptn

At a discrete endpoint the history label is the literal current label.

theorem Hex.GraphIso.Nauty.Sparse.FollowsPerm.child {n : Nat} {G : SparseGraph n} {store : Array Int} {base level : Nat} {root current : RefineSt n} (h : FollowsPerm G store base root level current) (hr : RefineSt.Ready G base root) (hc : RefineSt.Ready G level current) {tc len o : Nat} (hcell : IsCell current.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (htc : store[level]! = Int.ofNat tc) (scratch : Scratch) (hs : Scratch.Bounded n scratch) : FollowsPerm G store base root (level + 1) (RefineSt.child (Graph.ofGraph G) level current tc current.lab[tc + o]! scratch)

Individualization and native cached refinement extend a stored-target history even when the current parent has a different within-cell order.