def Hex.GraphIso.Nauty.Sparse.Join.qualifies (full : List Nat) (size : Nat → Nat) (k : Nat) : Bool

A join meets a cell but does not meet all of its vertices.

Equations

• Hex.GraphIso.Nauty.Sparse.Join.qualifies full size k = decide (0 < List.count k full ∧ List.count k full < size k)

structure Hex.GraphIso.Nauty.Sparse.Join.Sweep (keys full done : List Nat) (size : Nat → Nat) (hits : Array Nat) (count : Nat) : Prop

The second neighbour scan clears each cell after its first occurrence and accumulates one contribution per qualifying cell.

• bound (k : Nat) : k ∈ keys → k < hits.size
• get (k : Nat) : k ∈ keys → hits[k]! = if k ∈ done then 0 else List.count k full
• total : count = marked keys done (qualifies full size)

theorem Hex.GraphIso.Nauty.Sparse.Join.Sweep.initial {keys full : List Nat} {hits : Array Nat} (size : Nat → Nat) (h : Counts keys full hits) : Sweep keys full [] size hits 0

theorem Hex.GraphIso.Nauty.Sparse.Join.Sweep.clear {keys full done : List Nat} {size : Nat → Nat} {hits : Array Nat} {count k : Nat} (h : Sweep keys full done size hits count) (hn : keys.Nodup) (hk : k ∈ keys) (hf : k ∈ full) : Sweep keys full (done ++ [k]) size (hits.set! k 0) (count + if 0 < hits[k]! ∧ hits[k]! < size k then 1 else 0)

The actual test-and-clear operation counts only the first occurrence, including when a cell occurs several times in the adjacency row.

theorem Hex.GraphIso.Nauty.Sparse.Join.Sweep.skip {keys full done : List Nat} {size : Nat → Nat} {hits : Array Nat} {count k : Nat} (h : Sweep keys full done size hits count) (hk : ¬k ∈ keys) : Sweep keys full (done ++ [k]) size hits count

theorem Hex.GraphIso.Nauty.Sparse.Join.Sweep.finish {keys full : List Nat} {size : Nat → Nat} {hits : Array Nat} {count : Nat} (h : Sweep keys full full size hits count) : count = List.countP (qualifies full size) keys ∧ ∀ (k : Nat), k ∈ keys → hits[k]! = 0

At completion the result is the number of nontrivial joins, and all used count entries are zero for the next representative vertex.