def Hex.GraphIso.Nauty.SearchState.refined {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : RefineSt n

The refinement state at a search node, before target bookkeeping.

Equations

• Hex.GraphIso.Nauty.SearchState.refined ctx level numcells st = Hex.GraphIso.Nauty.refine ctx level st.lab st.ptn st.active numcells

theorem Hex.GraphIso.Nauty.prepareFirst_fields {n : Nat} (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : have r := Generic.prepareFirst ctx tcLevel level numcells st; r.snd.snd.snd.snd.lab = (SearchState.refined ctx level numcells st).lab ∧ r.snd.snd.snd.snd.ptn = (SearchState.refined ctx level numcells st).ptn ∧ r.snd.snd.snd.snd.firsttc = st.firsttc.set! level r.snd.fst

First-path preparation retains the refined partition and writes its target.

theorem Hex.GraphIso.Nauty.firstChild_refined {n : Nat} (ctx : Ctx n) (tcLevel level numcells tv : Nat) (st : Search n) : have r := Generic.prepareFirst ctx tcLevel level numcells st; SearchState.refined ctx (level + 1) (r.fst + 1) (child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd)) = childSt ctx level (SearchState.refined ctx level numcells st) r.snd.fst.toNat tv

The child's refinement is exactly the mathematical individualization step.

theorem Hex.GraphIso.Nauty.prepareFirst_code {n : Nat} (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd.firstcode = st.firstcode.set! level (SearchState.refined ctx level numcells st).longcode

Preparing a first-path node records precisely its refinement code.

theorem Hex.GraphIso.Nauty.firstPath_code_before {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells last slot : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) (hslot : slot < level) : leaf.firstcode[slot]! = st.firstcode[slot]!

The first descent retains the refinement codes of every earlier ancestor.

theorem Hex.GraphIso.Nauty.firstPath_before {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells last slot : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) (hslot : slot < level) : leaf.firsttc[slot]! = st.firsttc[slot]!

The first descent never changes a target slot above its current level.

theorem Hex.GraphIso.Nauty.firstPath_size {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) : leaf.firsttc.size = st.firsttc.size

The target array retains its allocated size along the first descent.

theorem Hex.GraphIso.Nauty.refined_iter {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) : IterOk ctx level (SearchState.refined ctx level numcells st)

A valid node's refinement has the state invariant used by descent paths.

theorem Hex.GraphIso.Nauty.prepareFirst_choice {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (hopen : (Generic.prepareFirst ctx tcLevel level numcells st).fst ≠ n) (hit : IterOk ctx level (SearchState.refined ctx level numcells st)) (heq : Equitable ctx level (SearchState.refined ctx level numcells st).lab (SearchState.refined ctx level numcells st).ptn) : (Generic.prepareFirst ctx tcLevel level numcells st).snd.fst = Int.ofNat (specTargetcell ctx (SearchState.refined ctx level numcells st).lab (SearchState.refined ctx level numcells st).ptn level tcLevel)

A first-path target uses the unhinted specification rule.

theorem Hex.GraphIso.Nauty.firstChild_ok {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells tv : Nat} {st : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (htv : (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.fst.nextElem none = some tv) : have r := Generic.prepareFirst ctx tcLevel level numcells st; SearchOk G (level + 1) (r.fst + 1) (child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd))

A selected child of the prepared first path has a valid entry partition.

theorem Hex.GraphIso.Nauty.Targets.cons {store : Array Int} {base tc : Nat} {xs : List Nat} (hhead : store[base]! = Int.ofNat tc) (htail : Targets store (base + 1) xs) : Targets store base (tc :: xs)

A stored head target and its suffix form one consecutive history.

theorem Hex.GraphIso.Nauty.firstPath_history {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (heq : Equitable ctx level (SearchState.refined ctx level numcells st).lab (SearchState.refined ctx level numcells st).ptn) (hsize : n < st.firsttc.size) (hcodeSize : n < st.firstcode.size) : ∃ (path : List (Nat × Nat)), ∃ (U : RefineSt n), DescPath ctx level (SearchState.refined ctx level numcells st) path last U ∧ Selects ctx tcLevel level (SearchState.refined ctx level numcells st) path ∧ Targets leaf.firsttc level (List.map Prod.fst path) ∧ U.lab = leaf.lab ∧ U.ptn = leaf.ptn ∧ (∀ (i : Nat), i < n → U.ptn[i]! ≤ last) ∧ StoredCodes leaf.firstcode level (pathCodes ctx level (SearchState.refined ctx level numcells st) path)

The actual first descent yields a selected mathematical path whose target positions are retained in the final first-target array.

theorem Hex.GraphIso.Nauty.firstPath_saved {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (heq : Equitable ctx level (SearchState.refined ctx level numcells st).lab (SearchState.refined ctx level numcells st).ptn) (hsize : n < st.firsttc.size) (hcodeSize : n < st.firstcode.size) : have out := (node true ctx inf tcLevel fuel level numcells st).snd; ∃ (path : List (Nat × Nat)), ∃ (U : RefineSt n), DescPath ctx level (SearchState.refined ctx level numcells st) path last U ∧ Selects ctx tcLevel level (SearchState.refined ctx level numcells st) path ∧ Targets out.firsttc level (List.map Prod.fst path) ∧ U.lab = out.firstlab ∧ (∀ (i : Nat), i < n → U.ptn[i]! ≤ last) ∧ StoredCodes out.firstcode level (pathCodes ctx level (SearchState.refined ctx level numcells st) path)

The saved first reference carries the selected descent history even after the full search call has searched later siblings.

theorem Hex.GraphIso.Nauty.initial_equitable {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : have st := initial n (initialPartition G).fst (initialPartition G).snd; have r := SearchState.refined { g := rowsOf G } 1 (initialPartition G).snd.length st; Equitable { g := rowsOf G } 1 r.lab r.ptn

The initial colour partition refines to an equitable root.

theorem Hex.GraphIso.Nauty.runState_history {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : have st := initial n (initialPartition G).fst (initialPartition G).snd; have out := (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).snd; ∃ (last : Nat), ∃ (path : List (Nat × Nat)), ∃ (U : RefineSt n), DescPath { g := rowsOf G } 1 (SearchState.refined { g := rowsOf G } 1 (initialPartition G).snd.length st) path last U ∧ Selects { g := rowsOf G } 100 1 (SearchState.refined { g := rowsOf G } 1 (initialPartition G).snd.length st) path ∧ Targets out.firsttc 1 (List.map Prod.fst path) ∧ U.lab = out.firstlab ∧ ∀ (i : Nat), i < n → U.ptn[i]! ≤ last

A nonempty search run stores the leaf of a selected descent from the refined colour partition, together with its complete target history.

theorem Hex.GraphIso.Nauty.firstPath_codeSize {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) : leaf.firstcode.size = st.firstcode.size

Recording first-path codes preserves the allocated code-store size.

theorem Hex.GraphIso.Nauty.firstPath_sentinel {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) (hsize : st.firstcode.size = n + 2) (hlast : last ≤ n) : (node true ctx inf tcLevel fuel level numcells st).snd.firstcode[last + 1]! = codeSentinel

The saved reference marks the level immediately after its actual first leaf.