structure Hex.GraphIso.Nauty.Sparse.CountTrace.Control (n : Nat) : Type

The observable control fields of count splitting. This projection is used only in proofs; the executable retains its original working state.

• active : VSet n
• queue : Array Nat
• code : Nat

def Hex.GraphIso.Nauty.Sparse.CountTrace.control {n : Nat} (s : RefineSt n) : Control n

Equations

• Hex.GraphIso.Nauty.Sparse.CountTrace.control s = { active := s.active, queue := s.queue, code := s.longcode }

def Hex.GraphIso.Nauty.Sparse.CountTrace.Control.hash {n : Nat} (s : Control n) (v : Nat) : Control n

Equations

• s.hash v = { active := s.active, queue := s.queue, code := Hex.GraphIso.Nauty.mash s.code v }

def Hex.GraphIso.Nauty.Sparse.CountTrace.Control.push {n : Nat} (s : Control n) (v : Nat) : Control n

Equations

• s.push v = { active := s.active.insert v, queue := s.queue.push v, code := s.code }

def Hex.GraphIso.Nauty.Sparse.CountTrace.Control.advance {n : Nat} (s : Control n) (distance : Bool) (k value : Nat) : Control n

The exact hash and insertion performed when entering a later count run.

Equations

• s.advance distance k value = if distance = true then (if distance = true then s.hash k else s).push (k + 1) else ((if distance = true then s.hash k else s).push (k + 1)).hash value

def Hex.GraphIso.Nauty.Sparse.CountTrace.Control.choose {n : Nat} (s : Control n) (pos : Option Nat) (big size : Nat) : Option Nat × Nat

The executed update of the saved largest fragment, including the singleton guard and strict comparison that retains the earlier tie.

Equations

• s.choose pos big size = if (size == 1) = true then (pos, big) else if big < size then (some (s.queue.size - 1), size) else (pos, big)

def Hex.GraphIso.Nauty.Sparse.CountTrace.Control.finish {n : Nat} (s : Control n) (distance : Bool) (first : Nat) (pos : Option Nat) : Control n

Final largest-fragment replacement, with its distance-only hash.

Equations

• One or more equations did not get rendered due to their size.
• s.finish distance first none = s

inductive Hex.GraphIso.Nauty.Sparse.CountTrace.Tail {n : Nat} (distance : Bool) (lab hits : Array Nat) (first last : Nat) : Nat → Control n → Option Nat → Nat → Control n → Prop

A derivation of the actual tail scan's control transitions. Each step consumes one maximal constant-count run; completion includes replacement. This relation does not run another refinement algorithm.

• done {n : Nat} {distance : Bool} {lab hits : Array Nat} {first last k : Nat} {s : Control n} {pos : Option Nat} {big : Nat} (hk : last ≤ k + 1) : Tail distance lab hits first last k s pos big (s.finish distance first pos)
• step {n : Nat} {distance : Bool} {lab hits : Array Nat} {first last k b : Nat} {out s : Control n} {pos : Option Nat} {big : Nat} (hk : k + 1 < last) (hr : Index.Run lab hits (k + 1) (last - 1) (k + 1) b) (ht : Tail distance lab hits first last b (s.advance distance k hits[lab[k + 1]!]!) ((s.advance distance k hits[lab[k + 1]!]!).choose pos big (b - (k + 1) + 1)).fst ((s.advance distance k hits[lab[k + 1]!]!).choose pos big (b - (k + 1) + 1)).snd out) : Tail distance lab hits first last k s pos big out

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Tail.deterministic {distance : Bool} {lab hits : Array Nat} {first last k n✝ : Nat} {s : Control n✝} {pos : Option Nat} {big : Nat} {out other : Control n✝} (h : Tail distance lab hits first last k s pos big out) (h' : Tail distance lab hits first last k s pos big other) : out = other

A fixed count sequence determines all tail hashes, queue entries and the saved-largest tie rule uniquely.

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Tail.congr {distance : Bool} {lab hits : Array Nat} {first last k n✝ : Nat} {s : Control n✝} {pos : Option Nat} {big : Nat} {out : Control n✝} {keys vertices : Array Nat} (h : Tail distance lab hits first last k s pos big out) (hk : ∀ (q : Nat), k + 1 ≤ q → q < last → hits[lab[q]!]! = keys[vertices[q]!]!) : Tail distance vertices keys first last k s pos big out

Equal count sequences transport the complete tail trace, without requiring literal equality of the vertex arrays.