feat(ch25): complete Johnson's algorithm — potential, triangle inequality, end-to-end correctness - #115
Merged
Merged
Conversation
…lity, end-to-end correctness - Add Bellman-Ford potential construction h(v) = δ(none, some v) via augmented graph with noNegCycle_johnsonAugmentedGraph lemma - Prove triangle inequality h(v) ≤ h(u) + w(u, v) for every edge - Prove reweighted graph edge nonnegativity (Dijkstra precondition) - Prove end-to-end Johnson correctness theorem johnsonDist_isShortestDist (CLRS Theorem 25.5) - Add generic walk-extension lemmas (append_step, walkWeight_append_step) - Add walk-projection infrastructure (chain_none_free_map, walkWeight_none_free_eq, exists_walk_in_G_of_none_free_walk) - Update chapter guide to reflect completion of Sections 25.2 and 25.3 - Update progress CSV to track completed theorems Closes #32, closes #104 Co-Authored-By: Claude <noreply@anthropic.com>
TankTechnology
added a commit
that referenced
this pull request
Aug 1, 2026
PR #113 (feat/johnson-algorithm-issue-104) was developed in parallel with PR #115 (already on main) and shares 11 declarations with it, so it could not be merged as-is. This commit transplants its unique content: - johnsonAllPairsDist_correct: CLRS Theorem 25.6, Johnson's algorithm computes all-pairs shortest distances via Dijkstra (main only had the Theorem 25.5 end-to-end statement) - isShortestDist_edge_ineq: general triangle inequality for shortest-path distances (no sign assumptions) - walk_johnsonAugmented_some_projection: augmented-graph walks project to original-graph walks with the same weight - edge_target_some, johnsonPotential_finite, johnsonReweightedNonneg The transplanted theorems compile against main's declarations (identical signatures for johnsonPotential, johnsonPotential_triangle, etc.). Proof-map and CSV updated (24/24); Progress.lean regenerated. Co-Authored-By: Claude <noreply@anthropic.com>
TankTechnology
added a commit
that referenced
this pull request
Aug 1, 2026
Completes Section 25.3 with Bellman-Ford potential construction, triangle inequality, reweighted edge nonnegativity, and end-to-end Johnson correctness (CLRS Theorem 25.5). - Add noNegCycle_johnsonAugmentedGraph lemma for augmented graph - Construct johnsonPotential h(v) = δ(none, some v) via Bellman-Ford - Prove triangle inequality h(v) ≤ h(u) + w(u,v) for every edge - Prove reweightedGraph_nonneg (Dijkstra precondition) - Prove end-to-end johnsonDist_isShortestDist (CLRS Theorem 25.5) - Add generic walk-extension lemmas (append_step, walkWeight_append_step) - Add walk-projection infrastructure for none-free walks - Update chapter guide and progress CSV - All 3 sections of Chapter 25 are now core-complete (0 sorry) Closes #32, closes #104 🤖 Generated with [Claude Code](https://claude.com/claude-code)
TankTechnology
added a commit
that referenced
this pull request
Aug 1, 2026
PR #113 (feat/johnson-algorithm-issue-104) was developed in parallel with PR #115 (already on main) and shares 11 declarations with it, so it could not be merged as-is. This commit transplants its unique content: - johnsonAllPairsDist_correct: CLRS Theorem 25.6, Johnson's algorithm computes all-pairs shortest distances via Dijkstra (main only had the Theorem 25.5 end-to-end statement) - isShortestDist_edge_ineq: general triangle inequality for shortest-path distances (no sign assumptions) - walk_johnsonAugmented_some_projection: augmented-graph walks project to original-graph walks with the same weight - edge_target_some, johnsonPotential_finite, johnsonReweightedNonneg The transplanted theorems compile against main's declarations (identical signatures for johnsonPotential, johnsonPotential_triangle, etc.). Proof-map and CSV updated (24/24); Progress.lean regenerated. Co-Authored-By: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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 targetsnonechain_no_none— chains not starting atnonenever containnonewalk_from_none_to_none_singleton— the onlynone→nonewalk is[none]noNegCycle_johnsonAugmentedGraph— G has no negative cycles iff G' has noneWalk projection (G' → G)
chain_none_free_map— lift a none-free chain from G' to GwalkWeight_none_free_eq— corresponding walk weights agreeexists_walk_in_G_of_none_free_walk— project walks back to GWalk extension utilities (reusable beyond Ch25)
IsWalkFrom.append_step— extend a walk by a single edge at the endwalkWeight_append_step— weight formula for extended walksJohnson potential
isWalkFrom_none_some— direct edgenone → some vrelaxDist_none_some_ne_top— distance finitenessjohnsonPotential—h(v) = δ(none, some v)via Bellman-FordjohnsonPotential_triangle—h(v) ≤ h(u) + w(u,v)for every edgeEnd-to-end correctness
reweightedGraph_nonneg/reweightedGraph_noNegCyclejohnsonDist— Johnson's all-pairs shortest-path distancejohnsonDist_isShortestDist— CLRS Theorem 25.5Chapter 25 status
0 sorry, full
lake buildandcheck_repository.pypass.Closes #32, closes #104
🤖 Generated with Claude Code