theorem Hex.GraphIso.Nauty.Guided.append {n : Nat} {ctx : Ctx n} {store : Array Int} {tcLevel base level tc o : Nat} {root leaf : RefineSt n} {path : List (Nat × Nat)} (h : DescPath ctx base root path level leaf) (hg : Guided ctx tcLevel store base root path) (htc : specTargetcell ctx leaf.lab leaf.ptn level tcLevel = tc ∨ store[level]! = Int.ofNat tc) : Guided ctx tcLevel store base root (path ++ [(tc, o)])

Appending a canonical or saved target extends a guided descent.

def Hex.GraphIso.Nauty.GuidedPerm {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (store : Array Int) (base : Nat) (root : RefineSt n) (level : Nat) (current : RefineSt n) : Prop

A guided descent whose endpoint agrees with the current partition up to label order within cells.

Equations

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

theorem Hex.GraphIso.Nauty.GuidedPerm.refl {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (store : Array Int) (level : Nat) (st : RefineSt n) : GuidedPerm ctx tcLevel store level st level st

A frozen frame starts its own guided history.

theorem Hex.GraphIso.Nauty.GuidedPerm.iter {n : Nat} {ctx : Ctx n} {store : Array Int} {tcLevel base level : Nat} {root current : RefineSt n} (h : GuidedPerm ctx tcLevel store base root level current) (hroot : IterOk ctx base root) : IterOk ctx level current

A guided descent retains the mathematical node invariant.

theorem Hex.GraphIso.Nauty.GuidedPerm.setLab {n : Nat} {ctx : Ctx n} {store : Array Int} {tcLevel base level : Nat} {root current : RefineSt n} {lab : Array Nat} (h : GuidedPerm ctx tcLevel store base root level current) (hsize : lab.size = current.lab.size) (hcells : cellsPerm current.ptn level current.lab lab) : GuidedPerm ctx tcLevel store base root level { lab := lab, ptn := current.ptn, active := current.active, numcells := current.numcells, hint := current.hint, maxpos := current.maxpos, longcode := current.longcode }

Sibling recovery may reorder labels within cells while retaining the same guided history.

theorem Hex.GraphIso.Nauty.GuidedPerm.leaf {n : Nat} {ctx : Ctx n} {store : Array Int} {tcLevel base level : Nat} {root current : RefineSt n} (h : GuidedPerm ctx tcLevel store base root level current) (hroot : IterOk ctx base root) (hdisc : ∀ (i : Nat), i < n → current.ptn[i]! ≤ level) : ∃ (leaf : RefineSt n), ∃ (path : List (Nat × Nat)), DescPath ctx base root path level leaf ∧ Guided ctx tcLevel store base root path ∧ leaf.lab = current.lab ∧ leaf.ptn = current.ptn

A guided discrete endpoint has the actual current labelling.

theorem Hex.GraphIso.Nauty.GuidedPerm.child {n : Nat} {ctx : Ctx n} {store : Array Int} {tcLevel base level tc e o : Nat} {root current : RefineSt n} (hsize : ctx.g.size = n) (hroot : IterOk ctx base root) (h : GuidedPerm ctx tcLevel store base root level current) (hlevel : level < n) (hcell : (tc, e) ∈ cells current.ptn level n) (hne : tc < e) (ho : o ≤ e - tc) (htc : specTargetcell ctx current.lab current.ptn level tcLevel = tc ∨ store[level]! = Int.ofNat tc) : GuidedPerm ctx tcLevel store base root (level + 1) (childSt ctx level current tc current.lab[tc + o]!)

A canonical or saved target extends the guided history through individualization and refinement, including after sibling reordering.