feat(ch25): complete Johnson's algorithm — potential, triangle inequality, end-to-end correctness

[TankTechnology]

Summary

Completes Section 25.3 (Johnson's Algorithm), filling the last remaining gaps in Chapter 25.

What's new

12 new definitions/theorems (~350 lines of Lean):

Negative-cycle equivalence for the augmented graph

• adj_target_ne_none — no edge in the augmented graph targets none
• chain_no_none — chains not starting at none never contain none
• walk_from_none_to_none_singleton — the only none→none walk is [none]
• noNegCycle_johnsonAugmentedGraph — G has no negative cycles iff G' has none

Walk projection (G' → G)

• chain_none_free_map — lift a none-free chain from G' to G
• walkWeight_none_free_eq — corresponding walk weights agree
• exists_walk_in_G_of_none_free_walk — project walks back to G

Walk extension utilities (reusable beyond Ch25)

• IsWalkFrom.append_step — extend a walk by a single edge at the end
• walkWeight_append_step — weight formula for extended walks

Johnson potential

• isWalkFrom_none_some — direct edge none → some v
• relaxDist_none_some_ne_top — distance finiteness
• johnsonPotential — h(v) = δ(none, some v) via Bellman-Ford
• johnsonPotential_triangle — h(v) ≤ h(u) + w(u,v) for every edge

End-to-end correctness

• reweightedGraph_nonneg / reweightedGraph_noNegCycle
• johnsonDist — Johnson's all-pairs shortest-path distance
• johnsonDist_isShortestDist — CLRS Theorem 25.5

Chapter 25 status

Section	Status
25.1 All-Pairs Model	✅ Complete
25.2 Floyd-Warshall	✅ Complete (incl. path-reconstruction weight equality, #114)
25.3 Johnson's Algorithm	✅ Complete (this PR)

0 sorry, full lake build and check_repository.py pass.

Closes #32, closes #104

🤖 Generated with Claude Code