theorem Hex.GraphIso.Nauty.StPerm.symm {n level : Nat} {U V : RefineSt n} (h : StPerm level U V) : StPerm level V U

theorem Hex.GraphIso.Nauty.StPerm.trans {n level : Nat} {U V W : RefineSt n} (hUV : StPerm level U V) (hVW : StPerm level V W) : StPerm level U W

theorem Hex.GraphIso.Nauty.StPerm.equitable {n : Nat} {ctx : Ctx n} {level : Nat} {current leaf : RefineSt n} (h : StPerm level current leaf) (heq : Equitable ctx level leaf.lab leaf.ptn) (hsize : leaf.ptn.size = n) (hend : leaf.ptn[leaf.ptn.size - 1]! ≤ level) : Equitable ctx level current.lab current.ptn

Cell-equivalent states have the same equitability property.

theorem Hex.GraphIso.Nauty.Descends.subtree {n : Nat} {ctx : Ctx n} {base level : Nat} {root leaf : RefineSt n} (h : Descends ctx base root level leaf) (hroot : SubtreeOk ctx base root) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) : SubtreeOk ctx level leaf

The small-cell invariant holds along any mathematical descent.

def Hex.GraphIso.Nauty.idRenaming {n : Nat} : Renaming n

The identity vertex renaming.

Equations

• Hex.GraphIso.Nauty.idRenaming = { toFun := id, inj := ⋯, maps := ⋯ }

theorem Hex.GraphIso.Nauty.mapSt_id {n : Nat} (st : RefineSt n) : mapSt idRenaming st = st

Mapping by the identity leaves a refinement state unchanged.

theorem Hex.GraphIso.Nauty.rowsMap_id {n : Nat} {ctx : Ctx n} (hsize : ctx.g.size = n) : RowsMap idRenaming ctx.g ctx.g

The identity renaming preserves a correctly sized row array.

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

A stored-target descent whose endpoint agrees with the current state up to label order inside cells.

Equations

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

theorem Hex.GraphIso.Nauty.Follows.perm {n : Nat} {ctx : Ctx n} {store : Array Int} {base level : Nat} {root leaf : RefineSt n} (h : Follows ctx store base root level leaf) : FollowsPerm ctx store base root level leaf

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

A descent modulo cell order retains the mathematical node invariant.

theorem Hex.GraphIso.Nauty.FollowsPerm.subtree {n : Nat} {ctx : Ctx n} {store : Array Int} {base level : Nat} {root current : RefineSt n} (h : FollowsPerm ctx store base root level current) (hroot : SubtreeOk ctx base root) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) : SubtreeOk ctx level current

A descent modulo cell order retains the entire small-cell invariant.

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

A cell-preserving relabelling of a recovered parent keeps its history.

theorem Hex.GraphIso.Nauty.FollowsPerm.set_after {n : Nat} {ctx : Ctx n} {store : Array Int} {base level slot : Nat} {root current : RefineSt n} (h : FollowsPerm ctx store base root level current) (hafter : level ≤ slot) (value : Int) : FollowsPerm ctx (store.set! slot value) base root level current

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

Individualizing a vertex in the stored target extends the history even when earlier sibling searches reordered the parent's labels.

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

At a discrete endpoint the ghost labelling is the actual labelling.

theorem Hex.GraphIso.Nauty.scatter_of_permHistory {n : Nat} {ctx : Ctx n} {st : Search n} {level : Nat} {cs fs : List Nat} (hcodes : FirstCodeInv n cs fs st.firstcode st.eqlevFirst) (heq : st.eqlevFirst = level) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) {ancestor U V : RefineSt n} (hsmall : SubtreeOk ctx st.gcaFirst ancestor) (hU : FollowsPerm ctx st.firsttc st.gcaFirst ancestor fs.length U) (hV : FollowsPerm ctx st.firsttc st.gcaFirst ancestor level V) (hUd : ∀ (i : Nat), i < n → U.ptn[i]! ≤ fs.length) (hVd : ∀ (i : Nat), i < n → V.ptn[i]! ≤ level) (hfirst : st.firstlab = U.lab) (hcurrent : st.lab = V.lab) (hwork : st.workperm.size = n) : checkAutom ctx.g (scatter st.firstlab st).workperm = true

Cheap admission remains valid when sibling recovery has reordered labels inside ancestor cells.