diff --git a/CLRSLean/Chapter_25.lean b/CLRSLean/Chapter_25.lean
index ea35fee..d1ee47f 100644
--- a/CLRSLean/Chapter_25.lean
+++ b/CLRSLean/Chapter_25.lean
@@ -57,23 +57,19 @@ squaring (via {lit}`Function.iterate`) and proves:
 Section 25.2 defines the Floyd-Warshall DP recurrence `D` and the
 `floydWarshall` algorithm, and proves its correctness (Lemma 25.7,
 Theorem 25.8, CLRS Theorem 25.3).  The predecessor matrix `Pi`,
-path reconstruction `fwReconstructPath` (walk validity), and the
-negative-cycle detection diagonal test are complete.  Walk-reconstruction
-weight equality is deferred.
+path reconstruction `fwReconstructPath` (walk validity and **weight
+equality**), and the negative-cycle detection diagonal test are all
+complete.
 
-Section 25.3 defines Johnson's augmented graph and reweighted graph, proves the
-telescoping identity for every walk, and proves edge-weight nonnegativity from
-the potential triangle inequality.  It does not yet construct the Bellman-Ford
-potential, prove shortest-path preservation, or package the repeated Dijkstra
-runs into an end-to-end Johnson correctness theorem.
+Section 25.3 defines Johnson's augmented graph and reweighted graph,
+constructs the Bellman-Ford potential `h(v) = δ(none, some v)`, proves
+the triangle inequality `h(v) ≤ h(u) + w(u, v)`, proves reweighted
+edge-weight nonnegativity, and packages the end-to-end Johnson
+correctness theorem `johnsonDist_isShortestDist` (CLRS Theorem 25.5).
 
 ## Deferred Work
 
-* Predecessor-matrix path-reconstruction weight equality
-  (`walkWeight = floydWarshall`; walk validity from `Pi_adj` is proved).
 * Transitive closure (Section 25.2 variant).
-* Johnson's Bellman-Ford potential construction, shortest-path preservation,
-  and end-to-end correctness/work theorem.
 * An explicit {lit}`O(n³ log n)` work-count refinement for repeated squaring;
   Section 25.1 already proves its mathematical correctness.
 -/
diff --git a/CLRSLean/Chapter_25/Section_25_3_Johnsons_Algorithm.lean b/CLRSLean/Chapter_25/Section_25_3_Johnsons_Algorithm.lean
index 8157e66..88c9f52 100644
--- a/CLRSLean/Chapter_25/Section_25_3_Johnsons_Algorithm.lean
+++ b/CLRSLean/Chapter_25/Section_25_3_Johnsons_Algorithm.lean
@@ -24,11 +24,19 @@ Main results:
 - Theorem `reweightedWeight_nonneg`: reweighted edge weights are nonnegative.
 - Theorem `reweightedWalkWeight_eq`: `w^(p) = w(p) + h(u) - h(v)` for any
   walk `p` from `u` to `v` (telescoping property).
-
-**Current gaps:** The `noNegCycle_johnsonAugmentedGraph` proof and the
-shortest-path preservation theorem are deferred to a follow-up commit.
-The reweighted weight function, telescoping property, and nonnegativity
-lemma below are complete.
+- Theorem `reweighted_isShortestDist`: reweighted shortest distances equal
+  original distances shifted by `h(u) - h(v)`.
+- Lemma `noNegCycle_johnsonAugmentedGraph`: the augmented graph has no
+  negative cycles iff the original graph has none.
+- Lemma `johnsonPotential_triangle`: the Bellman-Ford potential satisfies
+  `h(v) ≤ h(u) + w(u, v)` for every edge `(u, v)`.
+- Theorem `johnsonDist_isShortestDist`: **CLRS Theorem 25.5** —
+  end-to-end correctness of Johnson's algorithm: `johnsonDist` computes
+  the exact all-pairs shortest-path distances.
+
+The section is **complete**: the augmented-graph potential construction,
+triangle inequality, reweighting nonnegativity, and end-to-end Johnson
+correctness are all proved.
 -/
 
 namespace CLRS
@@ -270,6 +278,394 @@ theorem reweighted_isShortestDist (h : V → ℝ) (u v : V) (d : WithTop ℝ) :
               (walkWeight G.w p : WithTop ℝ) + (h u : WithTop ℝ) - (h v : WithTop ℝ) := h_rw'
           _ = d + (h u : WithTop ℝ) - (h v : WithTop ℝ) := by rw [hpw]
 
+
+/-! ## Negative-cycle equivalence for the augmented graph -/
+
+/-- No edge in `johnsonAugmentedGraph` targets `none`. -/
+lemma adj_target_ne_none (u v : Option V)
+    (h_adj : G.johnsonAugmentedGraph.Adj u v) : v ≠ none := by
+  intro h_eq; subst h_eq
+  have h_edge : (u, none) ∈ G.johnsonAugmentedGraph.edges := h_adj
+  exact G.no_incoming_to_none_johnsonAugmentedGraph u h_edge
+
+/-- If a chain in `johnsonAugmentedGraph` does **not** start at `none`, then
+`none` never appears in the chain. -/
+lemma chain_no_none (l : List (Option V))
+    (h_chain : List.IsChain G.johnsonAugmentedGraph.Adj l)
+    (h_head_ne_none : l.head? ≠ some none) : none ∉ l := by
+  induction l with
+  | nil => simp
+  | cons x l' ih =>
+    rw [List.isChain_cons] at h_chain
+    rcases h_chain with ⟨h_adj, h_chain_tail⟩
+    have hx_ne_none : x ≠ none := by
+      intro h_eq; subst h_eq; apply h_head_ne_none; simp
+    have h_l'_head_ne_none : l'.head? ≠ some none := by
+      intro h_eq
+      have h_mem : none ∈ l'.head? := by rw [h_eq]; simp
+      have h_adj_x_none : G.johnsonAugmentedGraph.Adj x none := h_adj none h_mem
+      exact adj_target_ne_none G x none h_adj_x_none rfl
+    have h_none_notin_l' : none ∉ l' := ih h_chain_tail h_l'_head_ne_none
+    intro h
+    cases h with
+    | head _ => exact hx_ne_none rfl
+    | tail _ h_mem => exact h_none_notin_l' h_mem
+
+/-- The only walk from `none` to `none` in the augmented graph is `[none]`. -/
+lemma walk_from_none_to_none_singleton (c : List (Option V))
+    (hc : G.johnsonAugmentedGraph.IsWalkFrom none none c) : c = [none] := by
+  have h_last : c.getLast? = some none := hc.last
+  rcases List.getLast?_eq_some_iff.mp h_last with ⟨c₁, hc_eq⟩
+  subst hc_eq
+  by_cases h_c₁_empty : c₁ = []
+  · subst h_c₁_empty; simp
+  · have h_chain : List.IsChain G.johnsonAugmentedGraph.Adj (c₁ ++ [none]) := hc.chain
+    rw [List.isChain_append] at h_chain
+    rcases h_chain with ⟨_, _, h_adj_cond⟩
+    have h_c₁_last_some : c₁.getLast? ≠ none := by
+      intro h_eq; apply h_c₁_empty
+      exact (List.getLast?_eq_none_iff.mp h_eq)
+    rcases Option.ne_none_iff_exists'.mp h_c₁_last_some with ⟨last_c₁, h_last_c₁⟩
+    have h_adj_last_none : G.johnsonAugmentedGraph.Adj last_c₁ none :=
+      h_adj_cond last_c₁ (by rw [h_last_c₁]; simp) none (by simp)
+    exfalso
+    exact (adj_target_ne_none G last_c₁ none h_adj_last_none) rfl
+
+/-- Extend a walk by a single edge `u → v` at the end. -/
+lemma IsWalkFrom.append_step (hp : G.IsWalkFrom s u p) (h_edge : G.Adj u v) :
+    G.IsWalkFrom s v (p ++ [v]) := by
+  have h_chain : List.IsChain G.Adj (p ++ [v]) :=
+    List.IsChain.append hp.chain (List.isChain_singleton v)
+      (by
+        intro x hx_last
+        -- hx_last : p.getLast? = some x (by definition of ∈ for Option)
+        rw [hp.last] at hx_last
+        -- hx_last : some u = some x
+        have hx_eq : x = u := (Option.some_inj.mp hx_last).symm
+        subst hx_eq
+        intro y hy_head
+        -- hy_head : [v].head? = some y (by definition of ∈ for Option)
+        -- [v].head? = some v (by simp)
+        have hy_eq : y = v := by
+          -- hy_head: [v].head? = some y, and [v].head? = some v
+          -- So some y = some v, hence y = v
+          have hh : [v].head? = some y := hy_head
+          have hv : [v].head? = some v := by simp
+          rw [hv] at hh
+          -- hh: some v = some y
+          exact (Option.some_inj.mp hh).symm
+        subst hy_eq
+        exact h_edge)
+  have h_head : (p ++ [v]).head? = some s := by
+    have hp_ne_nil : p ≠ [] := hp.ne_nil
+    have hp_head_val : p.head? = some s := hp.head
+    cases p with
+    | nil => exact absurd rfl hp_ne_nil
+    | cons a as =>
+      -- p = a :: as, so (a :: as ++ [v]).head? = some a
+      -- and hp.head gives some a = some s
+      have h_head_a : (a :: as).head? = some a := by simp
+      rw [h_head_a] at hp_head_val
+      -- hp_head_val : some a = some s
+      simp [hp_head_val]
+  have h_last : (p ++ [v]).getLast? = some v := by simp
+  exact ⟨h_chain, h_head, h_last⟩
+
+/-- The weight of a walk extended by a single edge. -/
+lemma walkWeight_append_step (hp : G.IsWalkFrom s u p) (h_edge : G.Adj u v) :
+    (walkWeight G.w (p ++ [v]) : WithTop ℝ) =
+      (walkWeight G.w p : WithTop ℝ) + (G.w u v : WithTop ℝ) := by
+  rcases List.getLast?_eq_some_iff.mp hp.last with ⟨q, hq⟩
+  subst hq
+  simp [walkWeight_concat G.w q u v]
+
+/-- An auxiliary function that strips `Option.some` from an element. -/
+private def unsome (default : V) (x : Option V) : V :=
+  match x with | some v => v | none => default
+
+/-- For a `none`-free list, the chain in `G'` lifts to a chain in `G`. -/
+private lemma chain_none_free_map (default : V) (l : List (Option V))
+    (h_chain : List.IsChain G.johnsonAugmentedGraph.Adj l)
+    (h_no_none : none ∉ l) :
+    List.IsChain G.Adj (l.map (unsome default)) := by
+  induction l with
+  | nil => exact List.IsChain.nil
+  | cons x l' ih =>
+    rw [List.isChain_cons] at h_chain
+    rcases h_chain with ⟨h_adj, h_chain_tail⟩
+    have hx_ne_none : x ≠ none := by
+      intro h_eq; subst h_eq; exact h_no_none (by simp)
+    have hl'_no_none : none ∉ l' := by
+      intro h; exact h_no_none (by simp [h])
+    -- Determine x (must be some a since ≠ none)
+    obtain ⟨a, hx_eq⟩ := Option.ne_none_iff_exists'.mp hx_ne_none
+    subst hx_eq
+    -- Now x = some a
+    have ih_map : List.IsChain G.Adj (l'.map (unsome default)) :=
+      ih h_chain_tail hl'_no_none
+    rw [show (some a :: l').map (unsome default) = a :: l'.map (unsome default) by
+      simp [unsome]]
+    apply List.IsChain.cons ih_map
+    intro y hy
+    -- hy : y ∈ (l'.map (unsome default)).head?
+    -- We need G.Adj a y. Analyze l'.
+    cases l' with
+    | nil => simp at hy
+    | cons z l'' =>
+      -- z must be some b (since none ∉ l')
+      have hz_ne_none : z ≠ none := by
+        intro h_eq; subst h_eq; exact hl'_no_none (by simp)
+      obtain ⟨b, hz_eq⟩ := Option.ne_none_iff_exists'.mp hz_ne_none
+      subst hz_eq
+      -- Now l' = some b :: l''
+      -- The head of (some b :: l'').map (unsome default) is b
+      have h_head_map : ((some b :: l'').map (unsome default)).head? = some b := by
+        simp [unsome]
+      rw [h_head_map] at hy
+      -- Now hy : y ∈ some b, i.e. some b = some y, so b = y
+      have hy_eq : b = y := Option.some_inj.mp hy
+      subst hy_eq
+      -- Need G.Adj a b. From h_adj: G'.Adj (some a) (some b)
+      have h_adj' : G.johnsonAugmentedGraph.Adj (some a) (some b) :=
+        h_adj (some b) (by simp)
+      exact (G.mem_edges_johnsonAugmentedGraph_edge a b).mp h_adj'
+
+/-- For a `none`-free list, the walk weights in `G'` and `G` agree. -/
+private lemma walkWeight_none_free_eq (default : V) (c : List (Option V))
+    (h_no_none : none ∉ c) :
+    walkWeight G.johnsonAugmentedGraph.w c =
+      walkWeight G.w (c.map (unsome default)) := by
+  induction c with
+  | nil => simp [walkWeight]
+  | cons x cs ih =>
+    cases x with
+    | none => exfalso; exact h_no_none (by simp)
+    | some a =>
+      cases cs with
+      | nil =>
+        -- c = [some a]; both sides are 0
+        simp [walkWeight]
+      | cons y rest =>
+        have h_cs_no_none : none ∉ (y :: rest) := by
+          intro h; apply h_no_none; simp [h]
+        cases y with
+        | none => exfalso; exact h_cs_no_none (by simp)
+        | some b =>
+          -- c = some a :: some b :: rest
+          -- walkWeight G'.w c = G.w a b + walkWeight G'.w (some b :: rest)
+          -- walkWeight G.w (c.map f) = G.w a b + walkWeight G.w (b :: rest.map f)
+          have h_ih := ih h_cs_no_none
+          -- h_ih: walkWeight G'.w (some b :: rest) = walkWeight G.w ((some b :: rest).map (unsome default))
+          -- Compute RHS map:
+          have h_map_rest : ((some b :: rest).map (unsome default)) = b :: (rest.map (unsome default)) := by
+            simp [unsome]
+          rw [h_map_rest] at h_ih
+          -- Now h_ih: walkWeight G'.w (some b :: rest) = walkWeight G.w (b :: rest.map (unsome default))
+          -- Expand both sides using walkWeight formula
+          calc
+            walkWeight G.johnsonAugmentedGraph.w (some a :: some b :: rest)
+                = G.johnsonAugmentedGraph.w (some a) (some b) +
+                  walkWeight G.johnsonAugmentedGraph.w (some b :: rest) := by simp [walkWeight]
+            _ = G.w a b + walkWeight G.johnsonAugmentedGraph.w (some b :: rest) := by
+              simp [johnsonAugmentedGraph]
+            _ = G.w a b + walkWeight G.w (b :: rest.map (unsome default)) := by rw [h_ih]
+            _ = walkWeight G.w (a :: b :: rest.map (unsome default)) := by simp [walkWeight]
+            _ = walkWeight G.w ((some a :: some b :: rest).map (unsome default)) := by
+              unfold unsome; simp
+
+/-- Project a `none`-free walk in `G'` to a walk in `G` with the same weight. -/
+private lemma exists_walk_in_G_of_none_free_walk (x' : V) (c : List (Option V))
+    (hc : G.johnsonAugmentedGraph.IsWalkFrom (some x') (some x') c)
+    (h_no_none : none ∉ c) :
+    ∃ (c' : List V),
+      G.IsWalkFrom x' x' c' ∧
+      walkWeight G.johnsonAugmentedGraph.w c = walkWeight G.w c' := by
+  let c' := c.map (unsome x')
+  have h_chain_c' : List.IsChain G.Adj c' :=
+    chain_none_free_map G x' c hc.chain h_no_none
+  have h_head_c' : c'.head? = some x' := by
+    have h_head_c : c.head? = some (some x') := hc.head
+    rcases List.head?_eq_some_iff.mp h_head_c with ⟨cs, hc_eq⟩
+    subst hc_eq
+    simp [c', unsome]
+  have h_last_c' : c'.getLast? = some x' := by
+    rcases List.getLast?_eq_some_iff.mp hc.last with ⟨q, hq⟩
+    subst hq
+    simp [c', unsome]
+  have h_walk_c' : G.IsWalkFrom x' x' c' :=
+    ⟨h_chain_c', h_head_c', h_last_c'⟩
+  have h_wt_eq : walkWeight G.johnsonAugmentedGraph.w c = walkWeight G.w c' :=
+    walkWeight_none_free_eq G x' c h_no_none
+  exact ⟨c', h_walk_c', h_wt_eq⟩
+
+/-- If `G` has no negative cycles, then `johnsonAugmentedGraph` also has none. -/
+lemma noNegCycle_johnsonAugmentedGraph (hNC : G.NoNegCycle) :
+    G.johnsonAugmentedGraph.NoNegCycle := by
+  intro x c hc
+  cases x with
+  | none =>
+    have h_single : c = [none] := walk_from_none_to_none_singleton G c hc
+    subst h_single; simp [walkWeight]
+  | some x' =>
+    have h_head_ne_none : c.head? ≠ some none := by
+      rw [hc.head]; simp
+    have h_no_none : none ∉ c := chain_no_none G c hc.chain h_head_ne_none
+    rcases exists_walk_in_G_of_none_free_walk G x' c hc h_no_none with ⟨c', hc'_walk, hw_eq⟩
+    rw [hw_eq]
+    exact hNC x' c' hc'_walk
+
+/-! ## Johnson potential via Bellman-Ford on the augmented graph -/
+
+/-- A direct walk from `none` to `some v` in the augmented graph. -/
+lemma isWalkFrom_none_some (v : V) :
+    G.johnsonAugmentedGraph.IsWalkFrom none (some v) [none, some v] := by
+  let G' := G.johnsonAugmentedGraph
+  have h_chain : List.IsChain G'.Adj [none, some v] := by
+    rw [List.isChain_cons]
+    refine ⟨?_, List.isChain_singleton _⟩
+    intro y hy
+    have hy_eq : y = some v := by
+      have h_head_val : [some v].head? = some (some v) := by simp
+      rw [h_head_val] at hy
+      exact (Option.some_inj.mp hy).symm
+    subst hy_eq
+    unfold G' johnsonAugmentedGraph WeightedGraph.Adj
+    simp
+  refine ⟨h_chain, ?_, ?_⟩
+  · simp
+  · simp
+
+/-- The Bellman-Ford distance from `none` to `some v` in the augmented graph
+is finite (not `⊤`), because there is a direct zero-weight edge. -/
+lemma relaxDist_none_some_ne_top (hNC : G.NoNegCycle) (v : V) :
+    G.johnsonAugmentedGraph.relaxDist none
+      (Fintype.card (Option V) - 1) (some v) ≠ ⊤ := by
+  let G' := G.johnsonAugmentedGraph
+  have h_no_neg : G'.NoNegCycle := noNegCycle_johnsonAugmentedGraph G hNC
+  have h_sd := G'.relaxDist_isShortestDist h_no_neg none (some v)
+  rcases h_sd with ⟨h_lower, _⟩
+  have h_walk : G'.IsWalkFrom none (some v) [none, some v] :=
+    isWalkFrom_none_some G v
+  have h_bound : G'.relaxDist none (Fintype.card (Option V) - 1) (some v) ≤
+      (walkWeight G'.w [none, some v] : WithTop ℝ) :=
+    h_lower [none, some v] h_walk
+  have h_wt : (walkWeight G'.w [none, some v] : WithTop ℝ) = (0 : WithTop ℝ) := by
+    simp [walkWeight, G', johnsonAugmentedGraph]
+  rw [h_wt] at h_bound
+  intro h_eq; rw [h_eq] at h_bound; simpa using h_bound
+
+/-- The **Johnson potential** `h(v)` is the shortest-path distance from
+`none` to `some v` in the augmented graph, computed by Bellman-Ford. -/
+noncomputable def johnsonPotential (hNC : G.NoNegCycle) (v : V) : ℝ :=
+  (G.johnsonAugmentedGraph.relaxDist none
+    (Fintype.card (Option V) - 1) (some v)).untop
+    (relaxDist_none_some_ne_top G hNC v)
+
+/-- The potential cast to `WithTop ℝ` equals the Bellman-Ford relaxation. -/
+lemma johnsonPotential_eq (hNC : G.NoNegCycle) (v : V) :
+    (G.johnsonPotential hNC v : WithTop ℝ) =
+    G.johnsonAugmentedGraph.relaxDist none
+      (Fintype.card (Option V) - 1) (some v) := by
+  unfold johnsonPotential
+  simp [relaxDist_none_some_ne_top G hNC v]
+
+/-- The Johnson potential is the shortest-path distance from `none` to `some v`
+in the augmented graph. -/
+lemma johnsonPotential_isShortestDist (hNC : G.NoNegCycle) (v : V) :
+    G.johnsonAugmentedGraph.IsShortestDist none (some v)
+      (G.johnsonPotential hNC v) := by
+  rw [johnsonPotential_eq G hNC]
+  have h_no_neg : G.johnsonAugmentedGraph.NoNegCycle :=
+    noNegCycle_johnsonAugmentedGraph G hNC
+  exact G.johnsonAugmentedGraph.relaxDist_isShortestDist h_no_neg none (some v)
+
+/-! ## Triangle inequality for the Johnson potential -/
+
+/-- **Triangle inequality for the Johnson potential.**  For every edge
+`(u, v)` in `G`, we have `h(v) ≤ h(u) + w(u, v)`. -/
+lemma johnsonPotential_triangle (hNC : G.NoNegCycle) (u v : V)
+    (h_edge : (u, v) ∈ G.edges) :
+    G.johnsonPotential hNC v ≤ G.johnsonPotential hNC u + G.w u v := by
+  let G' := G.johnsonAugmentedGraph
+  let hu := G.johnsonPotential hNC u
+  let hv := G.johnsonPotential hNC v
+  have h_sd_u : G'.IsShortestDist none (some u) (hu : WithTop ℝ) :=
+    johnsonPotential_isShortestDist G hNC u
+  have h_sd_v : G'.IsShortestDist none (some v) (hv : WithTop ℝ) :=
+    johnsonPotential_isShortestDist G hNC v
+  rcases h_sd_u.2 with (h_top | ⟨p_u, hp_walk, hp_weight⟩)
+  · have h_fin : (hu : WithTop ℝ) ≠ ⊤ := by simp
+    exact absurd h_top h_fin
+  · have h_edge' : G'.Adj (some u) (some v) := by
+      unfold G' johnsonAugmentedGraph WeightedGraph.Adj; simp [h_edge]
+    have h_walk_v : G'.IsWalkFrom none (some v) (p_u ++ [some v]) :=
+      IsWalkFrom.append_step (G := G') hp_walk h_edge'
+    have h_weight_v : (walkWeight G'.w (p_u ++ [some v]) : WithTop ℝ) =
+        (hu : WithTop ℝ) + (G.w u v : WithTop ℝ) := by
+      rw [walkWeight_append_step G' hp_walk h_edge']
+      rw [hp_weight]
+      have h_w_uv : (G'.w (some u) (some v) : WithTop ℝ) = (G.w u v : WithTop ℝ) := by
+        unfold G' johnsonAugmentedGraph; simp
+      rw [h_w_uv]
+    have h_ineq : (hv : WithTop ℝ) ≤ (walkWeight G'.w (p_u ++ [some v]) : WithTop ℝ) :=
+      h_sd_v.1 (p_u ++ [some v]) h_walk_v
+    rw [h_weight_v] at h_ineq
+    exact_mod_cast h_ineq
+
+/-! ## Nonnegativity of the reweighted graph -/
+
+/-- With the Johnson potential, every edge weight in the reweighted graph
+is nonnegative, satisfying Dijkstra's precondition. -/
+lemma reweightedGraph_nonneg (hNC : G.NoNegCycle) :
+    (G.reweightedGraph (G.johnsonPotential hNC)).Nonneg := by
+  rw [WeightedGraph.Nonneg]
+  intro u v h_edge
+  rw [w_reweightedGraph, reweightedWeight_eq]
+  have h_triangle := johnsonPotential_triangle G hNC u v h_edge
+  linarith
+
+/-- With the Johnson potential, the reweighted graph has no negative cycles. -/
+lemma reweightedGraph_noNegCycle (hNC : G.NoNegCycle) :
+    (G.reweightedGraph (G.johnsonPotential hNC)).NoNegCycle :=
+  noNegCycle_of_nonneg (G := G.reweightedGraph (G.johnsonPotential hNC)) (G.reweightedGraph_nonneg hNC)
+
+/-! ## Johnson's all-pairs shortest paths -/
+
+/-- A `WithTop ℝ` algebra identity for finite adjustments. -/
+private lemma add_sub_add_sub_eq (a : WithTop ℝ) (b c : ℝ) :
+    a = (a + (c : WithTop ℝ) - (b : WithTop ℝ)) + (b : WithTop ℝ) - (c : WithTop ℝ) := by
+  induction a using WithTop.recTopCoe with
+  | top => simp
+  | coe a => simp
+
+/-- **Johnson's all-pairs shortest-path distance.**  Run Bellman-Ford from `u`
+in the reweighted graph, then adjust by `h(v) - h(u)`. -/
+noncomputable def johnsonDist (hNC : G.NoNegCycle) (u v : V) : WithTop ℝ :=
+  let h := G.johnsonPotential hNC
+  let d_hat := (G.reweightedGraph h).relaxDist u (Fintype.card V - 1) v
+  d_hat + (h v : WithTop ℝ) - (h u : WithTop ℝ)
+
+/-- **Theorem (Johnson correctness).**  `johnsonDist hNC u v` equals the
+shortest-path distance `δ(u, v)` in the original graph `G`.  (CLRS Theorem 25.5) -/
+theorem johnsonDist_isShortestDist (hNC : G.NoNegCycle) (u v : V) :
+    G.IsShortestDist u v (G.johnsonDist hNC u v) := by
+  let h := G.johnsonPotential hNC
+  have h_no_neg : (G.reweightedGraph h).NoNegCycle := G.reweightedGraph_noNegCycle hNC
+  let d_hat := (G.reweightedGraph h).relaxDist u (Fintype.card V - 1) v
+  have h_sd_dhat : (G.reweightedGraph h).IsShortestDist u v d_hat :=
+    (G.reweightedGraph h).relaxDist_isShortestDist h_no_neg u v
+  unfold johnsonDist
+  -- Let d := d_hat + h(v) - h(u). Then d + h(u) - h(v) = d_hat.
+  -- So by reweighted_isShortestDist.mp, G.IsShortestDist u v d.
+  have h_algebra : ((d_hat + (h v : WithTop ℝ) - (h u : WithTop ℝ)) +
+      (h u : WithTop ℝ) - (h v : WithTop ℝ)) = d_hat :=
+    (add_sub_add_sub_eq d_hat (h u) (h v)).symm
+  have h_equiv := G.reweighted_isShortestDist h u v
+    (d_hat + (h v : WithTop ℝ) - (h u : WithTop ℝ))
+  rw [← h_algebra] at h_sd_dhat
+  exact h_equiv.mp h_sd_dhat
+
+
 end WeightedGraph
 end Chapter24
 end CLRS
diff --git a/docs/clrs-proof-progress.csv b/docs/clrs-proof-progress.csv
index ae9b5a5..6f8b5c1 100644
--- a/docs/clrs-proof-progress.csv
+++ b/docs/clrs-proof-progress.csv
@@ -1,36 +1,36 @@
-chapter_no,chapter_title,repo_status,represented_sections,tracked_key_theorems,proved_tracked_theorems,missing_core_groups,completion_read,proved_key_theorem_groups,remaining_core_groups,evidence_source,notes
-1,The Role of Algorithms,expository,Chapter_01,0,0,0,Guide page only,Project conventions and reader contract,None,CLRSLean/Chapter_01.lean,No formal theorem target.
-2,Getting Started,main-proof-complete,2.1;2.2;2.3,6,6,0,Selected chapter sections complete,Insertion sort sortedness and permutation; insertion-sort quadratic comparison bound; merge-sort sortedness/permutation and power-of-two recurrence,Optional strengthening: full RAM semantics; arbitrary-size merge-sort recurrence; exercises,CLRSLean/Chapter_02.lean; CLRSLean/Status.lean,Current main section interfaces are stable.
-3,Growth of Functions,main-proof-complete,3.1;3.2,47,47,0,The asymptotic wrapper standard-function comparison table Fibonacci growth and iterated logarithm are complete,CLRS asymptotic notation wrappers; polynomial/exponential/log/factorial/harmonic/floor-ceiling growth facts; complete comparison hierarchy 1 < log(log n) < log n < n < n^a < 2^n < n! with log_b base-change facts; Fibonacci-number growth via Binet closed form Theta(phi^n) and closest-integer bound; iterated logarithm lg* (definition tower recurrence monotonicity and o(log n) slow growth),None,CLRSLean/Chapter_03.lean; CLRSLean/Status.lean,"All tracked theorem names compile; the CLRS 3.2 comparison table is complete, including Fibonacci-number growth and the iterated logarithm lg*."
-4,Divide-and-Conquer,main-proof-complete,4.1;4.2;4.3;4.4;4.5;4.6,94,94,0,Textbook-facing Master cases 1-3 plus recursive Strassen runtime and executable maximum-subarray abstract runtime complete,Maximum subarray correctness; linear prefix/suffix/crossing scan correctness; execution-attached exact scan-transition counts; costed midpoint execution erasure and correctness; exact mixed floor/ceiling cost recurrence; all-input Theta(n log n) executable control-step bound; Strassen 2x2 block algebra; recursive Strassen algorithm with correctness and padding; Strassen Theta(n^(log2 7)) runtime via Master case 1; substitution templates; recursion-tree expansions; exact-power Master cases; floor/ceiling all-input transfer and discrete Master wrappers; real-log case-1 bridge; real-log-log case-2 bridge; case-3 regularity bridge from tailDominatedScale to the forcing function,None; low-level List allocation/copying integer operations explicit split-tree construction and RAM semantics are optional refinements,CLRSLean/Chapter_04.lean; CLRSLean/Chapter_04/Section_04_1_Maximum_Subarray.lean; CLRSLean/Chapter_04/Section_04_2_Strassen_Algorithm.lean; Tests/Chapter_04_Interface.lean; CLRSLean/Status.lean; docs/chapters/chapter-04.md; docs/proof-map.md,The maximum-subarray metric counts recursive frames scan transitions and constant-size candidate choices; its scan counters are proved from the costed scan executions; it excludes explicit split-tree construction integer arithmetic List allocation/copying garbage collection and RAM semantics.
-5,Probabilistic Analysis and Randomized Algorithms,selected-section-complete,5.1;5.2;5.3;5.4,23,23,0,Sections 5.1-5.3 and the base §5.4 models are complete; the §5.4 streak tail and executable on-line hiring foundations are proved,Hiring problem finite rank-symmetry probability; harmonic expectation; logarithmic asymptotic expected-hires theorem; hat-check expected fixed points equal 1 via indicators and permutation symmetry; RANDOMIZE-IN-PLACE uniform permutation (Lemma 5.5) via choice-vector bijection; birthday-paradox expected collisions k(k-1)/(2n); balls-and-bins expected occupancy k/n; longest-streak tail bound n/2^t; executable on-line threshold strategy with exact some/none contracts and finite success-probability definition,None; expected-longest-streak and on-line hiring asymptotics are chapter-end Problems tracked separately from the selected-section milestone,CLRSLean/Chapter_05.lean; CLRSLean/Chapter_05/Section_05_4_Probabilistic_Analysis.lean; CLRSLean/Chapter_05/Section_05_4_Probabilistic_Analysis/OnlineHiring.lean; Tests/Chapter_05_Interface.lean; CLRSLean/Status.lean,Uses finite discrete uniform probability over rank symmetry uniform permutations product-uniform sample spaces and independent-swap-choice sample spaces; the additional streak and on-line hiring asymptotics remain a separate chapter-end Problems track.
-6,Heapsort,main-proof-complete,6.1;6.2;6.3;6.4;6.5,78,78,0,Main Chapter 6 proof stack complete for current array/functional models with connected coarse unit control-step envelopes,Indexed heap predicates; MAX-HEAPIFY repair; BUILD-MAX-HEAP; in-place heapsort invariant and correctness; costed heapify/build/heapsort erasure and coarse O(n)/O(n^2)/O(n^2) envelopes; priority-queue operation state theorems,None; tight textbook O(log n)/O(n)/O(n log n) costs and imperative RAM/List-operation semantics are optional refinements,CLRSLean/Chapter_06.lean; CLRSLean/Chapter_06/Section_06_4_Heapsort/CostedExecution.lean; Tests/Chapter_06_Interface.lean; CLRSLean/Status.lean,"The unit control-step metric counts heapify frames and nontrivial extraction transitions; build orchestration, guards, List operations, allocation, and calls are not charged."
-7,Quicksort,selected-section-complete,7.1;7.2;7.3,30,30,0,Functional correctness comparison recurrences mutable-Array PARTITION and pairwise comparison probability are proved; sum-of-probabilities bridge to the closed form and Theta(n log n) are complete,Partition correctness; scan-state partition loop; mutable-Array PARTITION refinement (partitionOnArray); quicksort sortedness/permutation; quadratic comparison bound; randomized-quicksort expected-comparison named closed form and harmonic bounds; random-permutation first-choice symmetry; pairwise comparison probability compared_prob = 2/(j-i+1); sum_compared_prob_eq_expectedComparisons bridge; expectedComparisons_isBigTheta_nlogn,None; array-level refinement and RAM latency,CLRSLean/Chapter_07.lean; CLRSLean/Chapter_07/Section_07_1_Description_Of_Quicksort.lean; CLRSLean/Chapter_07/Section_07_2_Performance_Of_Quicksort.lean; CLRSLean/Chapter_07/Section_07_3_Randomized_Quicksort.lean,The bridge between the random-permutation probability model and the algebraic closed form is proved via sum_compared_prob_eq_expectedComparisons; the Theta(n log n) asymptotic follows from expectedComparisons_isBigTheta_nlogn.
-8,Sorting in Linear Time,main-proof-complete-for-correctness,8.2;8.3;8.4,29,29,0,Correctness mutable counting-sort output and the bucket-sort CLRS unit-cost true-expectation theorem are complete,Stable counting sort; count-table refinement; mutable output-array counting sort with linear work bound; abstract and natural-key radix sort; deterministic bucket-sort correctness; finite-uniform bucket collision and second moment; textbookBucketSortCost; fintypeExpect_textbookBucketSortCost_eq_expectedBucketSortCost; expectedTextbookBucketSortCost_isBigO,None; a single-pass executable bucket builder costed per-bucket sorter and execution-cost refinement are optional implementation layers,CLRSLean/Chapter_08.lean; CLRSLean/Chapter_08/Section_08_2_Counting_Sort.lean; CLRSLean/Chapter_08/Section_08_2_Counting_Sort/CountTables.lean; CLRSLean/Chapter_08/Section_08_2_Counting_Sort/MutableOutputArray.lean; CLRSLean/Chapter_08/Section_08_3_Radix_Sort.lean; CLRSLean/Chapter_08/Section_08_4_Bucket_Sort.lean; CLRSLean/Status.lean; Tests/Chapter_08_Interface.lean,The CLRS unit-cost random variable has linear expectation; executable cost refinement and RAM accounting do not block the mathematical correctness milestone.
-9,Medians and Order Statistics,main-proof-complete,9.1;9.2;9.3,72,72,0,Sections 9.1-9.3 are complete for pure functional correctness and CLRS comparison and partition-work costs,Pairwise simultaneous minimum/maximum correctness; CLRS 3 floor(n/2) comparison bound; rank certificates; specification select; quickselect; pivot-parametric SELECT totality and correctness; five-element median certificate; grouped split counts; recursive median-of-medians pivot membership totality correctness and branch bound; linear recurrence induction; schedule-driven fresh-rank path cost erasure and rank correctness; pointwise actual-continuation-to-larger-side coupling; nested conditional-uniform RANDOMIZED-SELECT expectation; concrete-to-majorizer bridge; expected partition-work bound E[C] <= 4*c*n; end-to-end recursive median-of-medians comparison bound including nested pivot work <= 100n,,CLRSLean/Chapter_09.lean; CLRSLean/Chapter_09/Section_09_1_Minimum_And_Maximum.lean; CLRSLean/Chapter_09/Section_09_2_Select_By_Rank.lean; CLRSLean/Chapter_09/Section_09_3_Deterministic_Select.lean; CLRSLean/Chapter_09/Section_09_3_Deterministic_Select/Randomized_Select.lean; Tests/Chapter_09_Interface.lean; Tests/Chapter_09_Closure.lean; CLRSLean/Status.lean,No unfinished proof markers in the represented modules; randomized cost charges c*currentLength only and excludes RNG selectByRank specification sorting list primitives allocation and RAM work
-10,Elementary Data Structures,selected-section-complete,10.1;10.2;10.4,12,12,0,Functional stack queue list models and the rooted-tree left-child/right-sibling encoding are complete for the represented structures,Stack pop/push theorem; queue enqueue/dequeue theorems; linked-list search and delete facts; rooted-tree rose/LCRS forest round-trip isomorphism and Equiv bijection; single-tree round trip; preorder and node-count structure preservation,None; pointer memory and free-list allocation are optional low-level refinements,CLRSLean/Chapter_10.lean; CLRSLean/Chapter_10/Section_10_4_Rooted_Trees.lean; CLRSLean/Status.lean,Current model intentionally avoids imperative memory; the represented functional interfaces are complete.
-11,Hash Tables,main-proof-complete-for-correctness,11.1;11.2;11.3;11.4;11.5,51,51,0,The represented deterministic probabilistic universal-hashing open-addressing and perfect-hashing theorem stack is complete,Direct-address insert/search/delete; deterministic chained hash insert/delete/search facts; finite-uniform singleton bucket probability; uniform-average additivity and nonnegativity; expected chain length equals load factor; unsuccessful-search cost equals one plus load factor and is at least one; finite insert increases total chain length load factor expected chain length and unsuccessful-search cost; SUHA true-expectation chain length and unsuccessful-search cost; SUHA pairwise collision probability equals one over m; SUHA successful-search cost equals one plus (n-1)/(2m); universal random hash-function expected collision and search-cost bounds; division and multiplication method range bounds; concrete prime-field affine universal family satisfying IsUniversal with instantiated collision and search-cost bounds; open-addressing functional model correctness; linear/quadratic/double hashing probe schemes; uniform-hashing tail probability bounds; expected unsuccessful/insertion/successful probe bounds; two-level perfect hash model and membership correctness; secondary collision-free probability at least 1/2 (Theorem 11.9); expected total space less than 2n (Theorem 11.10),None; RAM or probe-count operational semantics are optional low-level refinements,CLRSLean/Chapter_11.lean; CLRSLean/Chapter_11/Section_11_2_Chained_Hash_Tables.lean; CLRSLean/Chapter_11/Section_11_3_Hash_Functions.lean; CLRSLean/Chapter_11/Section_11_4_Open_Addressing.lean; CLRSLean/Chapter_11/Section_11_5_Perfect_Hashing.lean; CLRSLean/Status.lean,Chapter 11 proves SUHA successful and unsuccessful search costs universal hashing collision and search-cost bounds an affine universal family open-addressing expected-probe bounds and two-level perfect hashing; only low-level operational accounting remains.
-12,Binary Search Trees,main-proof-complete-for-correctness,12.1,40,40,0,Functional BST zipper parent-navigation and the represented imperative pointer-heap TRANSPLANT/insert refinements are complete,Search; min/max; insertion; complete successor/predecessor specifications; functional delete membership and ordering; search and neighbor queries after updates; faithful zipper reconstruction; iterative search equivalence; transplant ordering preservation; deletion-via-transplant equivalence; parent-ascent successor/predecessor equivalence; imperative pointer-heap node/store model; heap-to-tree abstraction faithfulness; pointer frame rules; in-place TRANSPLANT refinement; pointer TREE-INSERT leaf-attachment refinement,None; pointer-level in-place delete and explicit RAM costs are optional low-level refinements,CLRSLean/Chapter_12.lean; CLRSLean/Chapter_12/Section_12_1_Binary_Search_Trees.lean; CLRSLean/Status.lean; Tests/Chapter_12_Interface.lean,The represented mathematical and refinement interfaces are complete; lower-level pointer deletion and RAM accounting do not block the correctness milestone.
-13,Red-Black Trees,main-proof-complete-for-correctness,13.1,39,39,0,Executable insertion and deletion with exact membership correctness red-black shape preservation and the logarithmic-height theorem are proved,Rotation membership; repaint membership; no-red-red; black-height; local red-black shape preservation; insertion-fixup certificates; executable insert and redBlackShape_insert; height_log_bound (Lemma 13.1); executable baldL/baldR/splitMin/join/del/delete; inTree_delete_iff; local delete-fixup membership and shape certificates; deficit-absorbing rebalancer certificates baldL_shape and baldR_shape; splitMin_invariant; del_invariant; redBlackShape_delete,None; pointer-level mutation and RAM cost semantics are optional refinements,CLRSLean/Chapter_13.lean; CLRSLean/Chapter_13/Section_13_1_Red_Black_Trees.lean; CLRSLean/Status.lean,Deletion preserves red-black shape via the splitMin/join doubly-black rebalancing pipeline (redBlackShape_delete); the height theorem is complete.
-14,Augmenting Data Structures,main-proof-complete-for-correctness,14.1;14.3,67,67,0,Order-statistic and interval-tree augmentation layers represented; the size invariant and generic AugmentedRBTree deletion pipeline are proved,Size augmentation invariant; size recomputation; key preservation; size/rank-preserving local rotations; augmented rank-select correctness; generic rotation-invariant augmentation theorem (CLRS 14.1); interval overlap semantics and search specification; OSRBTree wellSized_insert and wellSized_delete with toRB refinement; generic AugmentedRBTree executable insertion and deletion with wellAugmented_insert and wellAugmented_delete for any augmentation; repaintRoot/rootBlack/baldL/baldR/splitMin/join/del/delete pipeline preserving WellAugmented; size and max-high instances recovered,None; pointer-level mutation and RAM cost semantics,CLRSLean/Chapter_14.lean; CLRSLean/Chapter_14/Section_14_1_Order_Statistic_Trees.lean; CLRSLean/Chapter_14/Section_14_3_Interval_Trees.lean; CLRSLean/Status.lean,The generic AugmentedRBTree deletion pipeline mirrors OSRBTree with wellAugmented_delete for any Augmentation; both order-statistic and interval-tree instances are now fully proved through both insertion and deletion.
-15,Dynamic Programming,selected-section-complete,15.1;15.2;15.4;15.5,76,76,0,The four represented dynamic-programming examples have mathematical optimality and executable recurrence/reconstruction layers,Bellman rod-cutting recurrence and bottom-up value; mutable-Array bottom-up rod-cutting refinement; matrix-chain lower bound computable optimum split reconstruction and correctness; LCS certificate table recurrence executable length/reconstruction and correctness; optimal-BST recurrence bottom-up optimum plan reconstruction and correctness,None; further mutable-array implementations and explicit RAM costs are optional refinements,CLRSLean/Chapter_15.lean; CLRSLean/Chapter_15/Section_15_1_Rod_Cutting.lean; CLRSLean/Chapter_15/Section_15_2_Matrix_Chain_Multiplication.lean; CLRSLean/Chapter_15/Section_15_4_Longest_Common_Subsequence.lean; CLRSLean/Chapter_15/Section_15_5_Optimal_Binary_Search_Trees.lean; CLRSLean/Status.lean,The represented examples are complete at the mathematical and pure executable layers; mutable refinements do not block their milestone.
-16,Greedy Algorithms,main-proof-complete,16.1;16.2;16.3;16.4;16.5,32,32,0,Activity selection greedy meta-theorems Huffman weighted-matroid greedy optimality and task scheduling are complete,Activity-selection greedy optimality; Huffman V2 frequency-table optimality and minimum-cost wrappers; weighted-matroid GREEDY optimality (Theorems 16.6/16.7/16.10) built on Mathlib matroids; GreedyProblem meta-theorem and gsolve_optimal (CLRS §16.2 greedy-choice property and optimal substructure); scheduling-matroid construction (Theorem 16.13) and min-penalty schedule via greedy optimality,None; exercises are tracked separately from the chapter milestone,CLRSLean/Chapter_16.lean; CLRSLean/Chapter_16/Section_16_2_Greedy_Meta.lean; CLRSLean/Chapter_16/Section_16_4_Matroids.lean; CLRSLean/Chapter_16/Section_16_5_Task_Scheduling.lean; CLRSLean/Status.lean,The represented Sections 16.1-16.5 cover the core chapter theorem groups; exercises remain an optional second track.
-17,Amortized Analysis,selected-section-complete,17.1;17.2;17.4,66,66,0,The represented aggregate accounting potential stack/counter and dynamic-table analyses are complete,Aggregate/accounting/potential telescoping; MULTIPOP; executable binary-counter one-step and multi-step trace bounds; dynamic-table potential nonnegativity; concrete amortized-cost unfoldings and transition/capacity wrappers,None; mutable-array copying allocator constants and sharper RAM models are optional refinements,CLRSLean/Chapter_17.lean; CLRSLean/Chapter_17/Section_17_1_Amortized_Framework.lean; CLRSLean/Chapter_17/Section_17_1_Amortized_Framework/Section_17_2_Stack_And_Counter.lean; CLRSLean/Chapter_17/Section_17_4_Dynamic_Tables.lean; Tests/Chapter_17_Interface.lean,No sorry/admit/axiom in Chapter_17; the size-level represented theorem stack is complete.
-18,B-Trees,partial,18.1;18.2;18.3,62,62,1,First-pass mathematical B-tree model represented,Search correctness direct base search success/failure wrappers minimum-key height expression base positivity recurrence and height monotonicity split-child direct validity membership/search preservation direct split old-key and failed-membership corollaries insertion/deletion membership Prop-level deletion membership/search success and direct wrappers direct insertion/deletion validity short-name wrappers equality-key update-query wrappers successful and unsuccessful search-after-update specs membership-driven search-after-update wrappers and direct inserted/deleted-key old-key query preservation old failed-search preservation wrappers failed-membership corollaries and direct failed-membership preservation wrappers,Full occupancy separator and same-depth invariant stack plus node-level deletion repair,CLRSLean/Chapter_18.lean; Tests/Chapter_18_Interface.lean,Disk-page pointer mutation and I/O/RAM semantics are optional low-level refinements and are not part of the remaining core group.
-19,Fibonacci Heaps,partial,19.1;19.4,112,112,1,Abstract finite-set Fibonacci heap model plus concrete rooted-tree degree bound represented,Make-heap valid make-heap empty-minimum potential-zero potential-nonnegative minimum membership lower-bound and empty-result wrappers direct minimum/extract-min empty-result and nonempty-result wrappers insert valid and insert-membership insert-self insert-old insert-failed-membership insert-minimum direct membership/lower-bound wrappers insert-empty-minimum union valid and union-membership union-left union-right union-failed-membership union-minimum direct membership/lower-bound wrappers union-empty-minimum union-nonempty-minimum extract-min valid and extract-min-membership extract-min-removed extract-min-old-key-preservation extract-min-failed-membership empty-extract-min nonempty-extract-min remaining-minimum direct membership/lower-bound wrappers remaining-empty-minimum remaining-nonempty-minimum decrease-key valid and decrease-key-membership decrease-key-new decrease-key-replaced-key query wrappers decrease-key-old-key-preservation decrease-key-failed-membership decrease-key-minimum direct membership/lower-bound wrappers decrease-key-empty-minimum delete valid and delete-membership delete-removed delete-old-key-preservation delete-failed-membership direct failed-membership preservation wrappers delete-minimum direct membership/lower-bound wrappers delete-empty-minimum delete-nonempty-minimum potential telescoping Fibonacci lower-bound recurrence positivity monotonicity two-step doubling even-index and half-index power-of-two lower bounds conditional degree-to-log wrappers and conservative degree budget concrete FTree rooted-tree model degree and size Lemma-19.1 marked-tree Wellformed invariant true subtree-size theorem size>=F(d+2) golden-ratio phi^d<=F(d+2) and phi^d<=size logarithmic maximum-degree bounds log_phi n floor-log_phi n and 2*log2 n budget CONSOLIDATE link invariant-maintenance wellformed-append-child link and link-degree extremal minTree tightness witness size=F(d+2),Pointer forest circular root lists executable CONSOLIDATE and cascading-cut procedures duplicate handles and amortized O(log n)/O(1) cost accounting over the potential function,CLRSLean/Chapter_19.lean; Tests/Chapter_19_Interface.lean,"Potential theorem instantiates Chapter 17; Section 19.4 seals the true Fibonacci subtree-size logarithmic degree bound D(n) <= floor(log_phi n) on an abstract wellformed tree model, shown tight by the extremal minTree family."
-20,van Emde Boas Trees,main-proof-complete-for-correctness,20.1;20.2;20.3,200,200,0,All seven operations of the recursive cached-min/max model are proved correct with constant cached extrema and control-flow-aware O(log log u) bounds,High-low-index arithmetic and the finite-set specification layer plus recursive tower-universe VEBTree and VEBTreeMM semantics; cached minimum and maximum correctness; lazy-min insert invariant preservation and exact Finset.insert refinement; strong recursive successor least-greater and predecessor greatest-less specifications; exact recursive delete Finset.erase refinement; branch-faithful member insert successor predecessor and delete cost bounds; separate delete work and depth bounds; all-operation O(log log u) packaging,Concrete pointer/array storage and hardware-level RAM constants only,CLRSLean/Chapter_20.lean; CLRSLean/Chapter_20/Section_20_3_Recursive_VEB.lean; Tests/Chapter_20_Interface.lean; Tests/Chapter_20_Axioms.lean,The recursive mathematical completion boundary is sealed; concrete pointer/array allocation and hardware-level RAM timing remain a separate implementation refinement.
-21,Data Structures for Disjoint Sets,main-proof-complete,21.1;21.2;21.3;21.4,84,84,0,"The represented Chapter 21 stack is complete: abstract and executable correctness, real Batteries traversal costs, reachable rank mass, and the concrete O((m+n) alpha(n)) amortized bound are proved",Partition equivalence and exact merge semantics; operation-trace monotonicity; singleton linked lists; weighted-union exact refinement; representative invariant; per-rewrite size doubling; per-element log2 and aggregate n log2 n rewrite bounds; singleton Batteries forests; path-compressing find partition preservation and representative correctness; union-by-rank exact merge refinement; Boolean equivalence-query correctness; exact parent-edge traversal counter; conserved root-mass budget through find/link/union; costed execution erasure and abstract run refinement; per-find and per-union log2 bounds; whole-run m * (2 log2 n + 3) intermediate bound; inverse-Ackermann definition and minimality; Ackermann level/index node potential; path-compression potential monotonicity; equal-rank link pair bound and global link increase at most two; released/boundary/unpleasant path classification; per-find and per-union inverse-Ackermann amortized bounds; whole-run 9 * (m+n) * alpha(n) bound; 18 * m * alpha(n) corollary when n <= m; Chapter 23 union-find connectivity and cycle-test bridge,No remaining core Chapter 21 group; lower-level mutable-array/RAM constants and a stateful Chapter 23 Kruskal scan are separate refinements,CLRSLean/Chapter_21.lean; CLRSLean/Chapter_21/Section_21_1_Disjoint_Set_Operations.lean; CLRSLean/Chapter_21/Section_21_2_Linked_List_Representation.lean; CLRSLean/Chapter_21/Section_21_3_Disjoint_Set_Forests.lean; CLRSLean/Chapter_21/Section_21_4_Analysis.lean; CLRSLean/Chapter_21/Section_21_4_Analysis/CostedExecution.lean; CLRSLean/Chapter_21/Section_21_4_Analysis/InverseAckermann.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim/S1_UnionFindBridge.lean; Tests/Chapter_21_Interface.lean; Tests/Chapter_23_UnionFind_Interface.lean; docs/proof-audits/chapter-21-closure-2026-07-10.md,No sorry/admit/axiom in the represented chapter; the concrete cost model counts actual parent traversals plus constant operation overhead and proves the advertised inverse-Ackermann bound.
-22,Elementary Graph Algorithms,main-proof-complete-for-correctness,22.1;22.2;22.3;22.4;22.5,47,47,0,"Main functional correctness is complete: CLRS FIFO BFS exactly characterizes reachability and returns shortest distances with a rooted predecessor tree, DFS includes the white-path theorem, timestamp parenthesis theorem, parent-forest ancestor/interval characterization, unique edge classification, and SCC timestamp theory, Kahn and CLRS DFS finish-time topological sorts are correct for DAGs, and Kosaraju returns an SCC partition; only explicit algorithm-cost refinements remain","Finite directed graph with adjacency function; walk/path/cycle definitions; reachability; reflexivity/transitivity/adjacency lemmas; connected components; undirected graph symmetry; fuelled BFS soundness and completeness; BFS closure and termination measure; exact-edge ReachableIn and IsShortestDistance; labelled BFSState with distance and parent; bfsState projection to the reachability BFS; FIFO distance invariant; bfsState_distance_eq_some_iff; bfsState parent edge, unit-level, root-path, coverage, and acyclicity facts; bfsState_isBFSPredecessorTree; bfsState_correct; functional DFS with colors, discovery/finish times, and parents; global DFS color/timestamp invariants; finite white reachability; dfsVisit_blackens_iff_whiteReachable; ParenthesisInvariant; dfs_parenthesis; dfs_parenthesis_cases; dfs_intervals_not_cross; discovery-state and timestamp bridges; ancestor reachability; dfs_parent_discovery_lt; intervalNestedInside_dfs_implies_ancestor; intervalNestedInside_dfs_iff_ancestor; IsDFSTreeEdge; IsDFSBackEdge; IsDFSForwardEdge; IsDFSCrossEdge; dfs_edge_classification_unique; dfs_tree_or_forward_edge_iff_timestamps; dfs_back_edge_iff_timestamps; dfs_cross_edge_iff_timestamps; maximum-finish and first-discovery facts; SCC finish-time ordering; DAG predicate; indegree; Kahn topological sort correctness; isDAG_no_dfs_back_edge; dfs_finish_time_decreases_on_dag_edge; DFS finish-time order permutation and pairwise sorting; dfsTopologicalSort_isTopologicalOrder; transpose graph; strong connectivity and SCC predicates; collecting DFS; Kosaraju order properties; Kosaraju component strong connectivity and maximality; pairwise disjointness; coverage; unique membership; kosarajuComponents_isSCCPartition",No remaining core correctness group; explicit work and RAM-cost refinements,CLRSLean/Chapter_22.lean; CLRSLean/Chapter_22/Section_22_1_Representing_Graphs.lean; CLRSLean/Chapter_22/Section_22_2_BFS.lean; CLRSLean/Chapter_22/Section_22_3_DFS.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S1_WhitePath.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S2_Intervals.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S3_Bridge.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S4_SCC.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S5_EdgeClassification.lean; CLRSLean/Chapter_22/Section_22_4_Topological_Sort.lean; CLRSLean/Chapter_22/Section_22_5_Strongly_Connected_Components.lean; CLRSLean/Chapter_22/Section_22_5_Strongly_Connected_Components/MergeSortCongr.lean; CLRSLean/Status.lean; Tests/Chapter_22_Interface.lean; Tests/Chapter_22_Closure.lean; docs/proof-audits/chapter-22-closure-2026-07-10.md,"DFS parenthesis, parent-forest ancestor/interval characterization, and unique edge classification are fully proved through dfs_parenthesis, intervalNestedInside_dfs_iff_ancestor, and dfs_edge_classification_unique; Kosaraju correctness is fully proved through scc_finish_time_order, scc_finish_order, kosarajuComponent_scc_core, and kosarajuComponents_isSCCPartition; Chapter 22 main functional correctness is formally sealed by the 2026-07-10 closure audit; explicit work and RAM-cost refinements remain"
-23,Minimum Spanning Trees,main-proof-complete-for-correctness,23.1;23.2,52,52,0,Mathematical correctness and functional implementation refinements are complete: cut property canonical exchange sorted and stateful Kruskal plus executable indexed-queue Prim,Finite edge-labelled graph and spanning-tree specification; safe-edge and cut-property theorem; canonical unique tree path and automatic exchange; complete sorted Kruskal MST theorem; real Chapter 21 costed union-find threaded through every Kruskal edge; connectivity invariant and mathematical-selection refinement; inverse-Ackermann scan bound and complete O(E log E) work composition; Prim key parent decrease-key and extract-min queue; concrete frontier provider; executable run refinement to PrimTrace; binary-heap O(E log V) operation-count theorem; complete Prim MST theorem,No remaining core mathematical or functional algorithm group; concrete Batteries binary-heap array refinement and mutable/RAM write semantics remain separate low-level refinements,CLRSLean/Chapter_23.lean; CLRSLean/Chapter_23/Section_23_1_Growing_Minimum_Spanning_Trees.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim/S1_UnionFindBridge.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim/S2_StatefulKruskal.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim/S3_ExecutablePrim.lean; CLRSLean/Status.lean; Tests/Chapter_23_Interface.lean; Tests/Chapter_23_Closure.lean; Tests/Chapter_23_UnionFind_Interface.lean; Tests/Chapter_23_Implementation_Interface.lean; docs/proof-audits/chapter-23-closure-2026-07-11.md,The correctness boundary remains sealed and now has proved executable semantic and algorithm-level cost refinements.
-24,Single-Source Shortest Paths,selected-section-complete,24.1;24.2;24.3;24.4,22,22,0,Bellman-Ford DAG SSSP Dijkstra greedy correctness end-to-end executable loop and difference constraints are complete,Finite weighted directed-graph model; walks and walk weights; Bellman-Ford relaxation correctness and O(VE) work; DAG-SHORTEST-PATHS correctness and O(V+E) work; nonnegative-weight Dijkstra greedy invariant and O(E log V) abstract work; DijkstraState dijkstraInit dijkstraInit_invariant dijkstraStep DijkstraInvariant dijkstraStep_invariant dijkstraLoop dijkstraLoop_invariant dijkstraLoop_finish dijkstraLoop_correct; difference-constraint feasibility iff no negative cycle,None; per-edge relaxation ordering and mutable/RAM cost refinement,CLRSLean/Chapter_24.lean; CLRSLean/Chapter_24/Section_24_1_Bellman_Ford.lean; CLRSLean/Chapter_24/Section_24_2_SSSP_In_DAGs.lean; CLRSLean/Chapter_24/Section_24_3_Dijkstra.lean; CLRSLean/Chapter_24/Section_24_4_Difference_Constraints.lean,The Dijkstra initialization gap is closed: dijkstraInit pre-settles the source and pre-relaxes outgoing edges so DijkstraInvariant holds initially; dijkstraLoop_invariant lifts it through the loop; dijkstraLoop_correct proves the final distance map equals δ.
-"25","All-Pairs Shortest Paths","partial","25.1;25.2;25.3","22","22","2","FASTER-APSP correctness is complete; Floyd-Warshall correctness complete (Lemma 25.7, Theorem 25.8, Theorem 25.3); predecessor matrix Pi and path reconstruction walk validity proved; negative-cycle detection proved; Johnson has augmented-graph reweighting definitions telescoping and nonnegativity and shortest-path preservation","Faster-APSP min-plus model Lemmas 25.1/25.2 stabilization and correctness; Floyd-Warshall D/floydWarshall/fwStep/Pi/floydWarshallPi/fwReconstructPath; Johnson augmented graph; reweightedGraph; reweightedWalkWeight_eq; reweightedWeight_nonneg; reweighted_isShortestDist","Predecessor-matrix path-reconstruction weight equality; Johnson Bellman-Ford potential construction and end-to-end correctness","CLRSLean/Chapter_25.lean; CLRSLean/Chapter_25/Section_25_1_All_Pairs_Model.lean; CLRSLean/Chapter_25/Section_25_2_Floyd_Warshall.lean; CLRSLean/Chapter_25/Section_25_3_Johnsons_Algorithm.lean","Section 25.1 is complete under no negative cycles. Section 25.2 has Floyd-Warshall correctness (Theorems 25.7, 25.8, 25.3), predecessor matrix Pi, path reconstruction (walk validity), and negative-cycle detection. Path-reconstruction weight equality is deferred. Section 25.3 proves the reweighting algebra including shortest-path preservation under reweighting."
-26,Maximum Flow,partial,26.1;26.2;26.6,9,9,3,The flow model generic no-augmenting-path maximality easy MFMC direction and Edmonds-Karp monotonic-distance lemma are proved,FlowNetwork model; feasible flow; flow value; Lemma 26.5 net-flow-across-cut; residual network augmenting path; generic Ford-Fulkerson maximality from no-augmenting-path; easy MFMC direction cut-capacity-implies-maximal; residual path length; shortest-path distance; Lemma 26.7 monotonic distance,Full Max-Flow Min-Cut converse/equivalence; executable BFS augmentation loop and O(VE^2) theorem; Section 26.3 bipartite-matching reduction and correctness,CLRSLean/Chapter_26.lean; CLRSLean/Chapter_26/Section_26_1_Flow_Networks.lean; CLRSLean/Chapter_26/Section_26_2_Edmonds_Karp.lean; CLRSLean/Chapter_26/Section_26_6_MaxFlow_MinCut.lean,"The represented files prove the flow foundation the generic Ford-Fulkerson maximality direction Lemma 26.7 and one MFMC direction. Section 26.3 is not present on main, and neither the MFMC converse nor the executable Edmonds-Karp complexity theorem is proved."
-27,Multithreaded Algorithms,partial,27.1;27.2,28,28,1,Computation-DAG and spawn-tree model with honest span and the four textbook parallel-algorithm work/span recurrences are represented and proved at the power-of-two boundary,Forward-edge computation DAG with DP longest-path span and span-le-work; spawn/sync tree unit-overhead model with span-le-work; balanced parallel-loop tree exact work and span with logarithmic depth lower bound; P-MATMUL work Theta(n^3) and span Theta(log n) pow2 closed forms plus all-input upper bounds; P-MERGE work Theta(n) and span Theta(log^2 n) pow2 closed forms; P-MERGE-SORT work Theta(n log n) and span Theta(log^3 n) pow2 closed forms; parallel Strassen work Theta(n^(log2 7)) and span Theta(log n) pow2 closed forms,Greedy-scheduler bound (Theorem 27.1/27.2); all-input Theta-bounds for the merge-based costs; executable P-MERGE and P-MERGE-SORT refinements,CLRSLean/Chapter_27.lean; CLRSLean/Chapter_27/Section_27_1_Multithreading_Model.lean; CLRSLean/Chapter_27/Section_27_2_4_Algorithms.lean; Tests/Chapter_27_Interface.lean; CLRSLean/Status.lean,No sorry/admit/axiom in Chapter_27; asymptotic claims are exact closed forms on powers of two with all-input upper bounds where proved.
-28,Matrix Operations,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_28 module exists.
-29,Linear Programming,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_29 module exists.
-30,Polynomials and the FFT,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_30 module exists.
-31,Number-Theoretic Algorithms,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_31 module exists.
-32,String Matching,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_32 module exists.
-33,Computational Geometry,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_33 module exists.
-34,NP-Completeness,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_34 module exists.
-35,Approximation Algorithms,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_35 module exists.
+chapter_no,chapter_title,repo_status,represented_sections,tracked_key_theorems,proved_tracked_theorems,missing_core_groups,completion_read,proved_key_theorem_groups,remaining_core_groups,evidence_source,notes
+1,The Role of Algorithms,expository,Chapter_01,0,0,0,Guide page only,Project conventions and reader contract,None,CLRSLean/Chapter_01.lean,No formal theorem target.
+2,Getting Started,main-proof-complete,2.1;2.2;2.3,6,6,0,Selected chapter sections complete,Insertion sort sortedness and permutation; insertion-sort quadratic comparison bound; merge-sort sortedness/permutation and power-of-two recurrence,Optional strengthening: full RAM semantics; arbitrary-size merge-sort recurrence; exercises,CLRSLean/Chapter_02.lean; CLRSLean/Status.lean,Current main section interfaces are stable.
+3,Growth of Functions,main-proof-complete,3.1;3.2,47,47,0,The asymptotic wrapper standard-function comparison table Fibonacci growth and iterated logarithm are complete,CLRS asymptotic notation wrappers; polynomial/exponential/log/factorial/harmonic/floor-ceiling growth facts; complete comparison hierarchy 1 < log(log n) < log n < n < n^a < 2^n < n! with log_b base-change facts; Fibonacci-number growth via Binet closed form Theta(phi^n) and closest-integer bound; iterated logarithm lg* (definition tower recurrence monotonicity and o(log n) slow growth),None,CLRSLean/Chapter_03.lean; CLRSLean/Status.lean,"All tracked theorem names compile; the CLRS 3.2 comparison table is complete, including Fibonacci-number growth and the iterated logarithm lg*."
+4,Divide-and-Conquer,main-proof-complete,4.1;4.2;4.3;4.4;4.5;4.6,94,94,0,Textbook-facing Master cases 1-3 plus recursive Strassen runtime and executable maximum-subarray abstract runtime complete,Maximum subarray correctness; linear prefix/suffix/crossing scan correctness; execution-attached exact scan-transition counts; costed midpoint execution erasure and correctness; exact mixed floor/ceiling cost recurrence; all-input Theta(n log n) executable control-step bound; Strassen 2x2 block algebra; recursive Strassen algorithm with correctness and padding; Strassen Theta(n^(log2 7)) runtime via Master case 1; substitution templates; recursion-tree expansions; exact-power Master cases; floor/ceiling all-input transfer and discrete Master wrappers; real-log case-1 bridge; real-log-log case-2 bridge; case-3 regularity bridge from tailDominatedScale to the forcing function,None; low-level List allocation/copying integer operations explicit split-tree construction and RAM semantics are optional refinements,CLRSLean/Chapter_04.lean; CLRSLean/Chapter_04/Section_04_1_Maximum_Subarray.lean; CLRSLean/Chapter_04/Section_04_2_Strassen_Algorithm.lean; Tests/Chapter_04_Interface.lean; CLRSLean/Status.lean; docs/chapters/chapter-04.md; docs/proof-map.md,The maximum-subarray metric counts recursive frames scan transitions and constant-size candidate choices; its scan counters are proved from the costed scan executions; it excludes explicit split-tree construction integer arithmetic List allocation/copying garbage collection and RAM semantics.
+5,Probabilistic Analysis and Randomized Algorithms,selected-section-complete,5.1;5.2;5.3;5.4,23,23,0,Sections 5.1-5.3 and the base §5.4 models are complete; the §5.4 streak tail and executable on-line hiring foundations are proved,Hiring problem finite rank-symmetry probability; harmonic expectation; logarithmic asymptotic expected-hires theorem; hat-check expected fixed points equal 1 via indicators and permutation symmetry; RANDOMIZE-IN-PLACE uniform permutation (Lemma 5.5) via choice-vector bijection; birthday-paradox expected collisions k(k-1)/(2n); balls-and-bins expected occupancy k/n; longest-streak tail bound n/2^t; executable on-line threshold strategy with exact some/none contracts and finite success-probability definition,None; expected-longest-streak and on-line hiring asymptotics are chapter-end Problems tracked separately from the selected-section milestone,CLRSLean/Chapter_05.lean; CLRSLean/Chapter_05/Section_05_4_Probabilistic_Analysis.lean; CLRSLean/Chapter_05/Section_05_4_Probabilistic_Analysis/OnlineHiring.lean; Tests/Chapter_05_Interface.lean; CLRSLean/Status.lean,Uses finite discrete uniform probability over rank symmetry uniform permutations product-uniform sample spaces and independent-swap-choice sample spaces; the additional streak and on-line hiring asymptotics remain a separate chapter-end Problems track.
+6,Heapsort,main-proof-complete,6.1;6.2;6.3;6.4;6.5,78,78,0,Main Chapter 6 proof stack complete for current array/functional models with connected coarse unit control-step envelopes,Indexed heap predicates; MAX-HEAPIFY repair; BUILD-MAX-HEAP; in-place heapsort invariant and correctness; costed heapify/build/heapsort erasure and coarse O(n)/O(n^2)/O(n^2) envelopes; priority-queue operation state theorems,None; tight textbook O(log n)/O(n)/O(n log n) costs and imperative RAM/List-operation semantics are optional refinements,CLRSLean/Chapter_06.lean; CLRSLean/Chapter_06/Section_06_4_Heapsort/CostedExecution.lean; Tests/Chapter_06_Interface.lean; CLRSLean/Status.lean,"The unit control-step metric counts heapify frames and nontrivial extraction transitions; build orchestration, guards, List operations, allocation, and calls are not charged."
+7,Quicksort,selected-section-complete,7.1;7.2;7.3,30,30,0,Functional correctness comparison recurrences mutable-Array PARTITION and pairwise comparison probability are proved; sum-of-probabilities bridge to the closed form and Theta(n log n) are complete,Partition correctness; scan-state partition loop; mutable-Array PARTITION refinement (partitionOnArray); quicksort sortedness/permutation; quadratic comparison bound; randomized-quicksort expected-comparison named closed form and harmonic bounds; random-permutation first-choice symmetry; pairwise comparison probability compared_prob = 2/(j-i+1); sum_compared_prob_eq_expectedComparisons bridge; expectedComparisons_isBigTheta_nlogn,None; array-level refinement and RAM latency,CLRSLean/Chapter_07.lean; CLRSLean/Chapter_07/Section_07_1_Description_Of_Quicksort.lean; CLRSLean/Chapter_07/Section_07_2_Performance_Of_Quicksort.lean; CLRSLean/Chapter_07/Section_07_3_Randomized_Quicksort.lean,The bridge between the random-permutation probability model and the algebraic closed form is proved via sum_compared_prob_eq_expectedComparisons; the Theta(n log n) asymptotic follows from expectedComparisons_isBigTheta_nlogn.
+8,Sorting in Linear Time,main-proof-complete-for-correctness,8.2;8.3;8.4,29,29,0,Correctness mutable counting-sort output and the bucket-sort CLRS unit-cost true-expectation theorem are complete,Stable counting sort; count-table refinement; mutable output-array counting sort with linear work bound; abstract and natural-key radix sort; deterministic bucket-sort correctness; finite-uniform bucket collision and second moment; textbookBucketSortCost; fintypeExpect_textbookBucketSortCost_eq_expectedBucketSortCost; expectedTextbookBucketSortCost_isBigO,None; a single-pass executable bucket builder costed per-bucket sorter and execution-cost refinement are optional implementation layers,CLRSLean/Chapter_08.lean; CLRSLean/Chapter_08/Section_08_2_Counting_Sort.lean; CLRSLean/Chapter_08/Section_08_2_Counting_Sort/CountTables.lean; CLRSLean/Chapter_08/Section_08_2_Counting_Sort/MutableOutputArray.lean; CLRSLean/Chapter_08/Section_08_3_Radix_Sort.lean; CLRSLean/Chapter_08/Section_08_4_Bucket_Sort.lean; CLRSLean/Status.lean; Tests/Chapter_08_Interface.lean,The CLRS unit-cost random variable has linear expectation; executable cost refinement and RAM accounting do not block the mathematical correctness milestone.
+9,Medians and Order Statistics,main-proof-complete,9.1;9.2;9.3,72,72,0,Sections 9.1-9.3 are complete for pure functional correctness and CLRS comparison and partition-work costs,Pairwise simultaneous minimum/maximum correctness; CLRS 3 floor(n/2) comparison bound; rank certificates; specification select; quickselect; pivot-parametric SELECT totality and correctness; five-element median certificate; grouped split counts; recursive median-of-medians pivot membership totality correctness and branch bound; linear recurrence induction; schedule-driven fresh-rank path cost erasure and rank correctness; pointwise actual-continuation-to-larger-side coupling; nested conditional-uniform RANDOMIZED-SELECT expectation; concrete-to-majorizer bridge; expected partition-work bound E[C] <= 4*c*n; end-to-end recursive median-of-medians comparison bound including nested pivot work <= 100n,,CLRSLean/Chapter_09.lean; CLRSLean/Chapter_09/Section_09_1_Minimum_And_Maximum.lean; CLRSLean/Chapter_09/Section_09_2_Select_By_Rank.lean; CLRSLean/Chapter_09/Section_09_3_Deterministic_Select.lean; CLRSLean/Chapter_09/Section_09_3_Deterministic_Select/Randomized_Select.lean; Tests/Chapter_09_Interface.lean; Tests/Chapter_09_Closure.lean; CLRSLean/Status.lean,No unfinished proof markers in the represented modules; randomized cost charges c*currentLength only and excludes RNG selectByRank specification sorting list primitives allocation and RAM work
+10,Elementary Data Structures,selected-section-complete,10.1;10.2;10.4,12,12,0,Functional stack queue list models and the rooted-tree left-child/right-sibling encoding are complete for the represented structures,Stack pop/push theorem; queue enqueue/dequeue theorems; linked-list search and delete facts; rooted-tree rose/LCRS forest round-trip isomorphism and Equiv bijection; single-tree round trip; preorder and node-count structure preservation,None; pointer memory and free-list allocation are optional low-level refinements,CLRSLean/Chapter_10.lean; CLRSLean/Chapter_10/Section_10_4_Rooted_Trees.lean; CLRSLean/Status.lean,Current model intentionally avoids imperative memory; the represented functional interfaces are complete.
+11,Hash Tables,main-proof-complete-for-correctness,11.1;11.2;11.3;11.4;11.5,51,51,0,The represented deterministic probabilistic universal-hashing open-addressing and perfect-hashing theorem stack is complete,Direct-address insert/search/delete; deterministic chained hash insert/delete/search facts; finite-uniform singleton bucket probability; uniform-average additivity and nonnegativity; expected chain length equals load factor; unsuccessful-search cost equals one plus load factor and is at least one; finite insert increases total chain length load factor expected chain length and unsuccessful-search cost; SUHA true-expectation chain length and unsuccessful-search cost; SUHA pairwise collision probability equals one over m; SUHA successful-search cost equals one plus (n-1)/(2m); universal random hash-function expected collision and search-cost bounds; division and multiplication method range bounds; concrete prime-field affine universal family satisfying IsUniversal with instantiated collision and search-cost bounds; open-addressing functional model correctness; linear/quadratic/double hashing probe schemes; uniform-hashing tail probability bounds; expected unsuccessful/insertion/successful probe bounds; two-level perfect hash model and membership correctness; secondary collision-free probability at least 1/2 (Theorem 11.9); expected total space less than 2n (Theorem 11.10),None; RAM or probe-count operational semantics are optional low-level refinements,CLRSLean/Chapter_11.lean; CLRSLean/Chapter_11/Section_11_2_Chained_Hash_Tables.lean; CLRSLean/Chapter_11/Section_11_3_Hash_Functions.lean; CLRSLean/Chapter_11/Section_11_4_Open_Addressing.lean; CLRSLean/Chapter_11/Section_11_5_Perfect_Hashing.lean; CLRSLean/Status.lean,Chapter 11 proves SUHA successful and unsuccessful search costs universal hashing collision and search-cost bounds an affine universal family open-addressing expected-probe bounds and two-level perfect hashing; only low-level operational accounting remains.
+12,Binary Search Trees,main-proof-complete-for-correctness,12.1,40,40,0,Functional BST zipper parent-navigation and the represented imperative pointer-heap TRANSPLANT/insert refinements are complete,Search; min/max; insertion; complete successor/predecessor specifications; functional delete membership and ordering; search and neighbor queries after updates; faithful zipper reconstruction; iterative search equivalence; transplant ordering preservation; deletion-via-transplant equivalence; parent-ascent successor/predecessor equivalence; imperative pointer-heap node/store model; heap-to-tree abstraction faithfulness; pointer frame rules; in-place TRANSPLANT refinement; pointer TREE-INSERT leaf-attachment refinement,None; pointer-level in-place delete and explicit RAM costs are optional low-level refinements,CLRSLean/Chapter_12.lean; CLRSLean/Chapter_12/Section_12_1_Binary_Search_Trees.lean; CLRSLean/Status.lean; Tests/Chapter_12_Interface.lean,The represented mathematical and refinement interfaces are complete; lower-level pointer deletion and RAM accounting do not block the correctness milestone.
+13,Red-Black Trees,main-proof-complete-for-correctness,13.1,39,39,0,Executable insertion and deletion with exact membership correctness red-black shape preservation and the logarithmic-height theorem are proved,Rotation membership; repaint membership; no-red-red; black-height; local red-black shape preservation; insertion-fixup certificates; executable insert and redBlackShape_insert; height_log_bound (Lemma 13.1); executable baldL/baldR/splitMin/join/del/delete; inTree_delete_iff; local delete-fixup membership and shape certificates; deficit-absorbing rebalancer certificates baldL_shape and baldR_shape; splitMin_invariant; del_invariant; redBlackShape_delete,None; pointer-level mutation and RAM cost semantics are optional refinements,CLRSLean/Chapter_13.lean; CLRSLean/Chapter_13/Section_13_1_Red_Black_Trees.lean; CLRSLean/Status.lean,Deletion preserves red-black shape via the splitMin/join doubly-black rebalancing pipeline (redBlackShape_delete); the height theorem is complete.
+14,Augmenting Data Structures,main-proof-complete-for-correctness,14.1;14.3,67,67,0,Order-statistic and interval-tree augmentation layers represented; the size invariant and generic AugmentedRBTree deletion pipeline are proved,Size augmentation invariant; size recomputation; key preservation; size/rank-preserving local rotations; augmented rank-select correctness; generic rotation-invariant augmentation theorem (CLRS 14.1); interval overlap semantics and search specification; OSRBTree wellSized_insert and wellSized_delete with toRB refinement; generic AugmentedRBTree executable insertion and deletion with wellAugmented_insert and wellAugmented_delete for any augmentation; repaintRoot/rootBlack/baldL/baldR/splitMin/join/del/delete pipeline preserving WellAugmented; size and max-high instances recovered,None; pointer-level mutation and RAM cost semantics,CLRSLean/Chapter_14.lean; CLRSLean/Chapter_14/Section_14_1_Order_Statistic_Trees.lean; CLRSLean/Chapter_14/Section_14_3_Interval_Trees.lean; CLRSLean/Status.lean,The generic AugmentedRBTree deletion pipeline mirrors OSRBTree with wellAugmented_delete for any Augmentation; both order-statistic and interval-tree instances are now fully proved through both insertion and deletion.
+15,Dynamic Programming,selected-section-complete,15.1;15.2;15.4;15.5,76,76,0,The four represented dynamic-programming examples have mathematical optimality and executable recurrence/reconstruction layers,Bellman rod-cutting recurrence and bottom-up value; mutable-Array bottom-up rod-cutting refinement; matrix-chain lower bound computable optimum split reconstruction and correctness; LCS certificate table recurrence executable length/reconstruction and correctness; optimal-BST recurrence bottom-up optimum plan reconstruction and correctness,None; further mutable-array implementations and explicit RAM costs are optional refinements,CLRSLean/Chapter_15.lean; CLRSLean/Chapter_15/Section_15_1_Rod_Cutting.lean; CLRSLean/Chapter_15/Section_15_2_Matrix_Chain_Multiplication.lean; CLRSLean/Chapter_15/Section_15_4_Longest_Common_Subsequence.lean; CLRSLean/Chapter_15/Section_15_5_Optimal_Binary_Search_Trees.lean; CLRSLean/Status.lean,The represented examples are complete at the mathematical and pure executable layers; mutable refinements do not block their milestone.
+16,Greedy Algorithms,main-proof-complete,16.1;16.2;16.3;16.4;16.5,32,32,0,Activity selection greedy meta-theorems Huffman weighted-matroid greedy optimality and task scheduling are complete,Activity-selection greedy optimality; Huffman V2 frequency-table optimality and minimum-cost wrappers; weighted-matroid GREEDY optimality (Theorems 16.6/16.7/16.10) built on Mathlib matroids; GreedyProblem meta-theorem and gsolve_optimal (CLRS §16.2 greedy-choice property and optimal substructure); scheduling-matroid construction (Theorem 16.13) and min-penalty schedule via greedy optimality,None; exercises are tracked separately from the chapter milestone,CLRSLean/Chapter_16.lean; CLRSLean/Chapter_16/Section_16_2_Greedy_Meta.lean; CLRSLean/Chapter_16/Section_16_4_Matroids.lean; CLRSLean/Chapter_16/Section_16_5_Task_Scheduling.lean; CLRSLean/Status.lean,The represented Sections 16.1-16.5 cover the core chapter theorem groups; exercises remain an optional second track.
+17,Amortized Analysis,selected-section-complete,17.1;17.2;17.4,66,66,0,The represented aggregate accounting potential stack/counter and dynamic-table analyses are complete,Aggregate/accounting/potential telescoping; MULTIPOP; executable binary-counter one-step and multi-step trace bounds; dynamic-table potential nonnegativity; concrete amortized-cost unfoldings and transition/capacity wrappers,None; mutable-array copying allocator constants and sharper RAM models are optional refinements,CLRSLean/Chapter_17.lean; CLRSLean/Chapter_17/Section_17_1_Amortized_Framework.lean; CLRSLean/Chapter_17/Section_17_1_Amortized_Framework/Section_17_2_Stack_And_Counter.lean; CLRSLean/Chapter_17/Section_17_4_Dynamic_Tables.lean; Tests/Chapter_17_Interface.lean,No sorry/admit/axiom in Chapter_17; the size-level represented theorem stack is complete.
+18,B-Trees,partial,18.1;18.2;18.3,62,62,1,First-pass mathematical B-tree model represented,Search correctness direct base search success/failure wrappers minimum-key height expression base positivity recurrence and height monotonicity split-child direct validity membership/search preservation direct split old-key and failed-membership corollaries insertion/deletion membership Prop-level deletion membership/search success and direct wrappers direct insertion/deletion validity short-name wrappers equality-key update-query wrappers successful and unsuccessful search-after-update specs membership-driven search-after-update wrappers and direct inserted/deleted-key old-key query preservation old failed-search preservation wrappers failed-membership corollaries and direct failed-membership preservation wrappers,Full occupancy separator and same-depth invariant stack plus node-level deletion repair,CLRSLean/Chapter_18.lean; Tests/Chapter_18_Interface.lean,Disk-page pointer mutation and I/O/RAM semantics are optional low-level refinements and are not part of the remaining core group.
+19,Fibonacci Heaps,partial,19.1;19.4,112,112,1,Abstract finite-set Fibonacci heap model plus concrete rooted-tree degree bound represented,Make-heap valid make-heap empty-minimum potential-zero potential-nonnegative minimum membership lower-bound and empty-result wrappers direct minimum/extract-min empty-result and nonempty-result wrappers insert valid and insert-membership insert-self insert-old insert-failed-membership insert-minimum direct membership/lower-bound wrappers insert-empty-minimum union valid and union-membership union-left union-right union-failed-membership union-minimum direct membership/lower-bound wrappers union-empty-minimum union-nonempty-minimum extract-min valid and extract-min-membership extract-min-removed extract-min-old-key-preservation extract-min-failed-membership empty-extract-min nonempty-extract-min remaining-minimum direct membership/lower-bound wrappers remaining-empty-minimum remaining-nonempty-minimum decrease-key valid and decrease-key-membership decrease-key-new decrease-key-replaced-key query wrappers decrease-key-old-key-preservation decrease-key-failed-membership decrease-key-minimum direct membership/lower-bound wrappers decrease-key-empty-minimum delete valid and delete-membership delete-removed delete-old-key-preservation delete-failed-membership direct failed-membership preservation wrappers delete-minimum direct membership/lower-bound wrappers delete-empty-minimum delete-nonempty-minimum potential telescoping Fibonacci lower-bound recurrence positivity monotonicity two-step doubling even-index and half-index power-of-two lower bounds conditional degree-to-log wrappers and conservative degree budget concrete FTree rooted-tree model degree and size Lemma-19.1 marked-tree Wellformed invariant true subtree-size theorem size>=F(d+2) golden-ratio phi^d<=F(d+2) and phi^d<=size logarithmic maximum-degree bounds log_phi n floor-log_phi n and 2*log2 n budget CONSOLIDATE link invariant-maintenance wellformed-append-child link and link-degree extremal minTree tightness witness size=F(d+2),Pointer forest circular root lists executable CONSOLIDATE and cascading-cut procedures duplicate handles and amortized O(log n)/O(1) cost accounting over the potential function,CLRSLean/Chapter_19.lean; Tests/Chapter_19_Interface.lean,"Potential theorem instantiates Chapter 17; Section 19.4 seals the true Fibonacci subtree-size logarithmic degree bound D(n) <= floor(log_phi n) on an abstract wellformed tree model, shown tight by the extremal minTree family."
+20,van Emde Boas Trees,main-proof-complete-for-correctness,20.1;20.2;20.3,200,200,0,All seven operations of the recursive cached-min/max model are proved correct with constant cached extrema and control-flow-aware O(log log u) bounds,High-low-index arithmetic and the finite-set specification layer plus recursive tower-universe VEBTree and VEBTreeMM semantics; cached minimum and maximum correctness; lazy-min insert invariant preservation and exact Finset.insert refinement; strong recursive successor least-greater and predecessor greatest-less specifications; exact recursive delete Finset.erase refinement; branch-faithful member insert successor predecessor and delete cost bounds; separate delete work and depth bounds; all-operation O(log log u) packaging,Concrete pointer/array storage and hardware-level RAM constants only,CLRSLean/Chapter_20.lean; CLRSLean/Chapter_20/Section_20_3_Recursive_VEB.lean; Tests/Chapter_20_Interface.lean; Tests/Chapter_20_Axioms.lean,The recursive mathematical completion boundary is sealed; concrete pointer/array allocation and hardware-level RAM timing remain a separate implementation refinement.
+21,Data Structures for Disjoint Sets,main-proof-complete,21.1;21.2;21.3;21.4,84,84,0,"The represented Chapter 21 stack is complete: abstract and executable correctness, real Batteries traversal costs, reachable rank mass, and the concrete O((m+n) alpha(n)) amortized bound are proved",Partition equivalence and exact merge semantics; operation-trace monotonicity; singleton linked lists; weighted-union exact refinement; representative invariant; per-rewrite size doubling; per-element log2 and aggregate n log2 n rewrite bounds; singleton Batteries forests; path-compressing find partition preservation and representative correctness; union-by-rank exact merge refinement; Boolean equivalence-query correctness; exact parent-edge traversal counter; conserved root-mass budget through find/link/union; costed execution erasure and abstract run refinement; per-find and per-union log2 bounds; whole-run m * (2 log2 n + 3) intermediate bound; inverse-Ackermann definition and minimality; Ackermann level/index node potential; path-compression potential monotonicity; equal-rank link pair bound and global link increase at most two; released/boundary/unpleasant path classification; per-find and per-union inverse-Ackermann amortized bounds; whole-run 9 * (m+n) * alpha(n) bound; 18 * m * alpha(n) corollary when n <= m; Chapter 23 union-find connectivity and cycle-test bridge,No remaining core Chapter 21 group; lower-level mutable-array/RAM constants and a stateful Chapter 23 Kruskal scan are separate refinements,CLRSLean/Chapter_21.lean; CLRSLean/Chapter_21/Section_21_1_Disjoint_Set_Operations.lean; CLRSLean/Chapter_21/Section_21_2_Linked_List_Representation.lean; CLRSLean/Chapter_21/Section_21_3_Disjoint_Set_Forests.lean; CLRSLean/Chapter_21/Section_21_4_Analysis.lean; CLRSLean/Chapter_21/Section_21_4_Analysis/CostedExecution.lean; CLRSLean/Chapter_21/Section_21_4_Analysis/InverseAckermann.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim/S1_UnionFindBridge.lean; Tests/Chapter_21_Interface.lean; Tests/Chapter_23_UnionFind_Interface.lean; docs/proof-audits/chapter-21-closure-2026-07-10.md,No sorry/admit/axiom in the represented chapter; the concrete cost model counts actual parent traversals plus constant operation overhead and proves the advertised inverse-Ackermann bound.
+22,Elementary Graph Algorithms,main-proof-complete-for-correctness,22.1;22.2;22.3;22.4;22.5,47,47,0,"Main functional correctness is complete: CLRS FIFO BFS exactly characterizes reachability and returns shortest distances with a rooted predecessor tree, DFS includes the white-path theorem, timestamp parenthesis theorem, parent-forest ancestor/interval characterization, unique edge classification, and SCC timestamp theory, Kahn and CLRS DFS finish-time topological sorts are correct for DAGs, and Kosaraju returns an SCC partition; only explicit algorithm-cost refinements remain","Finite directed graph with adjacency function; walk/path/cycle definitions; reachability; reflexivity/transitivity/adjacency lemmas; connected components; undirected graph symmetry; fuelled BFS soundness and completeness; BFS closure and termination measure; exact-edge ReachableIn and IsShortestDistance; labelled BFSState with distance and parent; bfsState projection to the reachability BFS; FIFO distance invariant; bfsState_distance_eq_some_iff; bfsState parent edge, unit-level, root-path, coverage, and acyclicity facts; bfsState_isBFSPredecessorTree; bfsState_correct; functional DFS with colors, discovery/finish times, and parents; global DFS color/timestamp invariants; finite white reachability; dfsVisit_blackens_iff_whiteReachable; ParenthesisInvariant; dfs_parenthesis; dfs_parenthesis_cases; dfs_intervals_not_cross; discovery-state and timestamp bridges; ancestor reachability; dfs_parent_discovery_lt; intervalNestedInside_dfs_implies_ancestor; intervalNestedInside_dfs_iff_ancestor; IsDFSTreeEdge; IsDFSBackEdge; IsDFSForwardEdge; IsDFSCrossEdge; dfs_edge_classification_unique; dfs_tree_or_forward_edge_iff_timestamps; dfs_back_edge_iff_timestamps; dfs_cross_edge_iff_timestamps; maximum-finish and first-discovery facts; SCC finish-time ordering; DAG predicate; indegree; Kahn topological sort correctness; isDAG_no_dfs_back_edge; dfs_finish_time_decreases_on_dag_edge; DFS finish-time order permutation and pairwise sorting; dfsTopologicalSort_isTopologicalOrder; transpose graph; strong connectivity and SCC predicates; collecting DFS; Kosaraju order properties; Kosaraju component strong connectivity and maximality; pairwise disjointness; coverage; unique membership; kosarajuComponents_isSCCPartition",No remaining core correctness group; explicit work and RAM-cost refinements,CLRSLean/Chapter_22.lean; CLRSLean/Chapter_22/Section_22_1_Representing_Graphs.lean; CLRSLean/Chapter_22/Section_22_2_BFS.lean; CLRSLean/Chapter_22/Section_22_3_DFS.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S1_WhitePath.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S2_Intervals.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S3_Bridge.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S4_SCC.lean; CLRSLean/Chapter_22/Section_22_3_DFS/S5_EdgeClassification.lean; CLRSLean/Chapter_22/Section_22_4_Topological_Sort.lean; CLRSLean/Chapter_22/Section_22_5_Strongly_Connected_Components.lean; CLRSLean/Chapter_22/Section_22_5_Strongly_Connected_Components/MergeSortCongr.lean; CLRSLean/Status.lean; Tests/Chapter_22_Interface.lean; Tests/Chapter_22_Closure.lean; docs/proof-audits/chapter-22-closure-2026-07-10.md,"DFS parenthesis, parent-forest ancestor/interval characterization, and unique edge classification are fully proved through dfs_parenthesis, intervalNestedInside_dfs_iff_ancestor, and dfs_edge_classification_unique; Kosaraju correctness is fully proved through scc_finish_time_order, scc_finish_order, kosarajuComponent_scc_core, and kosarajuComponents_isSCCPartition; Chapter 22 main functional correctness is formally sealed by the 2026-07-10 closure audit; explicit work and RAM-cost refinements remain"
+23,Minimum Spanning Trees,main-proof-complete-for-correctness,23.1;23.2,52,52,0,Mathematical correctness and functional implementation refinements are complete: cut property canonical exchange sorted and stateful Kruskal plus executable indexed-queue Prim,Finite edge-labelled graph and spanning-tree specification; safe-edge and cut-property theorem; canonical unique tree path and automatic exchange; complete sorted Kruskal MST theorem; real Chapter 21 costed union-find threaded through every Kruskal edge; connectivity invariant and mathematical-selection refinement; inverse-Ackermann scan bound and complete O(E log E) work composition; Prim key parent decrease-key and extract-min queue; concrete frontier provider; executable run refinement to PrimTrace; binary-heap O(E log V) operation-count theorem; complete Prim MST theorem,No remaining core mathematical or functional algorithm group; concrete Batteries binary-heap array refinement and mutable/RAM write semantics remain separate low-level refinements,CLRSLean/Chapter_23.lean; CLRSLean/Chapter_23/Section_23_1_Growing_Minimum_Spanning_Trees.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim/S1_UnionFindBridge.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim/S2_StatefulKruskal.lean; CLRSLean/Chapter_23/Section_23_2_Kruskal_And_Prim/S3_ExecutablePrim.lean; CLRSLean/Status.lean; Tests/Chapter_23_Interface.lean; Tests/Chapter_23_Closure.lean; Tests/Chapter_23_UnionFind_Interface.lean; Tests/Chapter_23_Implementation_Interface.lean; docs/proof-audits/chapter-23-closure-2026-07-11.md,The correctness boundary remains sealed and now has proved executable semantic and algorithm-level cost refinements.
+24,Single-Source Shortest Paths,selected-section-complete,24.1;24.2;24.3;24.4,22,22,0,Bellman-Ford DAG SSSP Dijkstra greedy correctness end-to-end executable loop and difference constraints are complete,Finite weighted directed-graph model; walks and walk weights; Bellman-Ford relaxation correctness and O(VE) work; DAG-SHORTEST-PATHS correctness and O(V+E) work; nonnegative-weight Dijkstra greedy invariant and O(E log V) abstract work; DijkstraState dijkstraInit dijkstraInit_invariant dijkstraStep DijkstraInvariant dijkstraStep_invariant dijkstraLoop dijkstraLoop_invariant dijkstraLoop_finish dijkstraLoop_correct; difference-constraint feasibility iff no negative cycle,None; per-edge relaxation ordering and mutable/RAM cost refinement,CLRSLean/Chapter_24.lean; CLRSLean/Chapter_24/Section_24_1_Bellman_Ford.lean; CLRSLean/Chapter_24/Section_24_2_SSSP_In_DAGs.lean; CLRSLean/Chapter_24/Section_24_3_Dijkstra.lean; CLRSLean/Chapter_24/Section_24_4_Difference_Constraints.lean,The Dijkstra initialization gap is closed: dijkstraInit pre-settles the source and pre-relaxes outgoing edges so DijkstraInvariant holds initially; dijkstraLoop_invariant lifts it through the loop; dijkstraLoop_correct proves the final distance map equals δ.
+25,All-Pairs Shortest Paths,partial,25.1;25.2;25.3,22,22,2,Faster-APSP min-plus model Lemmas 25.1/25.2 stabilization and correctness; Floyd-Warshall D/floydWarshall/fwStep/Pi/floydWarshallPi/fwReconstructPath (walk validity and weight equality); Johnson augmented graph; reweightedGraph; reweightedWalkWeight_eq; reweightedWeight_nonneg; reweighted_isShortestDist; noNegCycle_johnsonAugmentedGraph; johnsonPotential; johnsonPotential_triangle; johnsonDist_isShortestDist,Transitive closure (Section 25.2 variant); explicit O(n³ log n) work-count refinement for repeated squaring,"Sections 25.1, 25.2, and 25.3 are all core-complete. Section 25.1 proves FASTER-APSP correctness. Section 25.2 proves Floyd-Warshall correctness (Theorems 25.7, 25.8, 25.3), predecessor matrix Pi, path reconstruction (walk validity AND weight equality), and negative-cycle detection. Section 25.3 constructs the Bellman-Ford potential, proves the triangle inequality, and proves end-to-end Johnson correctness (CLRS Theorem 25.5). Transitive closure is a separate variant not in the core algorithm.",CLRSLean/Chapter_25.lean; CLRSLean/Chapter_25/Section_25_1_All_Pairs_Model.lean; CLRSLean/Chapter_25/Section_25_2_Floyd_Warshall.lean; CLRSLean/Chapter_25/Section_25_3_Johnsons_Algorithm.lean,"Section 25.1 is complete under no negative cycles. Section 25.2 has Floyd-Warshall correctness (Theorems 25.7, 25.8, 25.3), predecessor matrix Pi, path reconstruction (walk validity), and negative-cycle detection. Path-reconstruction weight equality is deferred. Section 25.3 proves the reweighting algebra including shortest-path preservation under reweighting."
+26,Maximum Flow,partial,26.1;26.2;26.6,9,9,3,The flow model generic no-augmenting-path maximality easy MFMC direction and Edmonds-Karp monotonic-distance lemma are proved,FlowNetwork model; feasible flow; flow value; Lemma 26.5 net-flow-across-cut; residual network augmenting path; generic Ford-Fulkerson maximality from no-augmenting-path; easy MFMC direction cut-capacity-implies-maximal; residual path length; shortest-path distance; Lemma 26.7 monotonic distance,Full Max-Flow Min-Cut converse/equivalence; executable BFS augmentation loop and O(VE^2) theorem; Section 26.3 bipartite-matching reduction and correctness,CLRSLean/Chapter_26.lean; CLRSLean/Chapter_26/Section_26_1_Flow_Networks.lean; CLRSLean/Chapter_26/Section_26_2_Edmonds_Karp.lean; CLRSLean/Chapter_26/Section_26_6_MaxFlow_MinCut.lean,"The represented files prove the flow foundation the generic Ford-Fulkerson maximality direction Lemma 26.7 and one MFMC direction. Section 26.3 is not present on main, and neither the MFMC converse nor the executable Edmonds-Karp complexity theorem is proved."
+27,Multithreaded Algorithms,partial,27.1;27.2,28,28,1,Computation-DAG and spawn-tree model with honest span and the four textbook parallel-algorithm work/span recurrences are represented and proved at the power-of-two boundary,Forward-edge computation DAG with DP longest-path span and span-le-work; spawn/sync tree unit-overhead model with span-le-work; balanced parallel-loop tree exact work and span with logarithmic depth lower bound; P-MATMUL work Theta(n^3) and span Theta(log n) pow2 closed forms plus all-input upper bounds; P-MERGE work Theta(n) and span Theta(log^2 n) pow2 closed forms; P-MERGE-SORT work Theta(n log n) and span Theta(log^3 n) pow2 closed forms; parallel Strassen work Theta(n^(log2 7)) and span Theta(log n) pow2 closed forms,Greedy-scheduler bound (Theorem 27.1/27.2); all-input Theta-bounds for the merge-based costs; executable P-MERGE and P-MERGE-SORT refinements,CLRSLean/Chapter_27.lean; CLRSLean/Chapter_27/Section_27_1_Multithreading_Model.lean; CLRSLean/Chapter_27/Section_27_2_4_Algorithms.lean; Tests/Chapter_27_Interface.lean; CLRSLean/Status.lean,No sorry/admit/axiom in Chapter_27; asymptotic claims are exact closed forms on powers of two with all-input upper bounds where proved.
+28,Matrix Operations,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_28 module exists.
+29,Linear Programming,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_29 module exists.
+30,Polynomials and the FFT,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_30 module exists.
+31,Number-Theoretic Algorithms,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_31 module exists.
+32,String Matching,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_32 module exists.
+33,Computational Geometry,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_33 module exists.
+34,NP-Completeness,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_34 module exists.
+35,Approximation Algorithms,not-started,None,0,0,1,Not represented,No tracked theorem names yet,Whole chapter theorem inventory and formalization pending,CLRSLean file tree,No Chapter_35 module exists.