def Hex.GraphIso.Nauty.renamingArray {n : Nat} (sigma : Renaming n) : Array Nat

The finite array represented by a vertex renaming.

Equations

• Hex.GraphIso.Nauty.renamingArray sigma = Array.ofFn fun (i : Fin n) => sigma.toFun ↑i

theorem Hex.GraphIso.Nauty.renamingArray_size {n : Nat} (sigma : Renaming n) : (renamingArray sigma).size = n

theorem Hex.GraphIso.Nauty.renamingArray_get {n : Nat} (sigma : Renaming n) {v : Nat} (hv : v < n) : (renamingArray sigma)[v]! = sigma.toFun v

theorem Hex.GraphIso.Nauty.checkAutom_renaming {n : Nat} {ctx : Ctx n} (sigma : Renaming n) (hrows : RowsMap sigma ctx.g ctx.g) : checkAutom ctx.g (renamingArray sigma) = true

A row-preserving renaming passes the concrete automorphism checker.

theorem Hex.GraphIso.Nauty.SubtreeOk.child_key_eq {n : Nat} {ctx : Ctx n} {st : RefineSt n} {tcLevel fuel level tc len numcells oU oV : Nat} (hS : SubtreeOk ctx level st) (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) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (hoU : oU < len) (hoV : oV < len) (hfuel : level + 1 + fuel ≤ n + 1) : childKey ctx tcLevel fuel level st.lab st.ptn tc numcells oV = childKey ctx tcLevel fuel level st.lab st.ptn tc numcells oU

At a small-cell node, every two members of a non-singleton cell have equal semantic child subtrees. This packages the geometric flip as the concrete checked, cell-stabilizing array expected by childKey_of_carried.

theorem Hex.GraphIso.Nauty.SubtreeOk.node_key {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {active : VSet n} {tcLevel fuel level numcells o : Nat} (hS : SubtreeOk ctx level (refine ctx level lab ptn active numcells)) (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) (hdisc : discreteAt (refine ctx level lab ptn active numcells).ptn level n = false) (ho : o < (specMaketargetcell ctx (refine ctx level lab ptn active numcells).lab (refine ctx level lab ptn active numcells).ptn level tcLevel).snd.snd) (hfuel : level + 1 + fuel ≤ n + 1) (stem : List Nat) : have r := refine ctx level lab ptn active numcells; have tc := (specMaketargetcell ctx r.lab r.ptn level tcLevel).fst; prefixKey stem (specNode ctx tcLevel (fuel + 1) level lab ptn active numcells) = prefixKey (stem ++ [r.longcode]) (childKey ctx tcLevel fuel level r.lab r.ptn tc r.numcells o)

Below a small-cell node, the specification maximum is the subtree of any member of its target cell, with the node's refinement code prefixed.