theorem
Hex.GraphIso.Nauty.Sparse.CountTrace.uniform_iff
{first last : Nat}
(lab out hits keys : Array Nat)
(hf : first < last)
(hp :
(List.map (fun (v : Nat) => hits[v]!) (segN lab first (last - first))).Perm
(List.map (fun (v : Nat) => keys[v]!) (segN out first (last - first))))
:
Uniformity depends on the cell's count multiset, including when its first vertex changes under a permutation.
theorem
Hex.GraphIso.Nauty.Sparse.CountTrace.Result.control_eq
{n : Nat}
{distance : Bool}
{first last : Nat}
{lab : Array Nat}
{c : Control n}
{out : Array Nat}
{d : Control n}
{s t : RefineSt n}
(hs : Result distance first last s lab c)
(ht : Result distance first last t out d)
(hc : control s = control t)
(hu :
(∀ (q : Nat), first ≤ q → q < last → s.hits[s.lab[q]!]! = s.hits[s.lab[first]!]!) ↔ ∀ (q : Nat), first ≤ q → q < last → t.hits[t.lab[q]!]! = t.hits[t.lab[first]!]!)
(hk : ∀ (q : Nat), first ≤ q → q < last → s.hits[lab[q]!]! = t.hits[out[q]!]!)
:
Equal ordered counts and initial control determine the complete split trace's final hash, active set and ordered queue.