theorem
Hex.GraphIso.Nauty.Sparse.OrbitTrace.root
{n k : Nat}
{G : Sparse.Colored n k}
{st : State n}
{base : List (Fin n)}
{guide : Fin n}
(h : OrbitTrace G st)
(ht : TraceOk G st)
(hfix : ∀ (gamma : Array Nat), gamma ∈ st.genTrace → ∀ (b : Fin n), b ∈ base → gamma[↑b]! = ↑b)
(hmin : ∀ (v : Fin n), Aut.Orbit G.toDense base guide v → ↑guide ≤ ↑v)
:
The least vertex of a true stabilizer orbit remains its own native representative whenever the emitted trace fixes that base.
theorem
Hex.GraphIso.Nauty.Sparse.OrbitReplay.mark
{n k : Nat}
{G : Sparse.Colored n k}
{st : State n}
{base : List (Fin n)}
{guide tv : Fin n}
{cell : VSet n}
(h : OrbitReplay st)
(ht : TraceOk G st)
(ho : OrbitTrace G st)
(hc : Generation.Cover G.toDense st.generators base guide cell (some ↑tv))
(hv : cell.mem ↑tv = true)
(hfix : ∀ (gamma : Array Nat), gamma ∈ st.genTrace → ∀ (b : Fin n), b ∈ base → gamma[↑b]! = ↑b)
(hmin : ∀ (v : Fin n), Aut.Orbit G.toDense base guide v → ↑guide ≤ ↑v)
:
At an advanced cursor, generated coverage and the literal join invariant make the executed counter test equivalent to membership in the guide's full point-stabilizer orbit.