theorem
Hex.GraphIso.Nauty.Sparse.Ready.child_store
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells tc tv : Nat}
{st : State n}
{lab : Array Nat}
{cell : VSet n}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(first : Bool)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hs :
have ch := Generic.Policy.child first level tc tv st;
lab.size = ch.lab.size ∧ cellsPerm ch.ptn (level + 1) ch.lab lab)
:
A label stored inside an actual individualized child retains the chosen vertex at its target position and respects the parent's cells.
theorem
Hex.GraphIso.Nauty.Sparse.child_canon
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv : Nat}
{st : State n}
{cell : VSet n}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(first childFirst : Bool)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
:
have out :=
(Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
out.gcaCanon ≤ st.gcaCanon ∧ out.canonlab = st.canonlab ∨ out.canonlab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab out.canonlab ∧ out.canonlab[tc]! = tv
A complete native child either retains the old canonical reference without deepening its ancestor, or installs a reference through its chosen vertex. This is independent of pruning correctness or generator completeness.
theorem
Hex.GraphIso.Nauty.Sparse.child_canon_old
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv : Nat}
{st : State n}
{cell : VSet n}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(first childFirst : Bool)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
:
A returned canonical ancestor above the child identifies exactly the parent's incoming reference and ancestor, even if that same label is reachable again inside the child's subtree.