theorem Hex.GraphIso.Nauty.Sparse.OrbitReplay.flat {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : OrbitReplay st) (ht : TraceOk G st) : Orbit.Flat st.orbits n

Intermediate native joins already store roots at every vertex.

theorem Hex.GraphIso.Nauty.Sparse.OrbitReplay.trace {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : OrbitReplay st) (ht : TraceOk G st) {gamma : Array Nat} (hg : gamma ∈ st.genTrace) {i : Nat} (hi : i < n) : st.orbits[gamma[i]!]! = st.orbits[i]!

Every emitted generator edge has been joined in the current array, including admissions that left the orbit count unchanged.

theorem Hex.GraphIso.Nauty.Sparse.OrbitReplay.generated {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : OrbitReplay st) (ht : TraceOk G st) {p : Perm n} (hp : Perm.Generated st.generators p) (v : Fin n) : st.orbits[↑(p.get v)]! = st.orbits[↑v]!

Words in the generators emitted so far preserve current native representatives. This applies before the search has completed.

theorem Hex.GraphIso.Nauty.Sparse.OrbitReplay.stable {n k : Nat} {G : Sparse.Colored n k} {st out : State n} (h : OrbitReplay out) (ht : TraceOk G out) (hs : OrbSound (OrbConn st.genTrace.toList n) st.orbits n) (hsub : ∀ (gamma : Array Nat), gamma ∈ st.genTrace → gamma ∈ out.genTrace) : Orbit.Stable st.orbits n fun (v : Nat) => out.orbits[v]!

Later joins preserve every connection already represented by an earlier pointer, provided the executed trace only grows.

theorem Hex.GraphIso.Nauty.Sparse.State.generators_mono {n : Nat} {st out : State n} (h : ∀ (gamma : Array Nat), gamma ∈ st.genTrace → gamma ∈ out.genTrace) (p : Perm n) : p ∈ st.generators → p ∈ out.generators

Extending the literal emitted array trace extends its decoded generator list without another automorphism check or graph traversal.