structure Hex.GraphIso.Nauty.Sparse.Limited.State (n : Nat) : Type

Search-limit bookkeeping surrounds the unchanged native search state. visited counts admitted node visits; exhaustion prevents all later native policy operations from executing.

• value : Sparse.State n
• remaining : Nat
• visited : Nat
• exhausted : Bool

def Hex.GraphIso.Nauty.Sparse.Limited.map {n : Nat} (f : Sparse.State n → Sparse.State n) (s : State n) : State n

Apply a native state operation while retaining the limit counters.

Equations

• Hex.GraphIso.Nauty.Sparse.Limited.map f s = if s.exhausted = true then s else { value := f s.value, remaining := s.remaining, visited := s.visited, exhausted := s.exhausted }

def Hex.GraphIso.Nauty.Sparse.Limited.visit {n : Nat} (g : Graph n) (level numcells : Nat) (s : State n) : Nat × Nat × State n

Admit a node before calling sparse refinement. No native visit occurs after the remaining quota reaches zero.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.Limited.policy {n : Nat} : Generic.Policy (State n) n

Every non-visit callback delegates to the production sparse policy. An exhausted first-path node becomes terminal without executing native callbacks; off-path exhaustion propagates the ordinary fuel exit.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.Limited.run? {n : Nat} (maxNodes : Nat) (g : Graph n) (lab : Array Nat) (ends : List Nat) : Option (State n)

Run a node-limited native search. Exhaustion returns no search result. The empty root costs one node, matching the direct search's convention.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.Limited.runColored? {n k : Nat} (maxNodes : Nat) (G : Sparse.Colored n k) : Option (State n)

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.Limited.runPair? {n k : Nat} (maxNodes : Nat) (G H : Sparse.Colored n k) : Option (State n × State n)

Both searches share one quota; the second receives only what the first left unused. Exhaustion of either search leaves the pair inconclusive.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.Limited.Budget {n : Nat} (limit : Nat) (s : State n) : Prop

The sum of admitted visits and the remaining quota.

Equations

• Hex.GraphIso.Nauty.Sparse.Limited.Budget limit s = (s.visited + s.remaining = limit)

theorem Hex.GraphIso.Nauty.Sparse.Limited.map_budget {n limit : Nat} {s : State n} (h : Budget limit s) (f : Sparse.State n → Sparse.State n) : Budget limit (map f s)

theorem Hex.GraphIso.Nauty.Sparse.Limited.visit_budget {n limit : Nat} {s : State n} (h : Budget limit s) (g : Graph n) (level numcells : Nat) : Budget limit (visit g level numcells s).snd.snd

theorem Hex.GraphIso.Nauty.Sparse.Limited.visit_exhausted {n : Nat} (g : Graph n) (level numcells : Nat) (s : State n) (h : s.remaining = 0) : visit g level numcells s = (n, 0, { value := s.value, remaining := s.remaining, visited := s.visited, exhausted := true })

theorem Hex.GraphIso.Nauty.Sparse.Limited.run?_zero {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : run? 0 g lab ends = none

theorem Hex.GraphIso.Nauty.Sparse.Limited.runColored?_zero {n k : Nat} (G : Sparse.Colored n k) : runColored? 0 G = none