theorem Hex.GraphIso.Nauty.Sparse.cells_inverse {n : Nat} {σ τ : Renaming n} {level : Nat} {lab out ptn : Array Nat} (hp : lab.size = n) (hq : out.size = n) (hs : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hok : LabOk lab n) (hc : cellsPerm ptn level out (Array.map σ.toFun lab)) (hinv : ∀ (v : Nat), v < n → τ.toFun (σ.toFun v) = v) : cellsPerm ptn level lab (Array.map τ.toFun out)

Reverse ordered-cell equivalence through inverse vertex renamings. Only inverse values on the actual vertex range are used.

theorem Hex.GraphIso.Nauty.Sparse.subtreeKey_map {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) (tcLevel fuel level : Nat) (lab out ptn : Array Nat) (active : VSet n) (numcells : Nat) (hg : SpecNode G level lab ptn active numcells) (hh : SpecNode H level out ptn active numcells) (hc : cellsPerm ptn level out (Array.map (renamingOf p).toFun lab)) (hf : n < fuel + numcells) : subtreeKey G tcLevel fuel level lab ptn active numcells = subtreeKey H tcLevel fuel level out ptn active numcells

A native graph isomorphism and corresponding ordered cells identify the complete subtree maxima, including their full refinement-code chains.

theorem Hex.GraphIso.Nauty.Sparse.subtreeKey_perm {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells : Nat} {lab out ptn : Array Nat} {active : VSet n} (hg : SpecNode G level lab ptn active numcells) (hh : SpecNode G level out ptn active numcells) (hc : cellsPerm ptn level out lab) (hf : n < fuel + numcells) : subtreeKey G tcLevel fuel level lab ptn active numcells = subtreeKey G tcLevel fuel level out ptn active numcells

Label permutations within ordered cells leave a native subtree maximum unchanged even when the two sparse refinements enumerate leaves differently.