theorem
Hex.GraphIso.Nauty.Sparse.prepared_bound
{n : Nat}
{g : Graph n}
{tcLevel level numcells target : Nat}
{short : Bool}
{st : State n}
(hf : st.gcaFirst < level)
(hc : st.gcaCanon < level)
(hb : st.noncheaplevel ≤ level)
:
Actual off-path preparation retains both saved ancestors and the cheap boundary. Its leaf therefore returns strictly above the entered node.
theorem
Hex.GraphIso.Nauty.Sparse.node_bound
{n : Nat}
(g : Graph n)
(inf tcLevel fuel level numcells : Nat)
(st : State n)
(hl : 1 ≤ level)
(hf : st.gcaFirst < level)
(hc : st.gcaCanon < level)
(hb : st.noncheaplevel ≤ level)
(target : Nat)
(short : Bool)
:
(Generic.node false g inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target short → target < level
A complete off-path node unwinds to a strict ancestor. This bound comes from the actual native leaf rules and generic sweep control flow.
theorem
Hex.GraphIso.Nauty.Sparse.first_node_bound
{n : Nat}
(g : Graph n)
(inf tcLevel fuel level numcells : Nat)
(st : State n)
(hl : 1 ≤ level)
(target : Nat)
(short : Bool)
:
(Generic.node true g inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target short → target < level
The first-path terminal rule and sweep also return strictly above their node, without any installed reference premises.
theorem
Hex.GraphIso.Nauty.Sparse.child_target
{n : Nat}
{g : Graph n}
{inf tcLevel fuel level numcells tc tv target : Nat}
{first childFirst : Bool}
{st : State n}
{short : Bool}
(hf : st.gcaFirst ≤ level)
(hc : st.gcaCanon ≤ level)
(hb : st.noncheaplevel ≤ level + 1)
(he :
(Generic.node childFirst g inf tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).fst = Generic.Exit.unwind target short)
(hr : level ≤ target)
:
A received child return targets this exact parent; it cannot point strictly between consecutive levels.