def Hex.GraphIso.Nauty.Sparse.State.generators {n : Nat} (st : State n) : List (Perm n)

Decode the complete emitted native trace as forward permutations. Sound reached traces lose no entry; decoding retains order and duplicates and does not repeat any graph search or adjacency test.

Equations

• st.generators = List.filterMap (Hex.Perm.ofNatArray? n) st.genTrace.toList

theorem Hex.GraphIso.Nauty.Sparse.TraceOk.generator {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) {p : Perm n} (hp : p ∈ st.generators) : Sparse.IsIso G G p

Every decoded permutation is exactly its emitted array and preserves the native graph and ordered colours.

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Sparse.Generation.Realizes {n k : Nat} (G : Sparse.Colored n k) (gs : List (Perm n)) (store : List (Array Nat)) : Prop

The shared abstract generated-group relation is applied to the native sparse graph's semantic interpretation. It executes no dense search.

Equations

• Hex.GraphIso.Nauty.Sparse.Generation.Realizes G gs store = Hex.GraphIso.Nauty.Generation.Realizes G.toDense gs store

theorem Hex.GraphIso.Nauty.Sparse.Generation.realized {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : TraceOk G st) : Realizes G st.generators st.genTrace.toList

A sound native trace realizes its own complete decoded generator list. Every emitted array parses successfully, including order zero.

theorem Hex.GraphIso.Nauty.Sparse.Generation.pointer {n k : Nat} {G : Sparse.Colored n k} {st : State n} {gs : List (Perm n)} {base : List (Fin n)} (h : OrbitTrace G st) (ht : TraceOk G st) (hr : Realizes G gs st.genTrace.toList) (hfix : ∀ (gamma : Array Nat), gamma ∈ st.genTrace → ∀ (b : Fin n), b ∈ base → gamma[↑b]! = ↑b) (v : Fin n) : ∃ (u : Fin n), ↑u = st.orbits[↑v]! ∧ ↑u ≤ ↑v ∧ ∃ (p : Perm n), Perm.Generated gs p ∧ Sparse.IsIso G G p ∧ Perm.Fixes base p ∧ p.get v = u

Native orbit pointers are realized by words in a containing trace whenever those recorded generators fix the active base.

theorem Hex.GraphIso.Nauty.Sparse.Generation.root {n k : Nat} (G : Sparse.Colored n k) : Realizes G (runColored G).generators (runColored G).genTrace.toList

The public production trace is represented without losing an emitted generator; this supplies the containing group for the first-path generation induction. Completeness of that group is a separate theorem.