For every fixed $\kappa\in\mathbb N$, there exist one finite deterministic word-RAM program $P$, one natural constant $b$, and one step-bound function $T$ that work for every input size $n$, including $n=0,1$, and for every word width $W\ge b(\operatorname{Nat.log2}(n)+1)$. All encoded input numbers have absolute value at most $n^\kappa$. The run must halt with the specified verdict and output within $T(n)$ steps.

For a directed $n$-vertex graph with integer weights and no negative-weight closed walk, accept and compute every exact shortest-path distance in

Each ordered vertex pair receives a flag and a distance. Reachable pairs have flag one and an attained minimum path weight; unreachable pairs have flag zero and an unconstrained distance slot. Negative edge weights and missing edges are permitted. Empty paths give diagonal distance zero. No assumptions about other algorithms appear in the theorem.

This is the corresponding known result extracted from the source formalization, presented here as an open proof obligation.