theorem Hex.GraphIso.Nauty.Sparse.breakout_perm {n level tc len o : Nat} {lab ptn : Array Nat} (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hc : IsCell ptn level tc len) (hb : tc + len ≤ n) (ho : o < len) : (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst.toList.Perm (List.range n)

Individualizing a member of a bounded partition cell preserves the whole label permutation, using the executed rotation's cell-content theorem.

theorem Hex.GraphIso.Nauty.Sparse.child_fields {n : Nat} (first : Bool) (level tc tv : Nat) (s : State n) : have t := Generic.Policy.child first level tc tv s; t.lab = (breakout n s.lab s.ptn (level + 1) tc tv).fst ∧ t.ptn = s.ptn.set! tc (level + 1) ∧ t.active = VSet.empty.insert tc

Partition projections of the actual sparse child policy. Cache invalidation and first-path bookkeeping leave individualization unchanged.

theorem Hex.GraphIso.Nauty.Sparse.child_entry {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 t := Generic.Policy.child first level tc s.lab[tc + o]! s; t.lab.toList.Perm (List.range n) ∧ NodeOk n (level + 1) t.lab t.ptn t.active ∧ Scratch.Valid n t.lab t.ptn (level + 1) t.canong.scratch ∧ numcells + 1 = bcount t.ptn (level + 1) n ∧ CertInv (Graph.context G) (level + 1) { lab := t.lab, ptn := t.ptn, active := t.active, numcells := numcells + 1, hint := 0, maxpos := 0, longcode := numcells + 1 }

The executed child policy supplies all entry facts for its next refinement, including the certificate derived from the parent's equitability.