theorem Hex.GraphIso.Nauty.stPerm_target {n : Nat} {ctx : Ctx n} {σ : Renaming n} {level tcLevel : Nat} {U V : RefineSt n} (hg : RowsMap σ ctx.g ctx.g) (hU : IterOk ctx level U) (hsp : StPerm level V (mapSt σ U)) : specTargetcell ctx V.lab V.ptn level tcLevel = specTargetcell ctx U.lab U.ptn level tcLevel

A row-preserving renaming and a reordering inside cells leave the next target position unchanged.

theorem Hex.GraphIso.Nauty.descPath_invariant {n : Nat} {ctx : Ctx n} {α : Type} (f : Nat → RefineSt n → α) (hf : ∀ {σ : Renaming n} {level : Nat} {U V : RefineSt n}, RowsMap σ ctx.g ctx.g → IterOk ctx level U → StPerm level V (mapSt σ U) → f level V = f level U) (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (tcs : List Nat) {level : Nat} {st : RefineSt n} {p₁ p₂ : List (Nat × Nat)} {last : Nat} {U V : RefineSt n} : SubtreeOk ctx level st → DescPath ctx level st p₁ last U → List.map Prod.fst p₁ = tcs → DescPath ctx level st p₂ last V → List.map Prod.fst p₂ = tcs → f last V = f last U

Descents following the same target positions below a cheap ancestor agree on every quantity invariant under cell reordering and automorphisms.

theorem Hex.GraphIso.Nauty.descPath_ptn {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) {level last : Nat} {st U V : RefineSt n} {p₁ p₂ : List (Nat × Nat)} (hS : SubtreeOk ctx level st) (hU : DescPath ctx level st p₁ last U) (hV : DescPath ctx level st p₂ last V) (hp : List.map Prod.fst p₂ = List.map Prod.fst p₁) : V.ptn = U.ptn

Equal target histories below a cheap ancestor have equal partitions.

theorem Hex.GraphIso.Nauty.descPath_target {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) {level last : Nat} {st U V : RefineSt n} {p₁ p₂ : List (Nat × Nat)} (hS : SubtreeOk ctx level st) (hU : DescPath ctx level st p₁ last U) (hV : DescPath ctx level st p₂ last V) (hp : List.map Prod.fst p₂ = List.map Prod.fst p₁) (tcLevel : Nat) : specTargetcell ctx V.lab V.ptn last tcLevel = specTargetcell ctx U.lab U.ptn last tcLevel

Equal target histories below a cheap ancestor choose the same next unhinted target, before either descent is discrete.

theorem Hex.GraphIso.Nauty.descPath_prefix {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (tcs : List Nat) {level : Nat} {st : RefineSt n} {p₁ p₂ : List (Nat × Nat)} {level₁ level₂ : Nat} {U V : RefineSt n} : SubtreeOk ctx level st → DescPath ctx level st p₁ level₁ U → List.map Prod.fst p₁ = tcs → (∀ (q : Nat), q < n → U.ptn[q]! ≤ level₁) → DescPath ctx level st p₂ level₂ V → List.map Prod.fst p₂ <+: tcs → (∀ (q : Nat), q < n → V.ptn[q]! ≤ level₂) → level₂ = level₁ ∧ leafRows ctx V.lab = leafRows ctx U.lab

Discrete descents below a cheap ancestor have the same depth and leaf rows when the second target path is a prefix of the first.