theorem Hex.GraphIso.Nauty.DescPath.length {n : Nat} {ctx : Ctx n} {base level : Nat} {root leaf : RefineSt n} {path : List (Nat × Nat)} (h : DescPath ctx base root path level leaf) : level = base + path.length

Each individualization increases the descent level by one.

theorem Hex.GraphIso.Nauty.DescPath.append {n : Nat} {ctx : Ctx n} {base level last : Nat} {root middle leaf : RefineSt n} {xs ys : List (Nat × Nat)} (h₁ : DescPath ctx base root xs level middle) (h₂ : DescPath ctx level middle ys last leaf) : DescPath ctx base root (xs ++ ys) last leaf

Consecutive descents concatenate their individualization paths.

theorem Hex.GraphIso.Nauty.DescPath.split {n : Nat} {ctx : Ctx n} {base level : Nat} {root leaf : RefineSt n} {path : List (Nat × Nat)} (h : DescPath ctx base root path level leaf) {k : Nat} (hk : k ≤ path.length) : ∃ (middle : RefineSt n), DescPath ctx base root (List.take k path) (base + k) middle ∧ DescPath ctx (base + k) middle (List.drop k path) level leaf

Split a descent at a prescribed number of individualizations.

def Hex.GraphIso.Nauty.Targets (store : Array Int) (base : Nat) (positions : List Nat) : Prop

A list of target positions is stored at consecutive ancestor levels.

Equations

• Hex.GraphIso.Nauty.Targets store base positions = ∀ (i : Nat), i < positions.length → store[base + i]! = Int.ofNat positions[i]!

theorem Hex.GraphIso.Nauty.Targets.take {store : Array Int} {base : Nat} {xs : List Nat} (h : Targets store base xs) (k : Nat) : Targets store base (List.take k xs)

The initial segment of a stored target history reads the same slots.

theorem Hex.GraphIso.Nauty.Targets.prefix {store : Array Int} {base : Nat} {xs ys : List Nat} (hx : Targets store base xs) (hy : Targets store base ys) (hlen : xs.length ≤ ys.length) : xs <+: ys

Two histories read from one store agree through the shorter history.

theorem Hex.GraphIso.Nauty.Targets.set_after {store : Array Int} {base slot : Nat} {xs : List Nat} (h : Targets store base xs) (hafter : base + xs.length ≤ slot) (value : Int) : Targets (store.set! slot value) base xs

Updating a later slot preserves an earlier target history.

theorem Hex.GraphIso.Nauty.Targets.append {store : Array Int} {base : Nat} {xs : List Nat} (h : Targets store base xs) {tc : Nat} (htc : store[base + xs.length]! = Int.ofNat tc) : Targets store base (xs ++ [tc])

A stored next target extends the history without changing the store.

theorem Hex.GraphIso.Nauty.Targets.push {store : Array Int} {base : Nat} {xs : List Nat} (h : Targets store base xs) (hsize : base + xs.length < store.size) (tc : Nat) : Targets (store.set! (base + xs.length) (Int.ofNat tc)) base (xs ++ [tc])

Writing the next target extends its stored history.

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

A descent follows the target positions saved for the first path.

Equations

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

theorem Hex.GraphIso.Nauty.Follows.refl {n : Nat} (ctx : Ctx n) (store : Array Int) (base : Nat) (root : RefineSt n) : Follows ctx store base root base root

An empty descent follows any target store.

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

A later target update preserves a completed descent's history.

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

Individualizing a vertex in the stored target extends a descent.

theorem Hex.GraphIso.Nauty.scatter_of_history {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 : Follows ctx st.firsttc st.gcaFirst ancestor fs.length U) (hV : Follows 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

The first-code bound and stored descent histories justify cheap admission. Equal leaf depths and rows follow from the small-cell subtree theorem.