Robust Interval Estimation and Error Accumulation Bounds in Shortest Path Algorithms via Johnson's Reweighting

We introduce a formalized mathematical bridge between deterministic graph theory androbust optimization under stochastic uncertainty. By applying principles of interval arithmetic to Johnson’s reweighting algorithm for sparse graphs, we demonstrate that shortestpath optimality is strictly preserved under bounded uncertainty. Moving beyond trivialwidth preservation, we establish mathematically verified bounds for path error accumulation, proving that deterministic robust intervals maintain a strictly linear additive variance.Furthermore, we prove that arbitrary heuristic potentials derived from the lower asymptoticbound guarantees topological validity across the entire uncertainty spectrum. The theoremshave been machine-verified natively in Lean 4 without omitted declarations.