feat(ch25): complete Floyd-Warshall path-reconstruction weight equality

[TankTechnology]

Summary

Prove that the path reconstructed from the final Floyd-Warshall predecessor matrix floydWarshallPi has weight exactly floydWarshall i j. This resolves the path-reconstruction weight-equality gap tracked in issue #95.

New lemmas

• D_diag_eq_zero — Under NoNegCycle, D ks i i = 0 for any intermediate set ks.
• Pi_D_ge — Optimal-substructure lower bound: if Pi ks i j = some k with i ≠ j, then D ks i k + w(k,j) ≤ D ks i j. Proved by induction on ks using only min_le_left/min_le_right from the D recurrence — avoids the difficult D-edge inequality entirely.
• isShortestDist_edge_ineq — Edge inequality for shortest-path distances: δ(v) ≤ δ(u) + w(u,v).
• floydWarshallPi_D_eq — Equality for the final matrices: floydWarshall i j = floydWarshall i k + w(k,j). Combines Pi_D_ge (lower bound) with isShortestDist_edge_ineq (upper bound).
• reconstructPathFuel_isWalkFrom — The reconstructed path is a valid walk.
• reconstructPathFuel_weight_eq — Main result: the reconstructed path has weight floydWarshall i j.

Key insight

The equality is proved by separating the optimal-substructure argument into two independent bounds:

• Lower bound (Pi_D_ge): uses only the algebraic min structure of the DP recurrence
• Upper bound (isShortestDist_edge_ineq): uses the existing IsShortestDist property of the final Floyd-Warshall matrices

No D-edge inequality or semantic walk-through-ks lemma is required.

Verification

lake build CLRSLean        # ✓ Build completed successfully
uv run python scripts/check_repository.py  # ✓ All checks passed

Closes #95.

🤖 Generated with Claude Code