theorem Hex.GraphIso.Nauty.Sparse.runState_history {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; have st := initial (Graph.ofGraph G.graph) p.fst p.snd; ∃ (href : FirstRef G.graph 100 1 (State.refined (Graph.ofGraph G.graph) 1 p.snd.length st) (runState (Graph.ofGraph G.graph) p.fst p.snd).snd), 1 ≤ href.last ∧ href.last ≤ n

Every nonempty initialized native search retains the complete selected first-reference history, with no external path, cache or code premise.

theorem Hex.GraphIso.Nauty.Sparse.runColored_history {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; have st := initial (Graph.ofGraph G.graph) p.fst p.snd; ∃ (href : FirstRef G.graph 100 1 (State.refined (Graph.ofGraph G.graph) 1 p.snd.length st) (runColored G)), 1 ≤ href.last ∧ href.last ≤ n

Final native row installation retains the same first-reference history in the diagnostic result.