structure Hex.GraphIso.Nauty.Generic.Trivial.Frame (n : Nat) : Type

A partition, its path codes, and the key it would have as a leaf.

• partition : RefineSt n
• codes : List Nat
• candidate : Key n

structure Hex.GraphIso.Nauty.Generic.Trivial.State (n : Nat) : Type

The exhaustive traversal's current frame, saved parents, and incumbent.

• frame : Frame n
• parents : List (Frame n)
• best : Option (Key n)

def Hex.GraphIso.Nauty.Generic.Trivial.visit {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : State n) : State n

Refine the current partition and append its code to the current path.

Equations

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

def Hex.GraphIso.Nauty.Generic.Trivial.positions {n : Nat} (len : Nat) : VSet n

The target positions, enumerated in increasing offset order.

Equations

• Hex.GraphIso.Nauty.Generic.Trivial.positions len = Hex.GraphIso.Nauty.VSet.ofList (List.range len)

def Hex.GraphIso.Nauty.Generic.Trivial.child {n : Nat} (level tc offset : Nat) (st : State n) : State n

Individualize an offset of the current target cell, retaining its parent frame.

Equations

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

def Hex.GraphIso.Nauty.Generic.Trivial.recover {n : Nat} (st : State n) : State n

Restore the saved parent while retaining the child's incumbent. The exhaustive policy returns to its immediate parent; each recovery therefore consumes exactly one frame pushed by child.

Equations

• Hex.GraphIso.Nauty.Generic.Trivial.recover st = match st.parents with | [] => st | frame :: parents => { frame := frame, parents := parents, best := st.best }

def Hex.GraphIso.Nauty.Generic.Trivial.install {n : Nat} (st : State n) : State n

Install the current leaf into the incumbent.

Equations

• Hex.GraphIso.Nauty.Generic.Trivial.install st = { frame := st.frame, parents := st.parents, best := some (Hex.GraphIso.Nauty.incMax st.best st.frame.candidate) }

@[instance_reducible]

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

The exhaustive policy uses the specification's target selector and never removes a target position or returns past its immediate parent. Sweep entries are offsets in the target cell.

Equations

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

theorem Hex.GraphIso.Nauty.Generic.Trivial.mem_positions {n len : Nat} (hlen : len ≤ n) (v : Nat) : (positions len).mem v = decide (v < len)

A valid offset set has precisely its requested interval as members.

theorem Hex.GraphIso.Nauty.Generic.Trivial.next_positions {n len : Nat} (hlen : len ≤ n) (cursor : Option Nat) : (positions len).nextElem cursor = if VSet.scanStart cursor < len then some (VSet.scanStart cursor) else none

The next offset is the scan start whenever it is still within the target.

theorem Hex.GraphIso.Nauty.Generic.Trivial.recover_child {n : Nat} (ctx : Ctx n) (level tc offset : Nat) (st : State n) (best : Option (Key n)) : recover (have __src := visit ctx (level + 1) (st.frame.partition.numcells + 1) (child level tc offset st); { frame := __src.frame, parents := __src.parents, best := best }) = { frame := st.frame, parents := st.parents, best := best }

Completing a child restores exactly its parent frame and new incumbent.

inductive Hex.GraphIso.Nauty.Generic.Trivial.Complete {n : Nat} (ctx : Ctx n) (tcLevel : Nat) : Nat → Nat → RefineSt n → Prop

Sufficient depth for the exhaustive refinement tree. The interval bounds ensure every target offset is representable by the policy's bitset.

• leaf {n : Nat} {ctx : Ctx n} {tcLevel fuel level : Nat} {p : RefineSt n} (discrete : discreteAt (refine ctx level p.lab p.ptn p.active p.numcells).ptn level n = true) : Complete ctx tcLevel (fuel + 1) level p
• branch {n : Nat} {ctx : Ctx n} {tcLevel fuel level : Nat} {p : RefineSt n} (nondiscrete : discreteAt (refine ctx level p.lab p.ptn p.active p.numcells).ptn level n = false) (bounded : let r := refine ctx level p.lab p.ptn p.active p.numcells; (specMaketargetcell ctx r.lab r.ptn level tcLevel).snd.snd ≤ n) (children : let r := refine ctx level p.lab p.ptn p.active p.numcells; let t := specMaketargetcell ctx r.lab r.ptn level tcLevel; ∀ (o : Nat), o < t.snd.snd → Complete ctx tcLevel fuel (level + 1) (child level t.fst o { frame := { partition := r, codes := [], candidate := default }, parents := [], best := none }).frame.partition) : Complete ctx tcLevel (fuel + 1) level p