Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 23. All-Pairs Shortest Paths
  4. 23.1. All-Pairs Shortest Paths Model
Browse chapters
Imports
import Mathlib import CLRSLean.FourthEdition.Chapter_22.Section_22_1_Bellman_Ford

23.1. All-Pairs Shortest Paths Model

Definitions and basic properties of the all-pairs shortest-path model: edge-weight matrix, min-plus product, FASTER-APSP.

Main results:

  • CLRS.Chapter24.WeightedGraph.minPlusMul: the min-plus matrix product.

  • CLRS.Chapter24.WeightedGraph.fasterAPSP: CLRS FASTER-APSP (repeated squaring).

  • CLRS.Chapter24.WeightedGraph.lemma_25_1: Lemma 23.1 (L^(m+1) = L^m ◁ W).

  • CLRS.Chapter24.WeightedGraph.L_sq_eq_minPlusMul: Lemma 23.2 (L^(2m) = L^m ◁ L^m).

  • CLRS.Chapter24.WeightedGraph.fasterAPSP_eq_L: FASTER-APSP equals L^(|V|-1) under NoNegCycle.

  • CLRS.Chapter24.WeightedGraph.fasterAPSP_eq_shortestDist: FASTER-APSP correctness.

  • minPlusMulCost, fasterAPSPCost — min-plus candidate budgets. The separate MatrixExecution companion realizes them with stored tables.

  • numSquarings_le_log2_add_one — the iteration count is O(log |V|).

  • fasterAPSPCost_le_n_cubed_log — O(V³ log V) repeated-squaring work.

  • fasterAPSPCost_le_n_four — trivial O(V⁴) corollary.

The recursive function-valued specification does not itself establish shared table evaluation. Stored execution and counts are in the matrix companion.

namespace CLRSnamespace Chapter24open Finsetnamespace WeightedGraphvariable {V : Type*} [Fintype V] [DecidableEq V] (G : WeightedGraph V)

Edge-weight matrix W.

def weightMatrix (i j : V) : WithTop ℝ := if i = j then (0 : WithTop ℝ) else if G.Adj i j then (G.w i j : WithTop ℝ) else ⊤

Min-plus matrix product: (A ◁ B)ij = mink (Aik + Bkj).

def minPlusMul (A B : V → V → WithTop ℝ) (i j : V) : WithTop ℝ := (Finset.univ : Finset V).inf (fun k => A i k + B k j)

EXTEND-SHORTEST-PATHS: L' = L ◁ W.

def extendShortestPaths (L : V → V → WithTop ℝ) (i j : V) : WithTop ℝ := minPlusMul L G.weightMatrix i j

L m — shortest-path weights using at most m edges.

def L (G : WeightedGraph V) : ℕ → V → V → WithTop ℝ | 0, i, j => if i = j then (0 : WithTop ℝ) else ⊤ | m + 1, i, j => G.extendShortestPaths (G.L m) i j
@[simp] theorem L_zero (i j : V) : G.L 0 i j = if i = j then (0 : WithTop ℝ) else ⊤ := rfl@[simp] theorem L_succ (m : ℕ) (i j : V) : G.L (m + 1) i j = G.extendShortestPaths (G.L m) i j := rfl

Number of squarings: ceil(log2(|V|-1)).

def Overlapping instance parameters in `numSquarings`: ⚠️ There are 2 `[Fintype V]` instances; one is sufficient. Note: This linter can be disabled with `set_option linter.overlappingInstances false`numSquarings [Fintype V] : ℕ := let x := Fintype.card V - 1 if x ≤ 1 then 0 else Nat.log2 (x - 1) + 1

FASTER-APSP: repeatedly square L = L ◁ L.

def Overlapping instance parameters in `fasterAPSP`: ⚠️ There are 2 `[Fintype V]` instances; one is sufficient. Note: This linter can be disabled with `set_option linter.overlappingInstances false`fasterAPSP [Fintype V] (G : WeightedGraph V) : V → V → WithTop ℝ := (fun L => minPlusMul L L)^[numSquarings (V := V)] G.weightMatrix

Identity matrix for min-plus multiplication.

def identityMatrix (i j : V) : WithTop ℝ := if i = j then (0 : WithTop ℝ) else ⊤
automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.identityMatrix_diag`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.identityMatrix_diag`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` @[simp] automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.identityMatrix_diag`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem identityMatrix_diag (i : V) : identityMatrix i i = (0 : WithTop ℝ) := by simp [identityMatrix]automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.identityMatrix_offdiag`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.identityMatrix_offdiag`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` @[simp] automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.identityMatrix_offdiag`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem identityMatrix_offdiag {i j : V} (h : i ≠ j) : identityMatrix i j = ⊤ := by simp [identityMatrix, h] theorem minPlusMul_identity_left (M : V → V → WithTop ℝ) (i j : V) : minPlusMul identityMatrix M i j = M i j := by unfold minPlusMul identityMatrix have h1 : (Finset.univ : Finset V).inf (fun k : V => (if i = k then (0 : WithTop ℝ) else ⊤) + M k j) ≤ M i j := by calc (Finset.univ : Finset V).inf (fun k : V => (if i = k then (0 : WithTop ℝ) else ⊤) + M k j) ≤ ((fun k : V => (if i = k then (0 : WithTop ℝ) else ⊤) + M k j) i) := Finset.inf_le (Finset.mem_univ i) _ = M i j := by simp have h2 : M i j ≤ (Finset.univ : Finset V).inf (fun k : V => (if i = k then (0 : WithTop ℝ) else ⊤) + M k j) := by apply Finset.le_inf intro k hk by_cases hik : i = k · subst k; simp · simp [hik] exact le_antisymm h1 h2 theorem minPlusMul_identity_right (M : V → V → WithTop ℝ) (i j : V) : minPlusMul M identityMatrix i j = M i j := by unfold minPlusMul identityMatrix have h1 : (Finset.univ : Finset V).inf (fun k : V => M i k + (if k = j then (0 : WithTop ℝ) else ⊤)) ≤ M i j := by calc (Finset.univ : Finset V).inf (fun k : V => M i k + (if k = j then (0 : WithTop ℝ) else ⊤)) ≤ ((fun k : V => M i k + (if k = j then (0 : WithTop ℝ) else ⊤)) j) := Finset.inf_le (Finset.mem_univ j) _ = M i j := by simp have h2 : M i j ≤ (Finset.univ : Finset V).inf (fun k : V => M i k + (if k = j then (0 : WithTop ℝ) else ⊤)) := by apply Finset.le_inf intro k hk by_cases hkj : k = j · subst k; simp · simp [hkj] exact le_antisymm h1 h2

Lemmas 23.1 and 23.2 (squaring identity)

Lemma 23.1. L^(m+1) = L^m ◁ W. A single EXTEND-SHORTEST-PATHS step is the min-plus product of the current shortest-path matrix with the weight matrix.

theorem lemma_25_1 (m : ℕ) (i j : V) : G.L (m + 1) i j = minPlusMul (G.L m) G.weightMatrix i j := by simp [L_succ, extendShortestPaths]

The function a + · distributes over ⊓ in WithTop ℝ.

lemma add_inf_distrib (a b c : WithTop ℝ) : a + (b ⊓ c) = (a + b) ⊓ (a + c) := by induction a using WithTop.recTopCoe with | top => simp | coe a' => induction b using WithTop.recTopCoe with | top => simp | coe b' => induction c using WithTop.recTopCoe with | top => simp | coe c' => simpa [WithTop.coe_add] using (congrArg (WithTop.some : ℝ → WithTop ℝ) (min_add_add_left a' b' c')).symm

Addition distributes over Finset.inf for nonempty sets.

automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.add_inf`: [Fintype V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`lemma add_inf (a : WithTop ℝ) (s : Finset V) (hs : s.Nonempty) (f : V → WithTop ℝ) : a + s.inf f = s.inf (fun x => a + f x) := by induction' s using Finset.induction_on with x s hx ih · exfalso; exact Finset.not_nonempty_empty hs · rw [Finset.inf_insert, Finset.inf_insert] by_cases hne : s.Nonempty · have h_ih := ih hne rw [← h_ih, add_inf_distrib] · have h_empty : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hne subst h_empty simp

Min-plus matrix multiplication is associative.

theorem minPlusMul_assoc (A B C : V → V → WithTop ℝ) (i j : V) : minPlusMul (minPlusMul A B) C i j = minPlusMul A (minPlusMul B C) i j := by unfold minPlusMul by_cases huniv : (Finset.univ : Finset V).Nonempty · have h_add_inf (a : WithTop ℝ) (f : V → WithTop ℝ) : a + (univ : Finset V).inf f = (univ : Finset V).inf (fun x => a + f x) := add_inf a (univ : Finset V) huniv f have hswap_inf (f : V → V → WithTop ℝ) : (univ : Finset V).inf (fun k : V => (univ : Finset V).inf (fun l : V => f k l)) = (univ : Finset V).inf (fun l : V => (univ : Finset V).inf (fun k : V => f k l)) := by calc (univ : Finset V).inf (fun k : V => (univ : Finset V).inf (fun l : V => f k l)) = (univ ×ˢ univ : Finset (V × V)).inf (fun (p : V × V) => f p.1 p.2) := by rw [inf_product_left] _ = (univ : Finset V).inf (fun l : V => (univ : Finset V).inf (fun k : V => f k l)) := by rw [inf_product_right] calc (univ : Finset V).inf (fun k : V => ((univ : Finset V).inf (fun l : V => A i l + B l k)) + C k j) = (univ : Finset V).inf (fun k : V => (univ : Finset V).inf (fun l : V => (A i l + B l k) + C k j)) := by refine Finset.inf_congr rfl (fun k hk => ?_) rw [add_comm, h_add_inf (C k j) (fun l : V => A i l + B l k)] refine Finset.inf_congr rfl (fun l hl => ?_) exact add_comm (C k j) (A i l + B l k) _ = (univ : Finset V).inf (fun l : V => (univ : Finset V).inf (fun k : V => (A i l + B l k) + C k j)) := by rw [hswap_inf (fun k l => (A i l + B l k) + C k j)] _ = (univ : Finset V).inf (fun l : V => (univ : Finset V).inf (fun k : V => A i l + (B l k + C k j))) := by refine Finset.inf_congr rfl (fun l hl => ?_) refine Finset.inf_congr rfl (fun k hk => ?_) simp [add_assoc] _ = (univ : Finset V).inf (fun l : V => A i l + (univ : Finset V).inf (fun k : V => B l k + C k j)) := by refine Finset.inf_congr rfl (fun l hl => ?_) rw [(h_add_inf (A i l) (fun k : V => B l k + C k j)).symm] · -- univ is empty have hempty : (Finset.univ : Finset V) = ∅ := Finset.not_nonempty_iff_eq_empty.mp huniv simp [hempty]

L (a + b) = (L a) ◁ (L b) for all a, b. General additive property of the shortest-path matrix.

theorem L_add_eq_minPlusMul (a b : ℕ) (i j : V) : G.L (a + b) i j = minPlusMul (G.L a) (G.L b) i j := by induction' b with b ih generalizing i j · -- b = 0: L (a+0) = L a = L a ◁ L 0 (since L 0 = identityMatrix) have hL0 : G.L (0 : ℕ) = identityMatrix := by ext i' j'; simp [L_zero, identityMatrix] rw [hL0, minPlusMul_identity_right] simp · have h_funext : G.L (a + b) = minPlusMul (G.L a) (G.L b) := by ext i' j'; exact ih i' j' calc G.L (a + (b + 1)) i j = G.L ((a + b) + 1) i j := by rw [add_assoc] _ = minPlusMul (G.L (a + b)) G.weightMatrix i j := by simp [extendShortestPaths] _ = minPlusMul (minPlusMul (G.L a) (G.L b)) G.weightMatrix i j := by rw [h_funext] _ = minPlusMul (G.L a) (minPlusMul (G.L b) G.weightMatrix) i j := by rw [minPlusMul_assoc] _ = minPlusMul (G.L a) (G.L (b + 1)) i j := by have hLb1 : G.L (b + 1) = minPlusMul (G.L b) G.weightMatrix := by ext i' j'; simpa using lemma_25_1 G b i' j' rw [← hLb1]

Lemma 23.2 (squaring identity). L^(2m) = L^m ◁ L^m.

theorem L_sq_eq_minPlusMul (m : ℕ) (i j : V) : G.L (2 * m) i j = minPlusMul (G.L m) (G.L m) i j := by calc G.L (2 * m) i j = G.L (m + m) i j := by rw [two_mul] _ = minPlusMul (G.L m) (G.L m) i j := by rw [L_add_eq_minPlusMul]

Stabilisation and FASTER-APSP correctness

L is monotone nonincreasing in m: using more edges cannot increase the shortest-path weight.

theorem L_monotone (m : ℕ) (i j : V) : G.L (m + 1) i j ≤ G.L m i j := by calc G.L (m + 1) i j = minPlusMul (G.L m) G.weightMatrix i j := lemma_25_1 G m i j _ ≤ (G.L m) i j + G.weightMatrix j j := Finset.inf_le (Finset.mem_univ j) _ = (G.L m) i j := by simp [weightMatrix]

Under NoNegCycle, the univ infimum over A u + weightMatrix u j equals min(A j, (preds j).inf (A u + w u j)). This bridges the min-plus product to the Bellman-Ford relaxation step.

lemma inf_univ_weightMatrix_eq_min_preds (hNC : G.NoNegCycle) (A : V → WithTop ℝ) (j : V) : (Finset.univ : Finset V).inf (fun u => A u + G.weightMatrix u j) = min (A j) ((G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ))) := by have h_nonneg_self_loop : G.Adj j j → (0 : WithTop ℝ) ≤ (G.w j j : WithTop ℝ) := by intro h_adj have h_nonneg_real : (0 : ℝ) ≤ G.w j j := by have h_walk : G.IsWalkFrom j j [j, j] := ⟨(List.isChain_pair.mpr h_adj), by simp, by simp⟩ have h_nonneg_cycle := hNC j [j, j] h_walk simpa [walkWeight] using h_nonneg_cycle exact WithTop.coe_le_coe.mpr h_nonneg_real apply le_antisymm · -- LHS <= RHS refine le_min ?_ (Finset.le_inf ?_) · -- LHS <= A j calc (Finset.univ : Finset V).inf (fun u => A u + G.weightMatrix u j) <= A j + G.weightMatrix j j := Finset.inf_le (Finset.mem_univ j) _ = A j := by simp [weightMatrix] · -- LHS <= A u + w u j for each u in preds j intro u hu have hu_edge : (u, j) ∈ G.edges := by simpa using hu by_cases h_uj : u = j · subst u have h_wjj_nonneg : (0 : WithTop ℝ) <= (G.w j j : WithTop ℝ) := h_nonneg_self_loop hu_edge calc (Finset.univ : Finset V).inf (fun u' => A u' + G.weightMatrix u' j) <= A j + G.weightMatrix j j := Finset.inf_le (Finset.mem_univ j) _ = A j := by simp [weightMatrix] _ = A j + (0 : WithTop ℝ) := by simp _ <= A j + (G.w j j : WithTop ℝ) := by simpa [add_comm] using add_le_add_left h_wjj_nonneg (A j) · calc (Finset.univ : Finset V).inf (fun u' => A u' + G.weightMatrix u' j) <= A u + G.weightMatrix u j := Finset.inf_le (Finset.mem_univ u) _ = A u + (G.w u j : WithTop ℝ) := by have hW : G.weightMatrix u j = (G.w u j : WithTop ℝ) := by dsimp [weightMatrix] have h_adj : G.Adj u j := hu_edge simp [h_uj, h_adj] rw [hW] · -- RHS <= LHS apply Finset.le_inf intro u hu by_cases h_uj : u = j · subst u calc min (A j) ((G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ))) <= A j := min_le_left _ _ _ = A j + G.weightMatrix j j := by simp [weightMatrix] · by_cases hu_preds : u ∈ G.preds j · have hu_edge : (u, j) ∈ G.edges := by simpa using hu_preds calc min (A j) ((G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ))) <= (G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ)) := min_le_right _ _ _ <= A u + (G.w u j : WithTop ℝ) := by simpa using Finset.inf_le hu_preds _ = A u + G.weightMatrix u j := by have hW : G.weightMatrix u j = (G.w u j : WithTop ℝ) := by dsimp [weightMatrix] have h_adj : G.Adj u j := hu_edge simp [h_uj, h_adj] rw [hW] · have h_no_edge : (u, j) ∉ G.edges := by simpa using hu_preds calc min (A j) ((G.preds j).inf (fun u => A u + (G.w u j : WithTop ℝ))) <= ⊤ := le_top _ = A u + G.weightMatrix u j := by have hW : G.weightMatrix u j = ⊤ := by have h_no_adj : ¬ G.Adj u j := by intro h_adj; apply h_no_edge; exact h_adj dsimp [weightMatrix]; simp [h_uj, h_no_adj] rw [hW]; simp
Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead. theorem L_succ_eq_relaxDist_succ (hNC : G.NoNegCycle) (k : ℕ) (i j : V) : G.L (k + 1) i j = G.relaxDist i (k + 1) j := by induction' k with k ih generalizing i j · -- k = 0: L 1 = relaxDist i 1 have h_inf : (Finset.univ : Finset V).inf (fun u => (G.relaxDist i 0) u + G.weightMatrix u j) = G.weightMatrix i j := by apply le_antisymm · calc (Finset.univ : Finset V).inf (fun u => (G.relaxDist i 0) u + G.weightMatrix u j) ≤ (G.relaxDist i 0) i + G.weightMatrix i j := Finset.inf_le (Finset.mem_univ i) _ = (0 : WithTop ℝ) + G.weightMatrix i j := by simp [relaxDist_zero_apply] _ = G.weightMatrix i j := by simp · apply Finset.le_inf intro u hu by_cases h_ui : u = i · subst u; simp [relaxDist_zero_apply] · simp [relaxDist_zero_apply, h_ui] have hL0 : G.L 0 = identityMatrix := by ext i' j'; simp [L_zero, identityMatrix] calc G.L 1 i j = minPlusMul (G.L 0) G.weightMatrix i j := by simp [L_succ, extendShortestPaths] _ = minPlusMul identityMatrix G.weightMatrix i j := by rw [hL0] _ = G.weightMatrix i j := by simp [minPlusMul_identity_left] _ = (Finset.univ : Finset V).inf (fun u => (G.relaxDist i 0) u + G.weightMatrix u j) := by rw [h_inf] _ = min (G.relaxDist i 0 j) ((G.preds j).inf (fun u => G.relaxDist i 0 u + (G.w u j : WithTop ℝ))) := inf_univ_weightMatrix_eq_min_preds (G := G) hNC (G.relaxDist i 0) j _ = G.relaxDist i 1 j := by simp [relaxDist_succ_apply, relaxStep] · -- k → k+1 have h_IH_fun : ∀ u : V, G.L (k + 1) i u = G.relaxDist i (k + 1) u := by exact ih i calc G.L ((k + 1) + 1) i j = G.L (k + 2) i j := by Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring _ = minPlusMul (G.L (k + 1)) G.weightMatrix i j := by simp [L_succ, extendShortestPaths] _ = (Finset.univ : Finset V).inf (fun u => G.L (k + 1) i u + G.weightMatrix u j) := rfl _ = min (G.L (k + 1) i j) ((G.preds j).inf (fun u => G.L (k + 1) i u + (G.w u j : WithTop ℝ))) := inf_univ_weightMatrix_eq_min_preds (G := G) hNC (λ u => G.L (k + 1) i u) j _ = min (G.relaxDist i (k + 1) j) ((G.preds j).inf (fun u => G.relaxDist i (k + 1) u + (G.w u j : WithTop ℝ))) := by have h_preds_inf : (G.preds j).inf (fun u => G.L (k + 1) i u + (G.w u j : WithTop ℝ)) = (G.preds j).inf (fun u => G.relaxDist i (k + 1) u + (G.w u j : WithTop ℝ)) := by refine Finset.inf_congr rfl (fun u hu => ?_) rw [h_IH_fun u] rw [h_IH_fun j, h_preds_inf] _ = G.relaxStep (G.relaxDist i (k + 1)) j := rfl _ = G.relaxDist i (k + 2) j := by simp [relaxDist_succ_apply] _ = G.relaxDist i ((k + 1) + 1) j := by Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring

Under NoNegCycle, L k i j = relaxDist i k j for all k.

theorem L_eq_relaxDist (hNC : G.NoNegCycle) (k : ℕ) (i j : V) : G.L k i j = G.relaxDist i k j := by cases' k with k · simp [L_zero, relaxDist_zero_apply, eq_comm] · rw [L_succ_eq_relaxDist_succ (G := G) hNC k i j]

Under NoNegCycle, L stabilises at |V|-1: for all m ≥ |V|-1, L m = L (|V|-1).

theorem L_stabilizes (hNC : G.NoNegCycle) (m : ℕ) (hm : Fintype.card V - 1 ≤ m) (i j : V) : G.L m i j = G.L (Fintype.card V - 1) i j := by rw [L_eq_relaxDist (G := G) hNC m i j, L_eq_relaxDist (G := G) hNC (Fintype.card V - 1) i j] apply le_antisymm · -- relaxDist i m j ≤ relaxDist i (|V|-1) j: more rounds give better (lower) estimate have h_mono : ∀ (k : ℕ), G.relaxDist i (k + 1) j ≤ G.relaxDist i k j := fun k => G.relaxDist_succ_le i k j exact Nat.le_induction (le_refl _) (fun k hk hk_ih => le_trans (h_mono k) hk_ih) m hm · -- relaxDist i (|V|-1) j ≤ relaxDist i m j: (|V|-1) rounds already gives the shortest distance rcases G.relaxDist_isShortestDist hNC i j with ⟨h_lower, _⟩ rcases G.exists_walk_of_relaxDist i m j with (htop | ⟨p, hp, hlen, hp_eq⟩) · rw [htop]; exact le_top · calc G.relaxDist i (Fintype.card V - 1) j ≤ (walkWeight G.w p : WithTop ℝ) := h_lower p hp _ = G.relaxDist i m j := by rw [hp_eq]

fasterAPSP iterates k times the function f(L) = L ◁ L applied to the weight matrix, which gives L (2^k).

Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead. theorem fasterAPSP_iterate_eq_L (k : ℕ) (i j : V) : ((fun (M : V → V → WithTop ℝ) => minPlusMul M M)^[k] G.weightMatrix) i j = G.L (2 ^ k) i j := by induction' k with k ih generalizing i j · -- k=0 have h2 : (2:ℕ)^0 = 1 := by norm_num calc ((fun M => minPlusMul M M)^[0] G.weightMatrix) i j = G.weightMatrix i j := rfl _ = minPlusMul identityMatrix G.weightMatrix i j := by rw [(minPlusMul_identity_left G.weightMatrix i j).symm] _ = G.L 1 i j := by have hL0 : G.L 0 = identityMatrix := by ext i' j'; simp [L_zero, identityMatrix] calc minPlusMul identityMatrix G.weightMatrix i j = minPlusMul (G.L 0) G.weightMatrix i j := by rw [hL0] _ = G.L 1 i j := by simp [L_succ, extendShortestPaths] _ = G.L ((2:ℕ)^0) i j := by rw [h2] · -- k → k+1 calc ((fun (M : V → V → WithTop ℝ) => minPlusMul M M)^[k+1] G.weightMatrix) i j = (minPlusMul (((fun (M : V → V → WithTop ℝ) => minPlusMul M M)^[k] G.weightMatrix)) (((fun (M : V → V → WithTop ℝ) => minPlusMul M M)^[k] G.weightMatrix))) i j := by rw [Function.iterate_succ', Function.comp_apply] _ = minPlusMul (G.L (2 ^ k)) (G.L (2 ^ k)) i j := by have h_fun_eq : ((fun M => minPlusMul M M)^[k] G.weightMatrix) = G.L (2 ^ k) := by ext i' j'; exact ih i' j' rw [h_fun_eq] _ = G.L (2 * (2 ^ k)) i j := (L_sq_eq_minPlusMul (G := G) (2 ^ k) i j).symm _ = G.L (2 ^ (k + 1)) i j := by Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring

2^numSquarings ≥ Fintype.card V - 1 for any Fintype V with at least 1 vertex. This holds because numSquarings is defined as ceil(log2(|V|-1)).

automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_pow_two_ge`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem numSquarings_pow_two_ge (hV : Nonempty V) : 2 ^ numSquarings (V := V) ≥ Fintype.card V - 1 := by have h_card_pos : 1 ≤ Fintype.card V := Fintype.card_pos_iff.mpr hV unfold numSquarings by_cases hx1 : Fintype.card V - 1 ≤ 1 · -- x ≤ 1, so numSquarings = 0, target: 1 ≥ x simp [hx1] · -- x > 1, so numSquarings = Nat.log2 (x - 1) + 1, target: 2^(log2(x-1)+1) ≥ x have hx_gt1 : 1 < Fintype.card V - 1 := by omega simp [hx1] have hnpos : Fintype.card V - 1 - 1 ≠ 0 := by omega set n := Fintype.card V - 1 with hn have h_log2_lt : n - 1 < 2 ^ (Nat.log2 (n - 1) + 1) := (Nat.log2_lt (k := Nat.log2 (n - 1) + 1) (h := hnpos)).mp (Nat.lt_succ_self (Nat.log2 (n - 1))) have h_le : n ≤ 2 ^ (Nat.log2 (n - 1) + 1) := by omega simpa [hn] using h_le

Under NoNegCycle, fasterAPSP equals L^(|V|-1).

theorem fasterAPSP_eq_L (hNC : G.NoNegCycle) (hV : Nonempty V) (i j : V) : G.fasterAPSP i j = G.L (Fintype.card V - 1) i j := by unfold fasterAPSP rw [fasterAPSP_iterate_eq_L (G := G) (numSquarings (V := V)) i j] exact L_stabilizes (G := G) hNC (2 ^ numSquarings (V := V)) (numSquarings_pow_two_ge hV) i j

Under NoNegCycle, fasterAPSP computes the true shortest-path distances for all pairs, i.e. fasterAPSP extends to IsShortestDist for every pair.

theorem fasterAPSP_eq_shortestDist (hNC : G.NoNegCycle) (hV : Nonempty V) (i j : V) : G.IsShortestDist i j (G.fasterAPSP i j) := by have h_eq : G.fasterAPSP i j = G.relaxDist i (Fintype.card V - 1) j := calc G.fasterAPSP i j = G.L (Fintype.card V - 1) i j := fasterAPSP_eq_L (G := G) hNC hV i j _ = G.relaxDist i (Fintype.card V - 1) j := L_eq_relaxDist (G := G) hNC (Fintype.card V - 1) i j rw [h_eq] exact G.relaxDist_isShortestDist hNC i j

Work-count refinement

FASTER-APSP performs numSquarings iterations of min-plus matrix squaring. Each squaring of an n × n matrix computes n² entries, each entry taking the minimum over n intermediate vertices, giving n³ scalar operations per squaring. The total is numSquarings × n³, which is O(n³ log n).

These formulas describe candidate budgets; the function-valued recursive specification does not guarantee cached intermediate tables. The separate MatrixExecution.fasterOn_visits_eq_budget theorem connects this budget to actual stored min-plus scans. Table writes are counted separately.

Candidate-visit budget of one min-plus matrix squaring on the actual |V| × |V| matrix: |V|² entries × |V| intermediate vertices = |V|³.

def minPlusMulCost (Variable name `G` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`G : WeightedGraph V) : ℕ := Fintype.card V * Fintype.card V * Fintype.card V

Candidate-visit budget of FASTER-APSP on graph G: numSquarings iterations of minPlusMulCost G.

def fasterAPSPCost (G : WeightedGraph V) : ℕ := numSquarings (V := V) * G.minPlusMulCost

The number of squarings is at most log₂ |V| + 1.

automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_log2_add_one`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`lemma numSquarings_le_log2_add_one : numSquarings (V := V) ≤ Nat.log2 (Fintype.card V) + 1 := by unfold numSquarings by_cases h : Fintype.card V - 1 ≤ 1 · simp [h] · simp [h] have hle : Nat.log2 (Fintype.card V - 1 - 1) ≤ Nat.log2 (Fintype.card V) := by simp only [Nat.log2_eq_log_two] exact Nat.log_mono_right (by omega : Fintype.card V - 1 - 1 ≤ Fintype.card V) exact hle

Trivial upper bound: numSquarings ≤ |V|.

automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.Chapter24.WeightedGraph.numSquarings_le_n`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`lemma numSquarings_le_n : numSquarings (V := V) ≤ Fintype.card V := by unfold numSquarings by_cases h : Fintype.card V - 1 ≤ 1 · simp [h] · simp [h] have hlog : Nat.log2 (Fintype.card V - 1 - 1) ≤ Fintype.card V - 1 - 1 := Nat.log2_le_self _ omega

Work-count refinement. FASTER-APSP performs O(|V|³ log |V|) scalar operations: numSquarings ≤ log₂|V| + 1 squarings, each costing |V|³.

theorem fasterAPSPCost_le_n_cubed_log (G : WeightedGraph V) : G.fasterAPSPCost ≤ Fintype.card V * Fintype.card V * Fintype.card V * (Nat.log2 (Fintype.card V) + 1) := by unfold fasterAPSPCost minPlusMulCost have hsq := numSquarings_le_log2_add_one (V := V) exact calc numSquarings (V := V) * (Fintype.card V * Fintype.card V * Fintype.card V) ≤ (Nat.log2 (Fintype.card V) + 1) * (Fintype.card V * Fintype.card V * Fintype.card V) := Nat.mul_le_mul_right _ hsq _ = Fintype.card V * Fintype.card V * Fintype.card V * (Nat.log2 (Fintype.card V) + 1) := by ac_rfl

Trivial O(|V|⁴) upper bound. FASTER-APSP performs at most |V|⁴ scalar operations on |V| vertices (via numSquarings ≤ |V|).

theorem fasterAPSPCost_le_n_four (G : WeightedGraph V) : G.fasterAPSPCost ≤ Fintype.card V * Fintype.card V * Fintype.card V * Fintype.card V := by unfold fasterAPSPCost minPlusMulCost have hsq := numSquarings_le_n (V := V) exact calc numSquarings (V := V) * (Fintype.card V * Fintype.card V * Fintype.card V) ≤ Fintype.card V * (Fintype.card V * Fintype.card V * Fintype.card V) := Nat.mul_le_mul hsq (Nat.le_refl _) _ = Fintype.card V * Fintype.card V * Fintype.card V * Fintype.card V := by ac_rfl
end WeightedGraphend Chapter24end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_23.MatrixExecution.Reindex

Finite-carrier interfaces for stored matrix execution

An explicit vertex/index equivalence supplies array indices. Its construction is not included in the scalar-operation counters. The equivalence itself is arbitrary; the refinement theorems relate results to the original graph.

noncomputable sectionnamespace CLRS.Chapter24.MatrixExecutionvariable {V : Type*} [Fintype V] [DecidableEq V]

Encode a mathematical matrix with the caller's vertex enumeration.

def encode (e : V ≃ Fin n) (a : V → V → WithTop ℝ) : Fin n → Fin n → WithTop ℝ := fun i j => a (e.symm i) (e.symm j)
omit [DecidableEq V] in theorem encode_minPlus (e : V ≃ Fin n) (a b : V → V → WithTop ℝ) : WeightedGraph.minPlusMul (encode e a) (encode e b) = encode e (WeightedGraph.minPlusMul a b) := by funext i j apply le_antisymm · apply Finset.le_inf intro v _ exact (Finset.inf_le (f := fun k => encode e a i k + encode e b k j) (Finset.mem_univ (e v))).trans_eq (by simp [encode]) · apply Finset.le_inf intro k _ exact Finset.inf_le (Finset.mem_univ (e.symm k))omit [Fintype V] [DecidableEq V] in theorem encode_floyd (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (ks : List V) : WeightedGraph.floydFrom (encode e a) (ks.map e) = encode e (WeightedGraph.floydFrom a ks) := by induction ks with | nil => rfl | cons k ks ih => funext i j simp [List.map_cons, WeightedGraph.floydFrom, ih, encode]def floydOn (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (ks : List V) : Run := floyd (encode e a) (ks.map e)automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.floydOn_read`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.floydOn_read`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` @[simp] automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.floydOn_read`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem floydOn_read (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (ks : List V) (i j : V) : read (floydOn e a ks).table (e i) (e j) = WeightedGraph.floydFrom a ks i j := by simp [floydOn, floyd_read, encode_floyd, encode]def squareOn (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (q : Nat) : Run := square (encode e a) qomit [DecidableEq V] in theorem encode_square (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (q : Nat) : (fun b => WeightedGraph.minPlusMul b b)^[q] (encode e a) = encode e ((fun b => WeightedGraph.minPlusMul b b)^[q] a) := by induction q with | zero => rfl | succ q ih => simp only [Function.iterate_succ_apply', ih, encode_minPlus]automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.squareOn_read`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.squareOn_read`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` @[simp] automatically included section variable(s) unused in theorem `CLRS.Chapter24.MatrixExecution.squareOn_read`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem squareOn_read (e : V ≃ Fin n) (a : V → V → WithTop ℝ) (q : Nat) (i j : V) : read (squareOn e a q).table (e i) (e j) = ((fun b => WeightedGraph.minPlusMul b b)^[q] a) i j := by simp [squareOn, square_read, encode_square, encode]

Actual stored cycle-safe Floyd result over the original vertex type.

def cycleFloydOn (e : V ≃ Fin n) (G : WeightedGraph V) : Run := floydOn e G.cycleWeightMatrix Finset.univ.toList
@[simp] theorem cycleFloydOn_read (e : V ≃ Fin n) (G : WeightedGraph V) (i j : V) : read (cycleFloydOn e G).table (e i) (e j) = G.cycleFloydWarshall i j := floydOn_read _ _ _ _ _ theorem cycleFloydOn_shortest (e : V ≃ Fin n) (G : WeightedGraph V) (hNC : G.NoNegCycle) (i j : V) : G.IsShortestDist i j (read (cycleFloydOn e G).table (e i) (e j)) := by rw [cycleFloydOn_read, WeightedGraph.cycleFloydWarshall_eq_floydWarshall G hNC] exact G.floydWarshall_isShortestDist hNC i j

Scan the actual stored diagonal, returning the minimum and visit count.

def diagonalScan (n : Nat) (t : Stored) : WithTop ℝ × Nat := scanFin (fun i : Fin n => read t i i)
@[simp] theorem diagonalScan_visits (n : Nat) (t : Stored) : (diagonalScan n t).2 = n := scanFin_visits _

The counted diagonal scan detects exactly the negative-cycle inputs.

theorem diagonalScan_negative_iff (e : V ≃ Fin n) (G : WeightedGraph V) : (diagonalScan n (cycleFloydOn e G).table).1 < 0 ↔ ¬ G.NoNegCycle := by rw [diagonalScan, scanFin_value, Finset.inf_lt_iff] have hex : (∃ i : Fin n, i ∈ Finset.univ ∧ read (cycleFloydOn e G).table i i < 0) ↔ ∃ v, G.cycleFloydWarshall v v < 0 := by constructor · rintro ⟨i, _, hi⟩ refine ⟨e.symm i, ?_⟩ have heq := cycleFloydOn_read e G (e.symm i) (e.symm i) simp only [Equiv.apply_symm_apply] at heq exact heq ▸ hi · rintro ⟨v, hv⟩ exact ⟨e v, Finset.mem_univ _, by simpa using hv⟩ exact hex.trans G.cycleFloydWarshall_negative_iff

Counted Floyd updates, excluding the separately counted final diagonal scan.

@[simp] theorem cycleFloydOn_visits (e : V ≃ Fin n) (G : WeightedGraph V) : (cycleFloydOn e G).visits = n ^ 3 := by have hcard : Fintype.card V = n := by simpa using Fintype.card_congr e simp [cycleFloydOn, floydOn, hcard, pow_succ, Nat.mul_assoc]

Stored repeated squaring over the original graph carrier.

def fasterOn (e : V ≃ Fin n) (G : WeightedGraph V) : Run := squareOn e G.weightMatrix (WeightedGraph.numSquarings (V := V))
@[simp] theorem fasterOn_read (e : V ≃ Fin n) (G : WeightedGraph V) (i j : V) : read (fasterOn e G).table (e i) (e j) = G.fasterAPSP i j := squareOn_read _ _ _ _ _ theorem fasterOn_shortest (e : V ≃ Fin n) (G : WeightedGraph V) (hNC : G.NoNegCycle) (i j : V) : G.IsShortestDist i j (read (fasterOn e G).table (e i) (e j)) := by rw [fasterOn_read] exact G.fasterAPSP_eq_shortestDist hNC ⟨i⟩ i j@[simp] theorem fasterOn_visits (e : V ≃ Fin n) (G : WeightedGraph V) : (fasterOn e G).visits = WeightedGraph.numSquarings (V := V) * n ^ 3 := square_visits _ _

The old Floyd budget is exactly the updates of this stored execution.

theorem cycleFloydOn_visits_eq_budget (e : V ≃ Fin n) (G : WeightedGraph V) : (cycleFloydOn e G).visits = G.floydWarshallCost := by have hc : Fintype.card V = n := by simpa using Fintype.card_congr e rw [cycleFloydOn_visits, G.floydWarshall_O_cubed, hc] ring

The old squaring budget is exactly the executed min-plus candidate visits.

theorem fasterOn_visits_eq_budget (e : V ≃ Fin n) (G : WeightedGraph V) : (fasterOn e G).visits = G.fasterAPSPCost := by have hc : Fintype.card V = n := by simpa using Fintype.card_congr e rw [fasterOn_visits] simp [WeightedGraph.fasterAPSPCost, WeightedGraph.minPlusMulCost, hc, pow_succ, Nat.mul_assoc]
end CLRS.Chapter24.MatrixExecution

CLRSLean.FourthEdition.Chapter_23.MatrixExecution.Basic

Stored matrices and counted min-plus products

Every row and cell is appended once. Inner scans return both their minimum and their actual number of visits. Exact real arithmetic, comparison, and array access are abstract primitives; allocation and bit costs are excluded.

noncomputable sectionnamespace CLRS.Chapter24.MatrixExecutionopen CLRS.Chapter15.DPExecutionabbrev Stored := Table (WithTop ℝ)def read (t : Stored) (i j : Fin n) : WithTop ℝ := get t.rows i.val j.valdef cell (f : Fin n → Fin n → WithTop ℝ × Nat) (i j : Nat) : WithTop ℝ × Nat := if hi : i < n then if hj : j < n then f ⟨i, hi⟩ ⟨j, hj⟩ else (⊤, 0) else (⊤, 0)def tabulate (f : Fin n → Fin n → WithTop ℝ × Nat) : Stored := buildLayers (fun _ => n) (fun i _ j => cell f i j) n @[simp] theorem tabulate_read (f : Fin n → Fin n → WithTop ℝ × Nat) (i j : Fin n) : read (tabulate f) i j = (f i j).1 := by have h := buildLayers_correct (fun _ => n) (fun i _ j => cell f i j) (fun i j => (cell f i j).1) (by intros; rfl) n i.val i.isLt j.val j.isLt simpa [read, tabulate, cell, i.isLt, j.isLt] using h@[simp] theorem tabulate_writes (f : Fin n → Fin n → WithTop ℝ × Nat) : (tabulate f).cellWrites = n * n := by simp [tabulate, buildLayers_cellWrites] theorem tabulate_visits (f : Fin n → Fin n → WithTop ℝ × Nat) (c : Nat) (hc : ∀ i j, (f i j).2 = c) : (tabulate f).candidateVisits = n * n * c := by have rowVisits (i : Nat) (hi : i < n) : ∑ j ∈ Finset.range n, (cell f i j).2 = n * c := by calc _ = ∑ _j ∈ Finset.range n, c := Finset.sum_congr rfl (fun j hj => by simp [cell, hi, Finset.mem_range.mp hj, hc]) _ = n * c := by simp have layers : ∀ k, k ≤ n → (buildLayers (fun _ => n) (fun i _ j => cell f i j) k).candidateVisits = k * (n * c) := by intro k hk induction k with | zero => simp [buildLayers] | succ k ih => simp only [buildLayers] rw [ih (by omega), buildRow_visits, rowVisits k (by omega)] ring simpa [tabulate, Nat.mul_assoc] using layers n (by omega)def scanMin (f : Nat → WithTop ℝ) : Nat → WithTop ℝ × Nat | 0 => (⊤, 0) | k + 1 => let prev := scanMin f k; (min prev.1 (f k), prev.2 + 1)@[simp] theorem scanMin_visits (f : Nat → WithTop ℝ) (k : Nat) : (scanMin f k).2 = k := by induction k with | zero => rfl | succ k ih => simp [scanMin, ih]theorem scanMin_value (f : Nat → WithTop ℝ) (k : Nat) : (scanMin f k).1 = (Finset.range k).inf f := by induction k with | zero => simp [scanMin] | succ k ih => simp [scanMin, ih, Finset.range_add_one, min_comm]def scanFin (f : Fin n → WithTop ℝ) : WithTop ℝ × Nat := scanMin (fun k => if hk : k < n then f ⟨k, hk⟩ else ⊤) n@[simp] theorem scanFin_visits (f : Fin n → WithTop ℝ) : (scanFin f).2 = n := scanMin_visits _ _ theorem scanFin_value (f : Fin n → WithTop ℝ) : (scanFin f).1 = Finset.univ.inf f := by rw [scanFin, scanMin_value] apply le_antisymm · apply Finset.le_inf intro i _ exact (Finset.inf_le (Finset.mem_range.mpr i.isLt)).trans_eq (by simp [i.isLt]) · apply Finset.le_inf intro k hk have hkn := Finset.mem_range.mp hk simpa [hkn] using (Finset.inf_le (s := Finset.univ) (f := f) (Finset.mem_univ (⟨k, hkn⟩ : Fin n)))def multiply (n : Nat) (a b : Stored) : Stored := tabulate (fun i j : Fin n => scanFin (fun k => read a i k + read b k j))@[simp] theorem multiply_read (a b : Stored) (i j : Fin n) : read (multiply n a b) i j = WeightedGraph.minPlusMul (read a) (read b) i j := by simp [multiply, scanFin_value, WeightedGraph.minPlusMul]@[simp] theorem multiply_writes (n : Nat) (a b : Stored) : (multiply n a b).cellWrites = n * n := tabulate_writes _ @[simp] theorem multiply_visits (n : Nat) (a b : Stored) : (multiply n a b).candidateVisits = n ^ 3 := by rw [multiply, tabulate_visits _ n (by intros; exact scanFin_visits _)] ringend CLRS.Chapter24.MatrixExecution

CLRSLean.FourthEdition.Chapter_23.MatrixExecution.Algorithms

Counted stored Floyd–Warshall and repeated squaring

Each recursive call is bound once. A Floyd phase reads the completed previous matrix and writes the next matrix; a squaring phase calls the counted min-plus product. Cumulative counters include initialization. No recursive specification is invoked by a cell evaluator.

noncomputable sectionnamespace CLRS.Chapter24.MatrixExecutionstructure Run where table : Stored writes : Nat visits : Natdef initialRun (f : Fin n → Fin n → WithTop ℝ) : Run := let t := tabulate (fun i j => (f i j, 0)) ⟨t, t.cellWrites, t.candidateVisits⟩@[simp] theorem initialRun_read (f : Fin n → Fin n → WithTop ℝ) (i j : Fin n) : read (initialRun f).table i j = f i j := tabulate_read _ _ _@[simp] theorem initialRun_writes (f : Fin n → Fin n → WithTop ℝ) : (initialRun f).writes = n * n := tabulate_writes _ @[simp] theorem initialRun_visits (f : Fin n → Fin n → WithTop ℝ) : (initialRun f).visits = 0 := by change (tabulate (fun i j => (f i j, 0))).candidateVisits = 0 rw [tabulate_visits _ 0 (by intros; rfl)] simpdef floyd (initial : Fin n → Fin n → WithTop ℝ) : List (Fin n) → Run | [] => initialRun initial | k :: ks => let prev := floyd initial ks let next := tabulate (fun i j => (min (read prev.table i j) (read prev.table i k + read prev.table k j), 1)) ⟨next, prev.writes + next.cellWrites, prev.visits + next.candidateVisits⟩theorem floyd_read (initial : Fin n → Fin n → WithTop ℝ) (ks : List (Fin n)) (i j : Fin n) : read (floyd initial ks).table i j = WeightedGraph.floydFrom initial ks i j := by induction ks generalizing i j with | nil => exact initialRun_read _ _ _ | cons k ks ih => simp only [floyd, tabulate_read, WeightedGraph.floydFrom, ih]@[simp] theorem floyd_writes (initial : Fin n → Fin n → WithTop ℝ) (ks : List (Fin n)) : (floyd initial ks).writes = (ks.length + 1) * (n * n) := by induction ks with | nil => simp [floyd] | cons k ks ih => simp [floyd, ih, Nat.add_mul] @[simp] theorem floyd_visits (initial : Fin n → Fin n → WithTop ℝ) (ks : List (Fin n)) : (floyd initial ks).visits = ks.length * (n * n) := by induction ks with | nil => simp [floyd] | cons k ks ih => simp only [floyd, List.length_cons] rw [ih, tabulate_visits _ 1 (by intros; rfl)] ringdef square (initial : Fin n → Fin n → WithTop ℝ) : Nat → Run | 0 => initialRun initial | q + 1 => let prev := square initial q let next := multiply n prev.table prev.table ⟨next, prev.writes + next.cellWrites, prev.visits + next.candidateVisits⟩theorem square_read (initial : Fin n → Fin n → WithTop ℝ) (q : Nat) : (read (square initial q).table : Fin n → Fin n → WithTop ℝ) = (fun a => WeightedGraph.minPlusMul a a)^[q] initial := by induction q with | zero => funext i j; exact initialRun_read _ _ _ | succ q ih => funext i j simp only [square, multiply_read, Function.iterate_succ_apply', ih]@[simp] theorem square_writes (initial : Fin n → Fin n → WithTop ℝ) (q : Nat) : (square initial q).writes = (q + 1) * (n * n) := by induction q with | zero => simp [square] | succ q ih => simp [square, ih, Nat.add_mul]@[simp] theorem square_visits (initial : Fin n → Fin n → WithTop ℝ) (q : Nat) : (square initial q).visits = q * n ^ 3 := by induction q with | zero => simp [square] | succ q ih => simp [square, ih, Nat.add_mul]

Cycle-safe stored Floyd execution, including negative self-edges.

def cycleFloyd (G : WeightedGraph (Fin n)) : Run := floyd G.cycleWeightMatrix Finset.univ.toList
@[simp] theorem cycleFloyd_read (G : WeightedGraph (Fin n)) (i j : Fin n) : read (cycleFloyd G).table i j = G.cycleFloydWarshall i j := floyd_read _ _ _ _

Exactly the counted Floyd cell update on every vertex pair and pivot.

@[simp] theorem cycleFloyd_visits (G : WeightedGraph (Fin n)) : (cycleFloyd G).visits = n ^ 3 := by simp [cycleFloyd, pow_succ, Nat.mul_assoc]

Correctness of the actual stored output under the valid-input premise.

theorem cycleFloyd_shortest (G : WeightedGraph (Fin n)) (hNC : G.NoNegCycle) (i j : Fin n) : G.IsShortestDist i j (read (cycleFloyd G).table i j) := by rw [cycleFloyd_read, WeightedGraph.cycleFloydWarshall_eq_floydWarshall G hNC] exact G.floydWarshall_isShortestDist hNC i j

The stored result detects a negative cycle in either direction.

theorem cycleFloyd_negative_iff (G : WeightedGraph (Fin n)) : (∃ i : Fin n, read (cycleFloyd G).table i i < 0) ↔ ¬ G.NoNegCycle := by simp only [cycleFloyd_read] exact G.cycleFloydWarshall_negative_iff

Counted repeated squaring of the graph matrix.

def faster (G : WeightedGraph (Fin n)) : Run := square G.weightMatrix (WeightedGraph.numSquarings (V := Fin n))
@[simp] theorem faster_read (G : WeightedGraph (Fin n)) (i j : Fin n) : read (faster G).table i j = G.fasterAPSP i j := by change read (square G.weightMatrix (WeightedGraph.numSquarings (V := Fin n))).table i j = _ rw [square_read] rflend CLRS.Chapter24.MatrixExecution