theorem
Hex.GraphIso.Nauty.Sparse.Pending.touched
{lab ptn starts ends before marks cells : Array Nat}
{n stamp level : Nat}
{seen : List Nat}
(h : Touched n stamp before marks cells (List.map (fun (v : Nat) => starts[v]!) seen))
(hi : Index.Valid n lab ptn level starts ends)
:
Pending n level (fun (a : Nat) => List.count a seen) ends cells.toList lab ptn
Marking alone identifies every nontrivial cell that can have a nonzero native neighbour count. No interpretation of retained scratch counts is needed.
theorem
Hex.GraphIso.Nauty.Sparse.Pending.binary
{key : Nat → Nat}
{ends lab out ptn : Array Nat}
{n level first cut last : Nat}
{todo : List Nat}
(h : Pending n level key ends (first :: todo) lab ptn)
(hc : IsCell ptn level first (last - first))
(hf : first ≤ cut)
(hl : cut ≤ last)
(hb : last ≤ ptn.size)
(he : last = ends[first]! + 1)
(ho : ∀ (q : Nat), q < first ∨ last ≤ q → out[q]! = lab[q]!)
(hleft : ∀ (q r : Nat), first ≤ q → q < cut → first ≤ r → r < cut → key out[q]! = key out[r]!)
(hright : ∀ (q r : Nat), cut ≤ q → q < last → cut ≤ r → r < last → key out[q]! = key out[r]!)
:
A binary split discharges its cell once both predicate classes have constant keys. The equal-endpoint cases perform no boundary write.
theorem
Hex.GraphIso.Nauty.Sparse.Pending.compact
{key : Nat → Nat}
{p : Nat → Bool}
{ends before lab hit out ptn : Array Nat}
{n level first cut last : Nat}
{todo : List Nat}
(h : Pending n level key ends (first :: todo) before ptn)
(hc : Compact before p first last (List.take (last - first) (List.drop first before.toList)) lab hit cut)
(hr : Fill lab hit.toList.reverse cut hit.toList.reverse.length out)
(hp : before.toList.Perm (List.range n))
(hs : ptn.size = n)
(hcell : IsCell ptn level first (last - first))
(he : last = ends[first]! + 1)
(hk : ∀ (v w : Nat), v < n → w < n → p v = p w → key v = key w)
:
The executed compaction and reverse fill provide the two constant classes required by the binary-cell argument.