theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.initial_key {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; key G.graph 100 { level := 1, numcells := p.snd.length, codes := [], entry := initial (Graph.ofGraph G.graph) p.fst p.snd } = canonSpecKey G

The root's depth-derived subtree bound is the declared sparse maximum: sufficient-fuel stability identifies the two enumerations.

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

Every key read from the executed production search is at most the declarative sparse maximum. No search-correctness premise is required; the order-zero run has no installed code chain.

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

Finishing the pending native row cache leaves the proved key bound unchanged, so the actual public search pipeline retains it.