theorem Hex.GraphIso.Nauty.recover_ptn_congr {n : Nat} {κ : Type} (inf level : Nat) (s t : SearchState n κ) (hs : s.ptn.size = n) (ht : t.ptn.size = n) (hlow : ∀ (q : Nat), s.ptn[q]! ≤ level ∨ t.ptn[q]! ≤ level → t.ptn[q]! = s.ptn[q]!) : (recover inf level t).ptn = (recover inf level s).ptn

Recovery identifies two bounded partition arrays when their values agree at every boundary visible at the receiving level. Storage is arbitrary.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_low {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hb : s.cellend[first]! < n) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (parent : Nat) (hp : parent < level) (q : Nat) (hq : s.ptn[q]! ≤ parent ∨ (splitCounts level first distance s).ptn[q]! ≤ parent) : (splitCounts level first distance s).ptn[q]! = s.ptn[q]!

Count splitting retains every boundary visible to an ancestor, from either side of the refinement.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_recover {n : Nat} {κ : Type} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hb : s.cellend[first]! < n) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (inf parent : Nat) (hp : parent < level) (st : SearchState n κ) : (recover inf parent { lab := st.lab, ptn := (splitCounts level first distance s).ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace, workperm := st.workperm }).ptn = (recover inf parent { lab := st.lab, ptn := s.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace, workperm := st.workperm }).ptn

The actual recovery operation erases this descendant count split while retaining its ancestor partition. This applies to the sparse canonical store as well as to every other shared search-storage type.