theorem Hex.GraphIso.Perm.val_get_of_ofNatArray? {n : Nat} {a : Array Nat} {p : Perm n} (h : ofNatArray? n a = some p) (i : Fin n) : ↑(p.get i) = a[↑i]!

The entries of a checked raw permutation array.

def Hex.GraphIso.autom? {n k : Nat} (G : Colored n k) (γ : Array Nat) : Option (Perm n)

Accept one raw generator array from the traversal: rebuild it as a permutation of Fin n and check that it is an automorphism. This is the only step that admits a generator, and the admission test is checkIso.

Equations

• Hex.GraphIso.autom? G γ = match Hex.Perm.ofNatArray? n γ with | some p => if Hex.GraphIso.checkIso G G p = true then some p else none | none => none

theorem Hex.GraphIso.autom?_isIso {n k : Nat} {G : Colored n k} {γ : Array Nat} {p : Perm n} (h : autom? G γ = some p) : IsIso G G p

theorem Hex.GraphIso.autom?_val_get {n k : Nat} {G : Colored n k} {γ : Array Nat} {p : Perm n} (h : autom? G γ = some p) (i : Fin n) : ↑(p.get i) = γ[↑i]!

theorem Hex.GraphIso.Perm.ofNatArray?_eq {n : Nat} {γ : Array Nat} {p : Perm n} (hsize : γ.size = n) (hval : ∀ (i : Fin n), ↑(p.get i) = γ[↑i]!) : ofNatArray? n γ = some p

The checked constructor accepts any correctly sized array representing a permutation, including the empty permutation.

theorem Hex.GraphIso.autom?_eq {n k : Nat} {G : Colored n k} {γ : Array Nat} {p : Perm n} (hsize : γ.size = n) (hval : ∀ (i : Fin n), ↑(p.get i) = γ[↑i]!) (hp : IsIso G G p) : autom? G γ = some p

A valid automorphism array passes the public admission filter.

theorem Hex.GraphIso.Aut.checked_perm {n k : Nat} {G : Colored n k} {γ : Array Nat} (h : Nauty.checkAutom (Nauty.rowsOf G) γ = true) : ∃ (p : Perm n), (∀ (i : Fin n), ↑(p.get i) = γ[↑i]!) ∧ ∀ (i j : Fin n), G.graph.adj (p.get i) (p.get j) = G.graph.adj i j

The row checker supplies a typed permutation with exactly the array's entries. Colour preservation is a separate obligation.

theorem Hex.GraphIso.Aut.admit {n k : Nat} {G : Colored n k} {γ : Array Nat} (hcheck : Nauty.checkAutom (Nauty.rowsOf G) γ = true) (hcolor : Nauty.ColorMap G γ) : ∃ (p : Perm n), autom? G γ = some p

A row-checked array preserving the initial colours passes the public admission filter.

theorem Hex.GraphIso.Aut.admit_scatter {n k : Nat} {G : Colored n k} {γ ref cur : Array Nat} (hn : 0 < n) (hrefSize : ref.size = n) (href : Nauty.CellsReach G ref) (hcur : Nauty.CellsReach G cur) (hcheck : Nauty.checkAutom (Nauty.rowsOf G) γ = true) (hmap : ∀ (i : Nat), i < n → γ[ref[i]!]! = cur[i]!) : ∃ (p : Perm n), autom? G γ = some p

A scatter between two reached labellings preserves the initial colouring, so its row-check certificate passes the public filter.

theorem Hex.GraphIso.Aut.admit_root {n k : Nat} {G : Colored n k} {γ : Array Nat} (hcheck : Nauty.checkAutom (Nauty.rowsOf G) γ = true) (hstab : Nauty.CellStab (Nauty.initPtn n (n + 2) (Nauty.initialPartition G).snd) 1 (Nauty.initialPartition G).fst γ) : ∃ (p : Perm n), autom? G γ = some p

A root-ledger carrier preserves colours because it stabilizes every initial colour cell. This includes carriers of implicit pruning pairs.