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. These public trace lemmas remain available to downstream consumers even though whole-group completeness now follows directly from the search theorem.
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)
:
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)
:
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.