theorem Hex.GraphIso.Nauty.Sparse.orbits_flat {n k : Nat} (G : Sparse.Colored n k) : Orbit.Flat (runColored G).orbits n

Every pointer stored by the actual sparse search is already a root.

theorem Hex.GraphIso.Nauty.Sparse.orbits_trace {n k : Nat} (G : Sparse.Colored n k) {gamma : Array Nat} (hg : gamma ∈ (runColored G).genTrace) {i : Nat} (hi : i < n) : (runColored G).orbits[gamma[i]!]! = (runColored G).orbits[i]!

The final native representatives identify both ends of every emitted generator edge, including admissions that did not reduce the orbit count.

theorem Hex.GraphIso.Nauty.Sparse.orbits_generated {n k : Nat} {G : Sparse.Colored n k} {p : Perm n} (hp : Perm.Generated (runColored G).generators p) (v : Fin n) : (runColored G).orbits[↑(p.get v)]! = (runColored G).orbits[↑v]!

The actual representatives are invariant under every word in the actual emitted generator list.

theorem Hex.GraphIso.Nauty.Sparse.orbits_eq_iff {n k : Nat} (G : Sparse.Colored n k) (u v : Fin n) : (runColored G).orbits[↑u]! = (runColored G).orbits[↑v]! ↔ ∃ (p : Perm n), Sparse.IsIso G G p ∧ p.get u = v

Two vertices have the same native output representative exactly when a colour-preserving automorphism carries one to the other.

theorem Hex.GraphIso.Nauty.Sparse.orbit_le {n k : Nat} (G : Sparse.Colored n k) (u v : Fin n) (h : ∃ (p : Perm n), Sparse.IsIso G G p ∧ p.get u = v) : (runColored G).orbits[↑u]! ≤ ↑v

The stored representative is the least vertex in the full native automorphism orbit, not merely the representative of a discovered subgroup.

theorem Hex.GraphIso.Nauty.Sparse.numorbits_eq_count {n k : Nat} (G : Sparse.Colored n k) : (runColored G).numorbits = List.countP (fun (i : Nat) => (runColored G).orbits[i]! == i) (List.range n)

The stored orbit count is exactly the number of least representatives of the full automorphism orbits. It is the actual orbjoin count, with no postprocessing search or replacement computation.