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.

theorem Hex.GraphIso.Aut.trace_admitted {n k : Nat} (G : Colored n k) (γ : Array Nat) : γ ∈ trace G → ∃ (p : Perm n), autom? G γ = some p

Every array in the executable trace is admitted, including redundant code-two automorphisms. The proof uses the search invariant; it adds no work to the traversal.

theorem Hex.GraphIso.Aut.raw_eq_trace {n k : Nat} (G : Colored n k) : raw G = trace G

The public filter retains the whole trace, in its original order.

theorem Hex.GraphIso.Aut.mem_gens {n k : Nat} {G : Colored n k} {γ : Array Nat} {p : Perm n} (htrace : γ ∈ trace G) (hcheck : autom? G γ = some p) : p ∈ gens G

A checked automorphism recorded in the raw trace belongs to the public generator list. This also admits code-two generators that leave the orbit partition unchanged.

theorem Hex.GraphIso.Aut.generated_carrier {n k : Nat} {G : Colored n k} {ctx : Nauty.Ctx n} {ref cur : Array Nat} {store : Array (Array Nat)} (h : Nauty.LabelCarrier ctx ref cur store) (hstore : ∀ (γ : Array Nat), γ ∈ store → γ ∈ trace G) (href : Nauty.LabOk ref n) (hsize : ref.size = n) : ∃ (p : Perm n), Perm.Generated (gens G) p ∧ ∀ (i : Nat) (hi : i < n), ↑(p.get ⟨ref[i]!, ⋯⟩) = cur[i]!

A recorded leaf carrier supplies a generated permutation with the same pointwise action on the entire reference labelling.

theorem Hex.GraphIso.Aut.generated_of_reference {n k : Nat} {G : Colored n k} {p q : Perm n} {ref : Array Nat} (hsize : ref.size = n) (href : ref.toList.Perm (List.range n)) (hq : Perm.Generated (gens G) q) (heq : ∀ (i : Nat), i < n → ∀ (hv : ref[i]! < n), q.get ⟨ref[i]!, hv⟩ = p.get ⟨ref[i]!, hv⟩) : Perm.Generated (gens G) p

Agreement on a reference permutation labelling identifies the whole permutation. No orbit-count inference is needed for this final step.

def Hex.GraphIso.Nauty.Generation.TraceOk {n k : Nat} (G : Colored n k) (st : SearchSt n) : Prop

Every recorded array passes the public colour-preserving checker.

Equations

• Hex.GraphIso.Nauty.Generation.TraceOk G st = ∀ (γ : Array Nat), γ ∈ st.genTrace → ∃ (p : Hex.GraphIso.Perm n), Hex.GraphIso.autom? G γ = some p

theorem Hex.GraphIso.Nauty.Generation.TraceOk.ofFields {n k : Nat} {G : Colored n k} {st out : SearchSt n} (h : TraceOk G st) (he : out.genTrace = st.genTrace) : TraceOk G out

theorem Hex.GraphIso.Nauty.Generation.TraceOk.processnode {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hg : ctx.g = rowsOf G) (hn : 0 < n) (hok : SearchOk G level numcells st) (hrefs : LeafRefsOk G st) (hcanong : CanongInv ctx st.canong st.canonlab st.samerows) (h : TraceOk G st) : TraceOk G (Nauty.processnode ctx level numcells st).snd

Admitting a generator preserves the complete public admission check: its scatter endpoints are both reached from the initial colour partition.