theorem Hex.GraphIso.Nauty.Sparse.Compact.kept_segment {before : Array Nat} {p : Nat → Bool} {first last : Nat} {seen : List Nat} {lab hit : Array Nat} {cut : Nat} {out : Array Nat} (h : Compact before p first last seen lab hit cut) (hr : Fill lab hit.toList.reverse cut hit.toList.reverse.length out) : segN out first (cut - first) = List.filter (fun (v : Nat) => !p v) seen

The first restored fragment is literally the retained source order.

theorem Hex.GraphIso.Nauty.Sparse.Compact.hit_segment {before : Array Nat} {p : Nat → Bool} {first last : Nat} {seen : List Nat} {lab hit : Array Nat} {cut : Nat} {out : Array Nat} (h : Compact before p first last seen lab hit cut) (hlen : seen.length = last - first) (hr : Fill lab hit.toList.reverse cut hit.toList.reverse.length out) : segN out cut (last - cut) = (List.filter p seen).reverse

The second restored fragment is literally the reverse of the collected source order, as in sparse nauty's descending hit-buffer traversal.

theorem Hex.GraphIso.Nauty.Sparse.Compact.fragments_map {before : Array Nat} {p : Nat → Bool} {first last : Nat} {seen : List Nat} {lab hit : Array Nat} {cut : Nat} {other : Array Nat} {q : Nat → Bool} {visits : List Nat} {temp collected : Array Nat} {next : Nat} {out final : Array Nat} (f : Nat → Nat) (hs : Compact before p first last seen lab hit cut) (ht : Compact other q first last visits temp collected next) (hfill : Fill lab hit.toList.reverse cut hit.toList.reverse.length out) (hfill' : Fill temp collected.toList.reverse next collected.toList.reverse.length final) (hlen : seen.length = last - first) (hp : visits.Perm (List.map f seen)) (hk : ∀ (v : Nat), v ∈ seen → q (f v) = p v) : cut = next ∧ hit.size = collected.size ∧ (segN final first (next - first)).Perm (List.map f (segN out first (cut - first))) ∧ (segN final next (last - next)).Perm (List.map f (segN out cut (last - cut)))

Both fragments of the executed compaction and reverse fill transport as vertex multisets, with identical cut and collected-hit count.