theorem
Hex.GraphIso.Nauty.Sparse.FirstRef.leaf_follows
{n : Nat}
{G : SparseGraph n}
{tcLevel base level : Nat}
{root current : RefineSt n}
{st : State n}
{f l : Label n}
(h : FirstRef G tcLevel base root st)
(hdepth : level ≤ h.last)
(hr : RefineSt.Ready G base root)
(hc : RefineSt.Ready G level current)
(hshape : NodeShape n base root.ptn)
(hp : FollowsPerm G st.firsttc base root level current)
(hd : discreteAt current.ptn level n = true)
(hf : Label.ofArray? n st.firstlab = some f)
(hl : Label.ofArray? n current.lab = some l)
:
A current history modulo within-cell order still identifies the saved first graph and depth at a discrete endpoint.
theorem
Hex.GraphIso.Nauty.Sparse.classify_first_follows
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level numcells : Nat}
{root current : RefineSt n}
{st out : State n}
{cs fs : List Nat}
{f l : Label n}
(hauto : classify (Graph.ofGraph G.graph) level numcells st = (Generic.Leaf.autoFirst, out))
(h : FirstRef G.graph tcLevel st.gcaFirst root st)
(hcodes : FirstCodeInv n cs fs st.firstcode st.eqlevFirst)
(hr : RefineSt.Ready G.graph st.gcaFirst root)
(hc : RefineSt.Ready G.graph level current)
(hshape : NodeShape n st.gcaFirst root.ptn)
(hp : FollowsPerm G.graph st.firsttc st.gcaFirst root level current)
(hd : discreteAt current.ptn level n = true)
(hcurrent : current.lab = st.lab)
(hw : st.workperm.size = n)
(hf : Label.ofArray? n st.firstlab = some f)
(hl : Label.ofArray? n st.lab = some l)
(hrf : CellsReach G.toDense st.firstlab)
(hrl : CellsReach G.toDense st.lab)
:
The literal native first-reference verdict emits a coloured automorphism when the retained cheap history allows sibling cell reordering. Production use requires these histories at every admission.