theorem Hex.GraphIso.Nauty.Sparse.runState_max {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; State.best G.graph (runState (Graph.ofGraph G.graph) p.fst p.snd).snd = some (canonSpecKey G)

For every nonempty sparse coloured graph, the literal production search installs exactly the declarative sparse maximum. Its first-path context is initialized from the actual colour buckets, all recursive coverage is proved, and the existing production bound excludes exhaustion.

theorem Hex.GraphIso.Nauty.Sparse.run_max {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; State.best G.graph (run (Graph.ofGraph G.graph) p.fst p.snd) = some (canonSpecKey G)

Finishing the pending sparse row cache retains the same exact maximum. This is the state consumed by the total native public API.