theorem
Hex.GraphIso.Nauty.Generation.HasLeaf.smallChild
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{tcLevel level tc e oU oV : Nat}
{targets : List Nat}
{key : Key n}
(hS : SubtreeOk ctx level st)
(hlvl : level < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(hoU : oU ≤ e - tc)
(hoV : oV ≤ e - tc)
(h : HasLeaf ctx tcLevel (level + 1) (childSt ctx level st tc st.lab[tc + oU]!) targets key)
:
At a small-cell node, a matching reference in one target child occurs in every target child. The geometric carrier supplies occurrence only; no membership in the emitted generator group is assumed.
theorem
Hex.GraphIso.Nauty.Generation.RefPath.smallChild
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{tcLevel boundary level tc e oU oV : Nat}
{targets : List Nat}
{key : Key n}
(hS : SubtreeOk ctx level st)
(hlvl : level < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(hoU : oU ≤ e - tc)
(hoV : oV ≤ e - tc)
(h : RefPath ctx tcLevel boundary (level + 1) (childSt ctx level st tc st.lab[tc + oU]!) targets key)
:
Small-cell transitivity transports the saved reference path, including its uniformity guarantees, to every target child.