def Hex.GraphIso.Nauty.pathKey {n : Nat} (ctx : Ctx n) : Nat → RefineSt n → List (Nat × Nat) → Key n

The refinement codes and terminal rows along an individualization path.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.pathKey ctx x✝¹ x✝ [] = { codes := [x✝.longcode, Hex.GraphIso.Nauty.codeSentinel], rows := Hex.GraphIso.Nauty.leafRows ctx x✝.lab }

theorem Hex.GraphIso.Nauty.pathKey_codes {n : Nat} (ctx : Ctx n) (path : List (Nat × Nat)) (level : Nat) (st : RefineSt n) : (pathKey ctx level st path).codes = pathCodes ctx level st path ++ [codeSentinel]

The key stores the descent's real refinement codes followed by its sentinel.

theorem Hex.GraphIso.Nauty.SubtreeOk.path_key {n : Nat} {ctx : Ctx n} (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) (path : List (Nat × Nat)) {lab ptn : Array Nat} {active : VSet n} {tcLevel fuel level numcells last : Nat} {leaf : RefineSt n} : have r := refine ctx level lab ptn active numcells; SubtreeOk ctx level r → DescPath ctx level r path last leaf → Selects ctx tcLevel level r path → discreteAt leaf.ptn last n = true → path.length < fuel → level + fuel ≤ n + 1 → specNode ctx tcLevel fuel level lab ptn active numcells = pathKey ctx level r path

Any complete selected descent below a small-cell node realizes its entire specification maximum, including every refinement code.