Dijkstra's algorithm greedily settles the closest unvisited vertex on each step, guaranteeing that its distance is final. Because the frontier grows outward like a wave, every shortest path is discovered before any longer path — but the guarantee only holds when all edge weights are non-negative. Watch the priority queue, per-step relaxations, and the shortest-path tree unfold below.
source current pop in queue settled target
Pop the vertex u with the smallest tentative distance d[u]. Suppose some other still-unsettled vertex actually has a shorter true distance — the path to it must pass through at least one unsettled vertex whose tentative distance is already ≥ d[u]. Every subsequent edge adds non-negative weight, so the arrival distance can only grow, contradicting the assumption. That's the induction: each settled vertex's distance is final. If any edge is negative, a later hop can shrink the total, and the invariant breaks — that's when you reach for Bellman-Ford instead. Complexity with a binary heap: O((|V| + |E|) log |V|). This visualizer uses a lazy min-heap: rather than decrease-key, it pushes duplicate entries and discards stale pops (whose d no longer matches dist[v]).