theorem
Hex.GraphIso.Nauty.Sparse.Binary.Result.cache
{n level first cut last : Nat}
{lab starts before : Array Nat}
{p : Nat → Bool}
{seen : List Nat}
{temp hit oldstarts : Array Nat}
{s r : RefineSt n}
(h : Result level first cut last s lab starts r)
(hc : Compact before p first last seen temp hit cut)
(hseen : seen = List.take (last - first) (List.drop first before.toList))
(hf : Fill temp hit.toList.reverse cut hit.toList.reverse.length lab)
(hw : Index.Writes n oldstarts starts hit.toList.reverse cut)
(hp : before.toList.Perm (List.range n))
(hptn : s.ptn.size = n)
(hi : Index.Valid n before s.ptn level oldstarts s.cellend)
(hcell : IsCell s.ptn level first (last - first))
(hn : first + 1 < last)
:
Index.Valid n r.lab r.ptn level r.cellstart r.cellend
The actual binary finalization writes exactly the cache justified by compaction and reverse fill, including both uniform predicate classes.