theorem
Hex.GraphIso.Nauty.Aligned.first_leaf
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level : Nat}
{root : RefineSt n}
{st : Search n}
(h : Aligned ctx st.gcaFirst root level level n st)
(href : FirstRef ctx tcLevel st.gcaFirst root st)
(hdepth : Depth href.last st)
(hsmall : SubtreeOk ctx st.gcaFirst root)
(hok : SearchOk G level n st)
(heq : st.eqlevFirst = level)
(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)
:
A discrete aligned endpoint reaches the first depth. Its sentinel is therefore the saved sentinel, even though the search does not test it.
theorem
Hex.GraphIso.Nauty.History.first_key
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{cs fs : List Nat}
{st : Search n}
(h : History ctx tcLevel cs.length cs.length n st)
(hcheap : st.noncheaplevel ≤ st.gcaFirst)
(hok : SearchOk G cs.length n st)
(hcodes : FirstCodeInv n cs fs st.firstcode st.eqlevFirst)
(heq : st.eqlevFirst = cs.length)
(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)
:
Below a cheap first ancestor, live code agreement and the retained histories identify the entire current leaf key with the saved first key.
theorem
Hex.GraphIso.Nauty.Codes.leaf_le
{n : Nat}
{ctx : Ctx n}
{cs bs : List Nat}
{st : Search n}
(h : Codes cs bs st)
(hc : st.compCanon < 0)
:
keyLe (pathLeafKey ctx cs st.lab) (incKey ctx bs st.canonlab)
The canonical code machine alone bounds every downward-frozen leaf, including leaves admitted against the first reference.