From 6a7bedf31b5d9858f085ad22f4afc904125585bd Mon Sep 17 00:00:00 2001
From: fawad haider <153737+FawadHa1der@users.noreply.github.com>
Date: Wed, 1 Jul 2026 13:46:40 -0400
Subject: [PATCH 1/3] feat(Algorithms/Graph): add Floyd-Warshall invariant

---
 Cslib.lean                                |   1 +
 Cslib/Algorithms/Graph/FloydWarshall.lean | 228 ++++++++++++++++++++++
 2 files changed, 229 insertions(+)
 create mode 100644 Cslib/Algorithms/Graph/FloydWarshall.lean

diff --git a/Cslib.lean b/Cslib.lean
index eea1f4491..3dd9a1e8a 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,5 +1,6 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import Cslib.Algorithms.Graph.FloydWarshall
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor
diff --git a/Cslib/Algorithms/Graph/FloydWarshall.lean b/Cslib/Algorithms/Graph/FloydWarshall.lean
new file mode 100644
index 000000000..6eb8f52b6
--- /dev/null
+++ b/Cslib/Algorithms/Graph/FloydWarshall.lean
@@ -0,0 +1,228 @@
+/-
+Copyright (c) 2026 Fawad Haider. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fawad Haider
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Algebra.Order.Group.Nat
+public import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
+
+/-!
+# Floyd-Warshall
+
+This file defines finite weighted directed graphs as min-plus matrices
+`Fin n → Fin n → WithTop Nat` and proves the standard Floyd-Warshall invariant.
+
+The theorem `phase_isShortestPathWeight` states that, after phase `k`, the entry
+`phase w k i j` is the shortest weight among the restricted paths from `i` to `j`
+whose intermediate vertices are introduced by the first `k` phases.  The theorem
+`RestrictedPath.mem_intermediates_lt` records the intended interpretation of the
+phase index: every intermediate vertex of such a path has value `< k`, i.e. lies
+in `{0, ..., k - 1}`.
+-/
+
+@[expose] public section
+
+set_option autoImplicit false
+
+namespace Cslib.Algorithms.Graph.FloydWarshall
+
+/-- Edge and path weights for Floyd-Warshall: finite natural costs plus infinity. -/
+abbrev Weight := WithTop Nat
+
+/-- A finite weighted directed graph, represented as a min-plus adjacency matrix. -/
+abbrev Matrix (n : Nat) := Fin n → Fin n → Weight
+
+/-- One Floyd-Warshall relaxation step through the pivot vertex `k`. -/
+def step {n : Nat} (d : Matrix n) (k : Fin n) : Matrix n :=
+  fun i j ↦ min (d i j) (d i k + d k j)
+
+/--
+The matrix after `k` Floyd-Warshall phases.
+
+For `k ≤ n`, phase `k` has considered exactly the possible intermediate vertices
+with values `< k`.  For `k > n`, the matrix remains stable.
+-/
+def phase {n : Nat} (w : Matrix n) : Nat → Matrix n
+  | 0 => w
+  | k + 1 =>
+      if hk : k < n then
+        step (phase w k) ⟨k, hk⟩
+      else
+        phase w k
+
+/-- The all-pairs shortest-path matrix produced after all vertices have been considered. -/
+def allPairsShortestPaths {n : Nat} (w : Matrix n) : Matrix n :=
+  phase w n
+
+/--
+Restricted paths used by the Floyd-Warshall invariant.
+
+`RestrictedPath k i j` is the family of paths from `i` to `j` generated after
+the first `k` phases.  The constructor `through` is the Floyd-Warshall
+decomposition through the newly available pivot vertex.
+-/
+inductive RestrictedPath {n : Nat} : Nat → Fin n → Fin n → Type
+  | edge (i j : Fin n) : RestrictedPath 0 i j
+  | keep {k : Nat} {i j : Fin n} :
+      RestrictedPath k i j → RestrictedPath (k + 1) i j
+  | through {k : Nat} {i j : Fin n} (hk : k < n) :
+      RestrictedPath k i ⟨k, hk⟩ →
+      RestrictedPath k ⟨k, hk⟩ j →
+      RestrictedPath (k + 1) i j
+
+namespace RestrictedPath
+
+/-- The min-plus weight of a restricted path. -/
+def weight {n k : Nat} {i j : Fin n} (w : Matrix n) :
+    RestrictedPath (n := n) k i j → Weight
+  | edge i j => w i j
+  | keep p => weight w p
+  | through _ p q => weight w p + weight w q
+
+/-- The intermediate vertices of a restricted path, excluding its endpoints. -/
+def intermediates {n k : Nat} {i j : Fin n} :
+    RestrictedPath (n := n) k i j → List (Fin n)
+  | edge _ _ => []
+  | keep p => intermediates p
+  | @through _ k _ _ hk p q => intermediates p ++ [⟨k, hk⟩] ++ intermediates q
+
+/--
+All intermediate vertices of a `k`-restricted path lie among the first `k`
+vertices.
+-/
+theorem mem_intermediates_lt {n k : Nat} {i j v : Fin n}
+    {p : RestrictedPath (n := n) k i j} (hv : v ∈ intermediates p) :
+    v.val < k := by
+  induction p with
+  | edge =>
+      simp [intermediates] at hv
+  | keep p ih =>
+      exact Nat.lt_trans (ih hv) (Nat.lt_succ_self _)
+  | through hk p q ihp ihq =>
+      rw [intermediates, List.mem_append] at hv
+      rcases hv with hv | hvq
+      · rw [List.mem_append] at hv
+        rcases hv with hvp | hv
+        · exact Nat.lt_trans (ihp hvp) (Nat.lt_succ_self _)
+        · simp only [List.mem_singleton] at hv
+          subst v
+          exact Nat.lt_succ_self _
+      · exact Nat.lt_trans (ihq hvq) (Nat.lt_succ_self _)
+
+end RestrictedPath
+
+/--
+`d` is the shortest weight among the restricted paths from `i` to `j`.
+
+The first conjunct says the bound is attained by an actual restricted path; the
+second says that no restricted path has smaller weight.
+-/
+def IsShortestPathWeight {n k : Nat} (w : Matrix n) (i j : Fin n) (d : Weight) :
+    Prop :=
+  (∃ p : RestrictedPath (n := n) k i j, p.weight w = d) ∧
+    ∀ p : RestrictedPath (n := n) k i j, d ≤ p.weight w
+
+@[simp]
+theorem phase_zero {n : Nat} (w : Matrix n) : phase w 0 = w := rfl
+
+@[simp]
+theorem phase_succ_of_lt {n k : Nat} (w : Matrix n) (hk : k < n) :
+    phase w (k + 1) = step (phase w k) ⟨k, hk⟩ := by
+  simp [phase, hk]
+
+@[simp]
+theorem phase_succ_of_not_lt {n k : Nat} (w : Matrix n) (hk : ¬ k < n) :
+    phase w (k + 1) = phase w k := by
+  simp [phase, hk]
+
+private theorem phase_succ_le_keep {n k : Nat} (w : Matrix n) (i j : Fin n) :
+    phase w (k + 1) i j ≤ phase w k i j := by
+  by_cases hk : k < n
+  · simp [phase, step, hk]
+  · simp [phase, hk]
+
+private theorem phase_succ_le_through {n k : Nat} (w : Matrix n) (hk : k < n)
+    (i j : Fin n) :
+    phase w (k + 1) i j ≤ phase w k i ⟨k, hk⟩ + phase w k ⟨k, hk⟩ j := by
+  simp [phase, step, hk]
+
+/-- Every restricted path is bounded below by the corresponding Floyd-Warshall entry. -/
+theorem phase_le_weight {n k : Nat} (w : Matrix n) {i j : Fin n}
+    (p : RestrictedPath (n := n) k i j) :
+    phase w k i j ≤ p.weight w := by
+  induction p with
+  | edge =>
+      simp [phase, RestrictedPath.weight]
+  | keep p ih =>
+      exact le_trans (phase_succ_le_keep w _ _) ih
+  | through hk p q ihp ihq =>
+      exact le_trans (phase_succ_le_through w hk _ _) (add_le_add ihp ihq)
+
+/-- Each Floyd-Warshall entry is the weight of some restricted path. -/
+theorem exists_weight_eq_phase {n : Nat} (w : Matrix n) (k : Nat) :
+    ∀ i j : Fin n, ∃ p : RestrictedPath (n := n) k i j, p.weight w = phase w k i j := by
+  induction k with
+  | zero =>
+      intro i j
+      exact ⟨RestrictedPath.edge i j, by simp [phase, RestrictedPath.weight]⟩
+  | succ k ih =>
+      intro i j
+      by_cases hk : k < n
+      · let pivot : Fin n := ⟨k, hk⟩
+        obtain ⟨pKeep, hpKeep⟩ := ih i j
+        obtain ⟨pLeft, hpLeft⟩ := ih i pivot
+        obtain ⟨pRight, hpRight⟩ := ih pivot j
+        by_cases hle : phase w k i j ≤ phase w k i pivot + phase w k pivot j
+        · refine ⟨RestrictedPath.keep pKeep, ?_⟩
+          simp [RestrictedPath.weight, phase, step, hk, hpKeep]
+          simpa [pivot] using hle
+        · refine ⟨RestrictedPath.through hk pLeft pRight, ?_⟩
+          have hright : phase w k i pivot + phase w k pivot j ≤ phase w k i j :=
+            le_of_not_ge hle
+          simp [RestrictedPath.weight, phase, step, hk, hpLeft, hpRight]
+          simpa [pivot] using (min_eq_right hright).symm
+      · obtain ⟨pKeep, hpKeep⟩ := ih i j
+        refine ⟨RestrictedPath.keep pKeep, ?_⟩
+        simp [RestrictedPath.weight, phase, hk, hpKeep]
+
+/--
+Floyd-Warshall phase invariant.
+
+After phase `k`, each matrix entry is the shortest weight among the paths whose
+intermediate vertices are available in the first `k` phases.
+-/
+theorem phase_isShortestPathWeight {n : Nat} (w : Matrix n) (k : Nat) (i j : Fin n) :
+    IsShortestPathWeight (n := n) (k := k) w i j (phase w k i j) :=
+  ⟨exists_weight_eq_phase w k i j, fun p ↦ phase_le_weight w p⟩
+
+/-- The final Floyd-Warshall matrix gives shortest restricted paths using all vertices. -/
+theorem allPairsShortestPaths_isShortestPathWeight {n : Nat} (w : Matrix n) (i j : Fin n) :
+    IsShortestPathWeight (n := n) (k := n) w i j (allPairsShortestPaths w i j) :=
+  phase_isShortestPathWeight w n i j
+
+/--
+Warshall-style reachability corollary: the phase entry is finite exactly when
+there exists a finite-weight restricted path.
+-/
+theorem phase_lt_top_iff_exists_weight_lt_top {n k : Nat} (w : Matrix n) (i j : Fin n) :
+    phase w k i j < ⊤ ↔
+      ∃ p : RestrictedPath (n := n) k i j, p.weight w < ⊤ := by
+  constructor
+  · intro h
+    obtain ⟨p, hp⟩ := exists_weight_eq_phase w k i j
+    exact ⟨p, by simpa [hp] using h⟩
+  · rintro ⟨p, hp⟩
+    exact lt_of_le_of_lt (phase_le_weight w p) hp
+
+/-- Final reachability corollary for the all-pairs matrix. -/
+theorem allPairsShortestPaths_lt_top_iff_exists_weight_lt_top {n : Nat}
+    (w : Matrix n) (i j : Fin n) :
+    allPairsShortestPaths w i j < ⊤ ↔
+      ∃ p : RestrictedPath (n := n) n i j, p.weight w < ⊤ :=
+  phase_lt_top_iff_exists_weight_lt_top w i j
+
+end Cslib.Algorithms.Graph.FloydWarshall

From 25de8914a49e360987f11cd31720f9989e88da68 Mon Sep 17 00:00:00 2001
From: fawad haider <153737+FawadHa1der@users.noreply.github.com>
Date: Thu, 2 Jul 2026 12:28:41 -0400
Subject: [PATCH 2/3] feat(Algorithms/Graph):path object exists only if it is
 made from finite input edges

---
 Cslib/Algorithms/Graph/FloydWarshall.lean | 123 ++++++++++++++--------
 1 file changed, 77 insertions(+), 46 deletions(-)

diff --git a/Cslib/Algorithms/Graph/FloydWarshall.lean b/Cslib/Algorithms/Graph/FloydWarshall.lean
index 6eb8f52b6..caeb54e0c 100644
--- a/Cslib/Algorithms/Graph/FloydWarshall.lean
+++ b/Cslib/Algorithms/Graph/FloydWarshall.lean
@@ -18,7 +18,8 @@ This file defines finite weighted directed graphs as min-plus matrices
 
 The theorem `phase_isShortestPathWeight` states that, after phase `k`, the entry
 `phase w k i j` is the shortest weight among the restricted paths from `i` to `j`
-whose intermediate vertices are introduced by the first `k` phases.  The theorem
+whose direct edges are finite in `w` and whose intermediate vertices are
+introduced by the first `k` phases.  The theorem
 `RestrictedPath.mem_intermediates_lt` records the intended interpretation of the
 phase index: every intermediate vertex of such a path has value `< k`, i.e. lies
 in `{0, ..., k - 1}`.
@@ -59,43 +60,56 @@ def allPairsShortestPaths {n : Nat} (w : Matrix n) : Matrix n :=
   phase w n
 
 /--
-Restricted paths used by the Floyd-Warshall invariant.
+Input-graph-valid restricted paths used by the Floyd-Warshall invariant.
 
-`RestrictedPath k i j` is the family of paths from `i` to `j` generated after
-the first `k` phases.  The constructor `through` is the Floyd-Warshall
-decomposition through the newly available pivot vertex.
+`RestrictedPath w k i j` is the family of paths from `i` to `j` generated after
+the first `k` phases.  The constructor `edge` requires a finite edge in the input
+matrix `w`; the constructor `through` is the Floyd-Warshall decomposition through
+the newly available pivot vertex.
 -/
-inductive RestrictedPath {n : Nat} : Nat → Fin n → Fin n → Type
-  | edge (i j : Fin n) : RestrictedPath 0 i j
+inductive RestrictedPath {n : Nat} (w : Matrix n) : Nat → Fin n → Fin n → Type
+  | edge {i j : Fin n} (h : w i j < ⊤) : RestrictedPath w 0 i j
   | keep {k : Nat} {i j : Fin n} :
-      RestrictedPath k i j → RestrictedPath (k + 1) i j
+      RestrictedPath w k i j → RestrictedPath w (k + 1) i j
   | through {k : Nat} {i j : Fin n} (hk : k < n) :
-      RestrictedPath k i ⟨k, hk⟩ →
-      RestrictedPath k ⟨k, hk⟩ j →
-      RestrictedPath (k + 1) i j
+      RestrictedPath w k i ⟨k, hk⟩ →
+      RestrictedPath w k ⟨k, hk⟩ j →
+      RestrictedPath w (k + 1) i j
 
 namespace RestrictedPath
 
 /-- The min-plus weight of a restricted path. -/
-def weight {n k : Nat} {i j : Fin n} (w : Matrix n) :
-    RestrictedPath (n := n) k i j → Weight
-  | edge i j => w i j
-  | keep p => weight w p
-  | through _ p q => weight w p + weight w q
+def weight {n k : Nat} {w : Matrix n} {i j : Fin n} :
+    RestrictedPath w k i j → Weight
+  | @edge _ w i j _ => w i j
+  | keep p => weight p
+  | through _ p q => weight p + weight q
 
 /-- The intermediate vertices of a restricted path, excluding its endpoints. -/
-def intermediates {n k : Nat} {i j : Fin n} :
-    RestrictedPath (n := n) k i j → List (Fin n)
-  | edge _ _ => []
+def intermediates {n k : Nat} {w : Matrix n} {i j : Fin n} :
+    RestrictedPath w k i j → List (Fin n)
+  | edge _ => []
   | keep p => intermediates p
-  | @through _ k _ _ hk p q => intermediates p ++ [⟨k, hk⟩] ++ intermediates q
+  | @through _ _ k _ _ hk p q => intermediates p ++ [⟨k, hk⟩] ++ intermediates q
+
+/-- Restricted paths have finite weight. -/
+theorem weight_lt_top {n k : Nat} {w : Matrix n} {i j : Fin n}
+    (p : RestrictedPath w k i j) :
+    p.weight < ⊤ := by
+  induction p with
+  | edge h =>
+      simpa [weight] using h
+  | keep p ih =>
+      simpa [weight] using ih
+  | through _ p q ihp ihq =>
+      simpa [weight] using And.intro ihp ihq
 
 /--
 All intermediate vertices of a `k`-restricted path lie among the first `k`
 vertices.
 -/
-theorem mem_intermediates_lt {n k : Nat} {i j v : Fin n}
-    {p : RestrictedPath (n := n) k i j} (hv : v ∈ intermediates p) :
+theorem mem_intermediates_lt {n k : Nat} {w : Matrix n} {i j v : Fin n}
+    {p : RestrictedPath w k i j} (hv : v ∈ intermediates p) :
     v.val < k := by
   induction p with
   | edge =>
@@ -116,15 +130,16 @@ theorem mem_intermediates_lt {n k : Nat} {i j v : Fin n}
 end RestrictedPath
 
 /--
-`d` is the shortest weight among the restricted paths from `i` to `j`.
+`d` is the shortest weight among the input-graph-valid restricted paths from `i` to `j`.
 
-The first conjunct says the bound is attained by an actual restricted path; the
-second says that no restricted path has smaller weight.
+The first conjunct says that no restricted path has smaller weight.  The second
+conjunct says that, if the shortest weight is finite, then the bound is attained
+by an actual restricted path.
 -/
 def IsShortestPathWeight {n k : Nat} (w : Matrix n) (i j : Fin n) (d : Weight) :
     Prop :=
-  (∃ p : RestrictedPath (n := n) k i j, p.weight w = d) ∧
-    ∀ p : RestrictedPath (n := n) k i j, d ≤ p.weight w
+  (∀ p : RestrictedPath w k i j, d ≤ p.weight) ∧
+    (d < ⊤ → ∃ p : RestrictedPath w k i j, p.weight = d)
 
 @[simp]
 theorem phase_zero {n : Nat} (w : Matrix n) : phase w 0 = w := rfl
@@ -152,8 +167,8 @@ private theorem phase_succ_le_through {n k : Nat} (w : Matrix n) (hk : k < n)
 
 /-- Every restricted path is bounded below by the corresponding Floyd-Warshall entry. -/
 theorem phase_le_weight {n k : Nat} (w : Matrix n) {i j : Fin n}
-    (p : RestrictedPath (n := n) k i j) :
-    phase w k i j ≤ p.weight w := by
+    (p : RestrictedPath w k i j) :
+    phase w k i j ≤ p.weight := by
   induction p with
   | edge =>
       simp [phase, RestrictedPath.weight]
@@ -162,30 +177,46 @@ theorem phase_le_weight {n k : Nat} (w : Matrix n) {i j : Fin n}
   | through hk p q ihp ihq =>
       exact le_trans (phase_succ_le_through w hk _ _) (add_le_add ihp ihq)
 
-/-- Each Floyd-Warshall entry is the weight of some restricted path. -/
-theorem exists_weight_eq_phase {n : Nat} (w : Matrix n) (k : Nat) :
-    ∀ i j : Fin n, ∃ p : RestrictedPath (n := n) k i j, p.weight w = phase w k i j := by
+/-- Each finite Floyd-Warshall entry is the weight of some restricted path. -/
+theorem exists_weight_eq_phase_of_lt_top {n : Nat} (w : Matrix n) (k : Nat) :
+    ∀ i j : Fin n, phase w k i j < ⊤ →
+      ∃ p : RestrictedPath w k i j, p.weight = phase w k i j := by
   induction k with
   | zero =>
-      intro i j
-      exact ⟨RestrictedPath.edge i j, by simp [phase, RestrictedPath.weight]⟩
+      intro i j h
+      exact ⟨RestrictedPath.edge h, by simp [phase, RestrictedPath.weight]⟩
   | succ k ih =>
-      intro i j
+      intro i j h
       by_cases hk : k < n
       · let pivot : Fin n := ⟨k, hk⟩
-        obtain ⟨pKeep, hpKeep⟩ := ih i j
-        obtain ⟨pLeft, hpLeft⟩ := ih i pivot
-        obtain ⟨pRight, hpRight⟩ := ih pivot j
         by_cases hle : phase w k i j ≤ phase w k i pivot + phase w k pivot j
-        · refine ⟨RestrictedPath.keep pKeep, ?_⟩
+        · have hKeep : phase w k i j < ⊤ := by
+            have hmin :
+                min (phase w k i j) (phase w k i pivot + phase w k pivot j) < ⊤ := by
+              simpa [phase, step, hk, pivot] using h
+            rwa [min_eq_left hle] at hmin
+          obtain ⟨pKeep, hpKeep⟩ := ih i j hKeep
+          refine ⟨RestrictedPath.keep pKeep, ?_⟩
           simp [RestrictedPath.weight, phase, step, hk, hpKeep]
           simpa [pivot] using hle
-        · refine ⟨RestrictedPath.through hk pLeft pRight, ?_⟩
-          have hright : phase w k i pivot + phase w k pivot j ≤ phase w k i j :=
+        · have hright : phase w k i pivot + phase w k pivot j ≤ phase w k i j :=
             le_of_not_ge hle
+          have hThrough :
+              phase w k i pivot + phase w k pivot j < ⊤ := by
+            have hmin :
+                min (phase w k i j) (phase w k i pivot + phase w k pivot j) < ⊤ := by
+              simpa [phase, step, hk, pivot] using h
+            rwa [min_eq_right hright] at hmin
+          have hLeft : phase w k i pivot < ⊤ := (WithTop.add_lt_top.mp hThrough).1
+          have hRight : phase w k pivot j < ⊤ := (WithTop.add_lt_top.mp hThrough).2
+          obtain ⟨pLeft, hpLeft⟩ := ih i pivot hLeft
+          obtain ⟨pRight, hpRight⟩ := ih pivot j hRight
+          refine ⟨RestrictedPath.through hk pLeft pRight, ?_⟩
           simp [RestrictedPath.weight, phase, step, hk, hpLeft, hpRight]
           simpa [pivot] using (min_eq_right hright).symm
-      · obtain ⟨pKeep, hpKeep⟩ := ih i j
+      · have hPrev : phase w k i j < ⊤ := by
+          simpa [phase, hk] using h
+        obtain ⟨pKeep, hpKeep⟩ := ih i j hPrev
         refine ⟨RestrictedPath.keep pKeep, ?_⟩
         simp [RestrictedPath.weight, phase, hk, hpKeep]
 
@@ -197,7 +228,7 @@ intermediate vertices are available in the first `k` phases.
 -/
 theorem phase_isShortestPathWeight {n : Nat} (w : Matrix n) (k : Nat) (i j : Fin n) :
     IsShortestPathWeight (n := n) (k := k) w i j (phase w k i j) :=
-  ⟨exists_weight_eq_phase w k i j, fun p ↦ phase_le_weight w p⟩
+  ⟨fun p ↦ phase_le_weight w p, exists_weight_eq_phase_of_lt_top w k i j⟩
 
 /-- The final Floyd-Warshall matrix gives shortest restricted paths using all vertices. -/
 theorem allPairsShortestPaths_isShortestPathWeight {n : Nat} (w : Matrix n) (i j : Fin n) :
@@ -210,10 +241,10 @@ there exists a finite-weight restricted path.
 -/
 theorem phase_lt_top_iff_exists_weight_lt_top {n k : Nat} (w : Matrix n) (i j : Fin n) :
     phase w k i j < ⊤ ↔
-      ∃ p : RestrictedPath (n := n) k i j, p.weight w < ⊤ := by
+      ∃ p : RestrictedPath w k i j, p.weight < ⊤ := by
   constructor
   · intro h
-    obtain ⟨p, hp⟩ := exists_weight_eq_phase w k i j
+    obtain ⟨p, hp⟩ := exists_weight_eq_phase_of_lt_top w k i j h
     exact ⟨p, by simpa [hp] using h⟩
   · rintro ⟨p, hp⟩
     exact lt_of_le_of_lt (phase_le_weight w p) hp
@@ -222,7 +253,7 @@ theorem phase_lt_top_iff_exists_weight_lt_top {n k : Nat} (w : Matrix n) (i j :
 theorem allPairsShortestPaths_lt_top_iff_exists_weight_lt_top {n : Nat}
     (w : Matrix n) (i j : Fin n) :
     allPairsShortestPaths w i j < ⊤ ↔
-      ∃ p : RestrictedPath (n := n) n i j, p.weight w < ⊤ :=
+      ∃ p : RestrictedPath w n i j, p.weight < ⊤ :=
   phase_lt_top_iff_exists_weight_lt_top w i j
 
 end Cslib.Algorithms.Graph.FloydWarshall

From 11574d772f3f798b6af307c9a0c7f638fce982c3 Mon Sep 17 00:00:00 2001
From: fawad haider <153737+FawadHa1der@users.noreply.github.com>
Date: Thu, 2 Jul 2026 12:32:26 -0400
Subject: [PATCH 3/3] feat(Algorithms/Graph): update authors to reflect AI use

---
 Cslib/Algorithms/Graph/FloydWarshall.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Graph/FloydWarshall.lean b/Cslib/Algorithms/Graph/FloydWarshall.lean
index caeb54e0c..1459c069a 100644
--- a/Cslib/Algorithms/Graph/FloydWarshall.lean
+++ b/Cslib/Algorithms/Graph/FloydWarshall.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Fawad Haider. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fawad Haider
+Authors: OpenAI, Fawad Haider
 -/
 
 module