theorem
Hex.GraphIso.Nauty.Sparse.Generation.RefPath.orbit
{n k : Nat}
{G : Sparse.Colored n k}
{base : List (Fin n)}
{tcLevel boundary level tc len a b : Nat}
{rs : RefineSt n}
{st : State n}
{scratch other : Scratch}
{u v : Fin n}
{targets : List Nat}
{key : Key n}
(hr : RefineSt.Ready G.graph level rs)
(hpath : PathInv G level st)
(hlab : st.lab = rs.lab)
(hptn : st.ptn = rs.ptn)
(hbase : ∀ (x : Fin n), st.fixedpts.mem ↑x = true → x ∈ base)
(hc : IsCell rs.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(ha : a < len)
(hb' : b < len)
(hs : Scratch.Bounded n scratch)
(ht : Scratch.Bounded n other)
(hatU : rs.lab[tc + a]! = ↑u)
(hatV : rs.lab[tc + b]! = ↑v)
(horbit : Aut.Orbit G.toDense base u v)
(h :
RefPath G.graph tcLevel boundary (level + 1)
(RefineSt.child (Graph.ofGraph G.graph) level rs tc rs.lab[tc + a]! scratch) targets key)
:
Every image under the true path stabilizer contains the transported native reference with the same all-same boundary. This justifies reference occurrence before the emitted subgroup is known to be complete.