theorem Hex.GraphIso.Nauty.frame_local {n k : Nat} {G : Colored n k} {level numcells : Nat} {st out : Search n} (hok : SearchOk G level numcells st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) (hf : out.firstlab = st.firstlab ∨ out.firstlab = st.lab) (hc : out.canonlab = st.canonlab ∨ out.canonlab = st.lab) : Generic.Local G (fun (st : Search n) => st) level numcells st out

A frame-preserving search operation satisfies the local reach rules.

theorem Hex.GraphIso.Nauty.maketargetcell_target {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (hint : Int) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (hnc : numcells < n) : have r := maketargetcell ctx st.lab st.ptn level tcLevel hint; Generic.Target (fun (st : Search n) => st) level r.fst r.snd.fst st

A target constructed from a live partition has the cell membership required by the generic sweep, for any target hint.

theorem Hex.GraphIso.Nauty.target_empty {n : Nat} (level tc : Nat) (st : Search n) : Generic.Target (fun (st : Search n) => st) level tc VSet.empty st

The empty target set requires no cell witness.

theorem Hex.GraphIso.Nauty.chooseTarget_target {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (first : Bool) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) : have r := chooseTarget first ctx tcLevel level numcells st; Generic.Target (fun (st : Search n) => st) level r.fst.toNat r.snd.fst r.snd.snd.snd

Any selected target is a nontrivial cell of the current partition. Bookkeeping performed while selecting it does not change that partition.

theorem Hex.GraphIso.Nauty.reachPolicy {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel : Nat) (hn0 : 0 < n) : Generic.ReachPolicy G ctx (n + 2) tcLevel fun (st : Search n) => st

The concrete search meets every local partition rule of the generic search. No automorphism or comparison-correctness premise is needed.

theorem Hex.GraphIso.Nauty.node_out {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells : Nat} {st : Search n} (first : Bool) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) : SearchOut G (level - 1) level st (node first ctx (n + 2) tcLevel fuel level numcells st).snd

Every search node preserves the caller's partition frame.

theorem Hex.GraphIso.Nauty.sweep_out {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel level numcells tc tv1 index : Nat} {cursor : Option Nat} {cell : VSet n} {st : Search n} (first : Bool) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (hcursor : ∀ (v : Nat), cursor = some v → cell.mem v = true) : SearchOut G level level st (sweep first ctx (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

Every search sweep preserves its parent partition frame.

theorem Hex.GraphIso.Nauty.initial_ok {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : SearchOk G 1 (initialPartition G).snd.length (initial n (initialPartition G).fst (initialPartition G).snd)

The search's nonempty initial state has the coloured root partition.

theorem Hex.GraphIso.Nauty.runState_out {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : SearchOut G 0 1 (initial n (initialPartition G).fst (initialPartition G).snd) (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).snd

Running the search preserves the root partition frame and stores only labellings reached from its original colour cells.

theorem Hex.GraphIso.Nauty.lab_cellsReach {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : CellsReach G (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).snd.lab

A nonempty run keeps a current labelling in the original colour cells.

theorem Hex.GraphIso.Nauty.canonlab_or {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : (runColored G).canonlab = Array.replicate n 0 ∨ (runColored G).canonlab.size = n ∧ CellsReach G (runColored G).canonlab

The final canonical array is either the untouched initial placeholder or a full labelling reached from the original colour cells.

theorem Hex.GraphIso.Nauty.node_noFuel {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells : Nat} {st : Search n} (first : Bool) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (hfuel : n + 1 ≤ level + fuel) : (node first ctx (n + 2) tcLevel fuel level numcells st).fst ≠ Generic.Exit.fuel

The search cannot exhaust a sufficient node bound on a valid partition.

theorem Hex.GraphIso.Nauty.sweep_noFuel {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel level numcells tc tv1 index : Nat} {cursor : Option Nat} {cell : VSet n} {st : Search n} (first : Bool) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (hcursor : ∀ (v : Nat), cursor = some v → cell.mem v = true) (hfuel : n ≤ level + fuel) (hcfuel : Generic.CursorFuel n cfuel cursor) : (sweep first ctx (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).fst ≠ Generic.Exit.fuel

The search cannot exhaust sufficient node and cursor bounds in a sweep.

theorem Hex.GraphIso.Nauty.runState_noFuel {n k : Nat} (G : Colored n k) : (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).fst ≠ Generic.Exit.fuel

The root search run never exhausts its recursion bounds.