structure Hex.GraphIso.Nauty.Sparse.Queue (n : Nat) (dist queue : Array Nat) (head tail : Nat) : Prop

The allocated BFS queue contains every discovered vertex exactly once. Its distance order and frontier band justify both append operations and the early exit when all vertices have been discovered.

• dist_size : dist.size = n
• queue_size : queue.size = n
• head_le : head ≤ tail
• tail_le : tail ≤ n
• vertex (i : Nat) : i < tail → queue[i]! < n
• injective (i j : Nat) : i < tail → j < tail → queue[i]! = queue[j]! → i = j
• bound (v : Nat) : v < n → dist[v]! ≤ n
• found (v : Nat) : v < n → (dist[v]! < n ↔ ∃ (i : Nat), i < tail ∧ queue[i]! = v)
• index (i : Nat) : i < tail → dist[queue[i]!]! ≤ i
• sorted (i j : Nat) : i ≤ j → j < tail → dist[queue[i]!]! ≤ dist[queue[j]!]!
• band (i j : Nat) : head ≤ i → i < tail → j < tail → dist[queue[j]!]! ≤ dist[queue[i]!]! + 1

theorem Hex.GraphIso.Nauty.Sparse.Queue.set_read (a : Array Nat) (i value j : Nat) (hj : j < a.size) : (a.set! i value)[j]! = if i = j then value else a[j]!

theorem Hex.GraphIso.Nauty.Sparse.Queue.finite {n : Nat} {dist queue : Array Nat} {head tail : Nat} (h : Queue n dist queue head tail) {i : Nat} (hi : i < tail) : dist[queue[i]!]! < n

theorem Hex.GraphIso.Nauty.Sparse.Queue.fresh {n : Nat} {dist queue : Array Nat} {head tail v : Nat} (h : Queue n dist queue head tail) (_hv : v < n) (hd : dist[v]! = n) {i : Nat} (hi : i < tail) : queue[i]! ≠ v

theorem Hex.GraphIso.Nauty.Sparse.Queue.room {n : Nat} {dist queue : Array Nat} {head tail v : Nat} (h : Queue n dist queue head tail) (hv : v < n) (hd : dist[v]! = n) : tail < n

An undiscovered vertex forces a free slot in the fixed queue.

theorem Hex.GraphIso.Nauty.Sparse.Queue.initial {n : Nat} (root : Fin n) : Queue n ((Array.replicate n n).set! (↑root) 0) ((Array.replicate n 0).set! 0 ↑root) 0 1

theorem Hex.GraphIso.Nauty.Sparse.Queue.add {n : Nat} {dist queue : Array Nat} {head tail v : Nat} (h : Queue n dist queue head tail) (hh : head < tail) (hv : v < n) (hd : dist[v]! = n) (hn : dist[queue[head]!]! + 1 < n) : Queue n (dist.set! v (dist[queue[head]!]! + 1)) (queue.set! tail v) head (tail + 1)

Discovering an unseen neighbour appends it once and gives it the next distance after the current head. The head stays fixed during its row scan.

theorem Hex.GraphIso.Nauty.Sparse.Queue.advance {n : Nat} {dist queue : Array Nat} {head tail : Nat} (h : Queue n dist queue head tail) (hh : head < tail) : Queue n dist queue (head + 1) tail

Completing one row advances the queue head without changing entries.