theorem Hex.GraphIso.Nauty.RouteHistory.first_leaf {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level : Nat} {st : Search n} (h : RouteHistory ctx tcLevel level level n st) (hok : SearchOk G level n st) (heq : st.eqlevFirst = level) (hgsz : ctx.g.size = n) (hcheck : checkAutom ctx.g (scatter st.firstlab st).workperm = true) (hwork : st.workperm.size = n) (hfirst : st.firstlab.size = n) (hperm : st.firstlab.toList.Perm (List.range n)) : st.firstcode[level + 1]! = codeSentinel ∧ leafRows ctx st.lab = leafRows ctx st.firstlab

A checked scatter between the actual leaves identifies the saved sentinel and all adjacency rows along a live guided history.

theorem Hex.GraphIso.Nauty.History.autoFirst_key {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {cs fs : List Nat} {st out : Search n} (h : History ctx tcLevel cs.length cs.length n st) (hinv : RunInv G ctx st) (hn0 : 0 < n) (hok : SearchOk G cs.length n st) (hcodes : FirstCodeInv n cs fs st.firstcode st.eqlevFirst) (hauto : Nauty.classify ctx cs.length n st = (Generic.Leaf.autoFirst, out)) (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) : pathLeafKey ctx cs st.lab = incKey ctx fs st.firstlab

Every first-reference admission has the complete saved key. The retained histories justify its depth even when admission uses a scan.

theorem Hex.GraphIso.Nauty.History.leaf_max {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {cs bs fs : List Nat} {st : Search n} (h : History ctx tcLevel cs.length cs.length n st) (hinv : RunInv G ctx st) (hn0 : 0 < n) (hlevel : 1 ≤ cs.length) (hok : SearchOk G cs.length n st) (hcanon : Codes cs bs st) (hfirst : FirstCodeInv n cs fs st.firstcode st.eqlevFirst) (hbs : bs ≠ []) (hle : keyLe (incKey ctx fs st.firstlab) (incKey ctx bs st.canonlab)) (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) : have verdict := Nauty.classify ctx cs.length n st; have out := (leafExit verdict.fst cs.length verdict.snd).snd; ∃ (bs' : List Nat), Settled cs bs' out ∧ SearchState.key ctx bs' out = some (incMax (SearchState.key ctx bs st) (pathLeafKey ctx cs st.lab))

At every discrete node with live histories, the leaf action computes exactly the maximum of its incoming incumbent and its current leaf key. The saved first key is already bounded by the incoming incumbent.

theorem Hex.GraphIso.Nauty.History.leaf_best {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {cs bs fs : List Nat} {st : Search n} (h : History ctx tcLevel cs.length cs.length n st) (hinv : RunInv G ctx st) (hn0 : 0 < n) (hlevel : 1 ≤ cs.length) (hok : SearchOk G cs.length n st) (hcanon : Codes cs bs st) (hfirst : FirstCodeInv n cs fs st.firstcode st.eqlevFirst) (hbs : bs ≠ []) (hle : keyLe (incKey ctx fs st.firstlab) (incKey ctx bs st.canonlab)) (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) : have verdict := Nauty.classify ctx cs.length n st; SearchState.best ctx (leafExit verdict.fst cs.length verdict.snd).snd = some (incMax (SearchState.key ctx bs st) (pathLeafKey ctx cs st.lab))

The completed leaf action exposes that maximum through the executable code store, even if the incoming store was in the overwrite window.