theorem
Hex.GraphIso.Nauty.Generation.HasLeaf.orbit
{n k : Nat}
{G : Colored n k}
{base : List (Fin n)}
{rs : RefineSt n}
{st : SearchSt n}
{tcLevel level tc e oU oV : Nat}
{u v : Fin n}
{targets : List Nat}
{key : Key n}
(hok : IterOk { g := rowsOf G } level rs)
(hlvl : level < n)
(hpath : PathStab { g := rowsOf G } (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(hlab : st.lab = rs.lab)
(hptn : st.ptn = rs.ptn)
(hbase : ∀ (b : Fin n), st.fixedpts.mem ↑b = true → b ∈ base)
(hcell : (tc, e) ∈ cells rs.ptn level n)
(hne : tc < e)
(hoU : oU ≤ e - tc)
(hoV : oV ≤ e - tc)
(hatU : rs.lab[tc + oU]! = ↑u)
(hatV : rs.lab[tc + oV]! = ↑v)
(horbit : Aut.Orbit G base u v)
(h : HasLeaf { g := rowsOf G } tcLevel (level + 1) (childSt { g := rowsOf G } level rs tc rs.lab[tc + oU]!) targets key)
:
Every image of a reference child under the true path stabilizer contains the same reference occurrence. This supplies the matching-search premise before any generation theorem has been established.