A Lean 4 proof package for a directed single-source shortest-path bound was published. It proves a uniform deterministic program for exact paths with a charged runtime. The bound applies when edge count is below a stated density function. A verified Bellman-Ford fallback covers cases outside the C-HD branch. The project passed a full build and kernel replay checks. The theorem uses only Lean's standard axioms. An internal agent review accepted the Gate-C claim. The result is asymptotic with large constants and does not claim practical speedup.

• 2,548 build jobs passed
• 18,994 project constants checked
• 266-module dependency closure
• O(n log(n)^(11/12)) proved upper bound