theorem Hex.GraphIso.Nauty.Sparse.child_match {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j) {level : Nat} {s t : RefineSt n} (hs : RefineSt.Ready G level s) (ht : RefineSt.Ready H level t) (hp : t.ptn = s.ptn) (hnc : t.numcells = s.numcells) (he : cellsPerm s.ptn level t.lab (Array.map (renamingOf p).toFun s.lab)) {tc len o : Nat} (hc : IsCell s.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (a b : Scratch) (ha : Scratch.Bounded n a) (hb' : Scratch.Bounded n b) : ∃ (j : Nat), j < len ∧ t.lab[tc + j]! = (renamingOf p).toFun s.lab[tc + o]! ∧ RefineSt.Equiv (renamingOf p) (level + 1) (RefineSt.child (Graph.ofGraph G) level s tc s.lab[tc + o]! a) (RefineSt.child (Graph.ofGraph H) level t tc t.lab[tc + j]! b)

Corresponding members of a cell give equivalent literal cached child calls. Both scratch arguments remain independent; tied label order may change the selected offset but not the refined partition or code.

theorem Hex.GraphIso.Nauty.Sparse.child_equiv {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j) {level : Nat} {s t : RefineSt n} (hs : RefineSt.Ready G level s) (ht : RefineSt.Ready H level t) (hp : t.ptn = s.ptn) (hnc : t.numcells = s.numcells) (he : cellsPerm s.ptn level t.lab (Array.map (renamingOf p).toFun s.lab)) {tc len a b : Nat} (hc : IsCell s.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ha : a < len) (hb' : b < len) (scratch other : Scratch) (hsc : Scratch.Bounded n scratch) (hoc : Scratch.Bounded n other) (hmove : t.lab[tc + b]! = (renamingOf p).toFun s.lab[tc + a]!) : RefineSt.Equiv (renamingOf p) (level + 1) (RefineSt.child (Graph.ofGraph G) level s tc s.lab[tc + a]! scratch) (RefineSt.child (Graph.ofGraph H) level t tc t.lab[tc + b]! other)

Specifying both corresponding vertices identifies the exact pair of native cached child calls, independently of their offsets and scratch.