theorem
Hex.GraphIso.Nauty.Generation.first_leaf
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells : Nat}
{st : SearchSt n}
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n)
(hsize : st.firstcode.size = n + 2)
(hlevel : level ≤ n)
(hdisc : ∀ (q : Nat), q < n → (refine ctx level st.lab st.ptn st.active numcells).ptn[q]! ≤ level)
:
have rs := refine ctx level st.lab st.ptn st.active numcells;
have out := (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).snd;
have key := { codes := [rs.longcode, codeSentinel], rows := leafRows ctx rs.lab };
HasLeaf ctx tcLevel level rs [] key ∧ Matches ctx level out [] key ∧ out.firstlab = rs.lab
The first discrete descent installs the exact reference occurrence used by subsequent matching searches.
theorem
Hex.GraphIso.Nauty.Generation.other_leaf_trace
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells : Nat}
{st : SearchSt n}
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n)
:
(otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd.genTrace = (processnode ctx level n (otherLeafSt ctx level numcells st)).snd.genTrace
Both ways of returning from a discrete off-path node retain precisely the trace produced by its leaf event.
theorem
Hex.GraphIso.Nauty.Generation.other_leaf_lab
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells : Nat}
{st : SearchSt n}
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n)
:
A discrete off-path return retains the refined leaf labelling through both the immediate return and the empty-sweep cleanup.
theorem
Hex.GraphIso.Nauty.Generation.other_leaf
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells : Nat}
{st : SearchSt n}
{targets : List Nat}
{key : Key n}
(hgsz : ctx.g.size = n)
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n)
(hok : IterOk ctx level (refine ctx level st.lab st.ptn st.active numcells))
(hdisc : ∀ (q : Nat), q < n → (refine ctx level st.lab st.ptn st.active numcells).ptn[q]! ≤ level)
(hfirstSize : st.firstlab.size = n)
(hfirst : st.firstlab.toList.Perm (List.range n))
(hperm : (refine ctx level st.lab st.ptn st.active numcells).lab.toList.Perm (List.range n))
(hm : Matches ctx level st targets key)
(hleaf : HasLeaf ctx tcLevel level (refine ctx level st.lab st.ptn st.active numcells) targets key)
(hlevel : st.eqlevFirst = level - 1)
:
A discrete off-path node containing the matching first-reference leaf returns an emitted carrier. This is stated for the actual recursive search call, including its comparison preparation and leaf cleanup.