theorem Hex.GraphIso.Nauty.Sparse.visit_equitable {n : Nat} (G : SparseGraph n) (level numcells : Nat) (s : State n) (hp : s.lab.toList.Perm (List.range n)) (h : NodeOk n level s.lab s.ptn s.active) (hb : Scratch.Bounded n s.canong.scratch) (hc : numcells = bcount s.ptn level n) (hinv : CertInv (Graph.context G) level { lab := s.lab, ptn := s.ptn, active := s.active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }) : have t := (visit (Graph.ofGraph G) level numcells s).snd.snd; Equitable (Graph.context G) level t.lab t.ptn

The production visit runs the certified sparse refinement.

theorem Hex.GraphIso.Nauty.Sparse.child_equitable {n : Nat} (G : SparseGraph n) (first : Bool) (level numcells tc len o : Nat) (s : State n) (hp : s.lab.toList.Perm (List.range n)) (h : NodeOk n level s.lab s.ptn s.active) (hb : Scratch.Bounded n s.canong.scratch) (hl : level ≤ n) (hcount : numcells = bcount s.ptn level n) (heq : Equitable (Graph.context G) level s.lab s.ptn) (hc : IsCell s.ptn level tc len) (hr : tc + len ≤ n) (hn : 1 < len) (ho : o < len) : have child := Generic.Policy.child first level tc s.lab[tc + o]! s; have result := visit (Graph.ofGraph G) (level + 1) (numcells + 1) child; result.snd.snd.lab.toList.Perm (List.range n) ∧ NodeOk n (level + 1) result.snd.snd.lab result.snd.snd.ptn result.snd.snd.active ∧ Scratch.Valid n result.snd.snd.lab result.snd.snd.ptn (level + 1) result.snd.snd.canong.scratch ∧ result.fst = bcount result.snd.snd.ptn (level + 1) n ∧ Equitable (Graph.context G) (level + 1) result.snd.snd.lab result.snd.snd.ptn

Every individualized target-cell member has an equitable child after the actual sparse policy's cache invalidation and production visit.