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.
theorem
Hex.GraphIso.Nauty.Generation.cheap_reference
{n : Nat}
{ctx : Ctx n}
(inf tcLevel : Nat)
(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)
(fuel level numcells : Nat)
(st : SearchSt n)
(targets : List Nat)
(key : Key n)
:
SubtreeOk ctx level (refine ctx level st.lab st.ptn st.active numcells) →
st.firstlab.size = n →
st.firstlab.toList.Perm (List.range n) →
Matches ctx level st targets key →
HasLeaf ctx tcLevel level (refine ctx level st.lab st.ptn st.active numcells) targets key →
st.eqlevFirst = level - 1 →
st.needshortprune = false →
st.gcaFirst < level →
level ≤ n →
n < level + fuel →
have result := otherNode ctx inf tcLevel fuel level numcells st;
result.fst = Int.ofNat st.gcaFirst ∧ LabelCarrier ctx st.firstlab result.snd.lab result.snd.genTrace
A matching small-cell subtree emits a first-reference carrier on its first descent and returns to that reference's guide. In particular, no implicit-pair generation hypothesis is needed for this off-path case.