TL;DR. This is the runtime bound for C-HD, a directed shortest-path algorithm that ten Claude Opus 5.5 agents designed and proved in Lean (Vals AI writeup). n is vertices, m is edges. The bound is linear time, plus a penalty that grows with density, plus a cube-root blend of m and n log n. It only holds in a certified range, m ≤ n·⌊⌊log₂n⌋¾⌋; outside that, C-HD hands off to Bellman–Ford. Drag things below to see where each term takes over, where C-HD actually wins, and how far out its headline advantage kicks in.
Pick a graph size and an average degree (edges per vertex, so m = n·d). The bar splits the predicted operation count into its three terms. Hover a term in the formula or the bar to link them.
m = edges · density m/n² = · total ≈ ops
| Algorithm | ≈ ops | × C-HD |
|---|
Ratios under 1 beat C-HD. Outside the certified range C-HD runs Bellman–Ford, and the table charges it that. BFS only applies to unweighted graphs; it's the floor, not a competitor.
The y-axis is overhead over linear time: predicted ops ÷ (n + m). A flat line at 1 would be perfect. Everything here is the textbook formula with constants set to 1, so read the shapes and crossings, not the absolute heights.
The writeup's showcase regime is m ≈ n·log¾n, right at the certified edge. There, C-HD's leading term is n·log11/12n versus Dijkstra's n·log n, and the proof is a real asymptotic win. But the whole formula also carries m·log(m/n), which only shrinks relative to the leading term very slowly. Here's the same comparison with every term kept and constants set to 1.
Every bound here fits one picture. Give the graph an average degree of d = logα n, so α = 0 is road-network sparse and α = 1 is where m reaches n log n. Divide each running time by n and what's left is log n raised to some power. That exponent is the y-axis. Lower is faster, and the flat line at 1 is the sorting barrier: the n log n cost of emitting vertices in sorted order. It held for 40 years.
How big does a graph have to get before C-HD's full formula beats Dijkstra's on its own showcase profile? Scroll. Each frame is ten, a hundred, then a thousand times more zeros than the one inside it, because the horizontal scale here is doubly logarithmic. The gauge tracks both comparisons as you go: leading terms only, and every term kept with constants set to 1.
Constants set to 1 are a stand-in. The writeup notes the real constants in C-HD's formal construction are enormous, so the true crossover sits further out than the one you just scrolled to.
Every cell is one graph shape: size across, average degree up. Color shows which algorithm's formula is smallest there, or how much faster C-HD is than Dijkstra with a Fibonacci heap (the 1987 champion). The white-space top-left is impossible (more than n − 1 neighbors per vertex). Click a cell to load it into section 01.
Height is C-HD's advantage: log₂ of (competitor's cost ÷ C-HD's cost). Land above the translucent waterline is where C-HD wins; everything below, it loses. Color is still the overall winner. Turn on the certified range and the ground outside it drops off a cliff (it starts off, so you can see the raw formula first), because there C-HD runs Bellman–Ford. Drag to orbit, scroll or pinch to zoom, tap the terrain to load a point into section 01.
Dijkstra finalizes vertices one at a time, in exact distance order, so as a side effect it sorts all n vertices by distance. That sorting is where the n log n comes from. C-HD, like the Duan et al. algorithms before it, gets under that by not insisting on the order: run bounded local searches out from the frontier, charge newly touched vertices against a size limit, and only keep a heap over a thinned-out set of "pivot" vertices that organize the recursion. The right panel shows the band idea (Δ-stepping), which is a simpler cousin of the real algorithm, on the same graph.
One vertex per round, always the closest unfinished one. Every push and pop is heap comparisons.
Everything within the current band is relaxed together, in no particular order. Wider band means fewer rounds but more redone work.
Section 06 showed the general trick: don't insist on sorting. Here is how C-HD does it. Each call takes a frontier, runs one bounded local search per frontier vertex, and stops a search once it has discovered k vertices. Vertices it touches but can't improve still count toward that size limit, as unexplored leaves. Searches that hit the limit become trees whose roots are kept as pivots; searches that run dry finish their small patch on the spot. Only pivots go into the priority structure, and the recursion tree does the rest in bounded batches.
Same start, same 617 intersections of Savannah's grid, two ways to keep the frontier in order. On the left, Dijkstra's binary heap: every vertex waiting to be settled lives in one structure, and every settle costs a trip down a tree whose height is log of its size. On the right, the C-HD model from section 07: the frontier is thinned to pivots and split into a small queue per recursion level. Underneath, what each one hands back, and in what order.
Both sides advance by share of their own run, so the same slider position means "this far through" for each.
Every tentative vertex, ordered by distance. The root is always next.
Only pivots and re-queued leftovers get in. Each row is one live recursion level.
Same race as section 06, now on actual road networks from OpenStreetMap, baked into this page. One-way streets are honored, so this is a directed graph, which is exactly C-HD's setting. Edge weights are meters of road. Road networks are the showcase for this whole topic: an average out-degree around 2 to 3 puts them in the sparse band where the new bounds bite, if the graph is big enough. Tap the map to move the start.
Settles the single nearest intersection each round.
Settles every intersection inside the current Δ-meter band per round.
Real code on real random directed graphs (weights uniform in (0, 1]). Each run checks that every algorithm returns the same distances. The chart shows nanoseconds per edge: a flat line means linear scaling, a rising line means a log factor is showing up.
| n | m | Dijkstra ms | Δ-step ms | Bellman–Ford (queue) ms | BFS ms | agree |
|---|---|---|---|---|---|---|
| Press "run sweep". | ||||||
Where the bound comes from. C-HD, from a Vals AI writeup (Sept 20, 2026): ten Claude Opus 5.5 agents coordinating on a message board designed it in about 15 hours and proved correctness and the runtime bound in Lean (proof repo). Directed graphs, non-negative real weights, exact distances. The bound holds for m ≤ n·⌊⌊log₂n⌋¾⌋; outside that the program runs Bellman–Ford. It's a blog post with a machine-checked proof, not yet a peer-reviewed paper.
The +2 and +1. Pure guards. log(2 + …) never drops below 1, and n + 1 never divides by zero. They change nothing asymptotically.
Reference formulas used. Dijkstra binary heap (n+m)log n; Fibonacci heap m + n log n; d-ary heap with d = m/n, 2m·log n / log d; Duan, Mao, Mao, Shu, Yin 2025, m·log⅔n; Duan, Mao, Shu, Yin 2026, m√log n + √(mn·log n·log log n); Bellman–Ford nm; BFS n + m. All logs base 2, all constants 1.
Why constants = 1 matters. Big-O hides constants and the new algorithms have large ones (recursion, pivot finding, block data structures). The crossings in sections 02 and 05 show where the formulas cross, which is a statement about growth, not stopwatch time.
Model assumptions. Directed graph, real non-negative weights, only comparisons and additions on weights. With integer weights on a word RAM, other algorithms (Thorup's linear-time undirected result, for one) change the picture.
Street data. Road snapshots from OpenStreetMap, fetched via the Overpass API in Sept 2026 and contracted to intersections: drivable and pedestrian highway types, one-way tags and roundabouts honored, clipped to a small box, and trimmed to the largest strongly connected piece so every intersection is reachable from any start. © OpenStreetMap contributors, ODbL.
Sources. arXiv 2504.17033 (2025, m log⅔ n) · arXiv 2602.07868 (2026 improvement) · arXiv 2511.03007 (implementation study).