From 386be45a4b103e0c0a7e86ed4060385e5372aaad Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Mon, 2 Nov 2026 13:14:41 +0100
Subject: [PATCH] Move the Refactors roadmap to Completed

Every item of the Refactors roadmap is merged in LMLExplore. Archive it
under Completed/, list it in the README, and update the links to it
from the Bandits and Identification roadmaps.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0196ftMTTvboLE9rrbLUFss1
---
 Completed/.gitkeep                                  | 0
 {LMLRoadmaps => Completed}/Refactors/README.md      | 4 ++--
 {LMLRoadmaps => Completed}/Refactors/Suggested.lean | 0
 {LMLRoadmaps => Completed}/Refactors/metadata.toml  | 0
 LMLRoadmaps/Bandits/README.md                       | 2 +-
 LMLRoadmaps/Identification/README.md                | 2 +-
 README.md                                           | 7 +++++++
 7 files changed, 11 insertions(+), 4 deletions(-)
 delete mode 100644 Completed/.gitkeep
 rename {LMLRoadmaps => Completed}/Refactors/README.md (98%)
 rename {LMLRoadmaps => Completed}/Refactors/Suggested.lean (100%)
 rename {LMLRoadmaps => Completed}/Refactors/metadata.toml (100%)

diff --git a/Completed/.gitkeep b/Completed/.gitkeep
deleted file mode 100644
index e69de29..0000000
diff --git a/LMLRoadmaps/Refactors/README.md b/Completed/Refactors/README.md
similarity index 98%
rename from LMLRoadmaps/Refactors/README.md
rename to Completed/Refactors/README.md
index 10712d5..33c9431 100644
--- a/LMLRoadmaps/Refactors/README.md
+++ b/Completed/Refactors/README.md
@@ -22,8 +22,8 @@ In scope:
 - Wald's identities, probability vectors on finite types, and the generic parts of
   `LMLExplore/Bandits/Concentration.lean`.
 
-Relation to the other roadmaps. The [Bandits](../Bandits/README.md) and
-[Identification](../Identification/README.md) roadmaps specify the mathematics these developments
+Relation to the other roadmaps. The [Bandits](../../LMLRoadmaps/Bandits/README.md) and
+[Identification](../../LMLRoadmaps/Identification/README.md) roadmaps specify the mathematics these developments
 contain, in the generality of the targets here (Bandits Layer 6 for online linear optimization,
 Identification Layer 1.2 for exponential families); this roadmap restates the merged code in that
 generality and moves it where its users are. It adds no target of those roadmaps.
diff --git a/LMLRoadmaps/Refactors/Suggested.lean b/Completed/Refactors/Suggested.lean
similarity index 100%
rename from LMLRoadmaps/Refactors/Suggested.lean
rename to Completed/Refactors/Suggested.lean
diff --git a/LMLRoadmaps/Refactors/metadata.toml b/Completed/Refactors/metadata.toml
similarity index 100%
rename from LMLRoadmaps/Refactors/metadata.toml
rename to Completed/Refactors/metadata.toml
diff --git a/LMLRoadmaps/Bandits/README.md b/LMLRoadmaps/Bandits/README.md
index 90b9718..57e557f 100644
--- a/LMLRoadmaps/Bandits/README.md
+++ b/LMLRoadmaps/Bandits/README.md
@@ -335,7 +335,7 @@ against `u` after `n` rounds is $\sum_{t<n}y_t(a_t-u)$. Strong convexity refers
 (Mathlib's `StrongConvexOn`), and the norm of a loss is its operator norm, the dual norm. Losses
 are minimized. Statements whose proofs do not use the dimension, such as the FTRL bounds of item 3,
 are stated without it. The merged FTRL development of LMLExplore is restated in this generality by
-the [Refactors](../Refactors/README.md) roadmap, Layer 0.1.
+the [Refactors](../../Completed/Refactors/README.md) roadmap, Layer 0.1.
 
 1. **Legendre functions.** For a convex function $F$ with domain $D$ (represent it as `F : E → ℝ`
    with a convex set `D`, or as `E → EReal`; choose one representation and give conversions to
diff --git a/LMLRoadmaps/Identification/README.md b/LMLRoadmaps/Identification/README.md
index dc8f4af..9670f19 100644
--- a/LMLRoadmaps/Identification/README.md
+++ b/LMLRoadmaps/Identification/README.md
@@ -250,7 +250,7 @@ forms above, and that development may be adapted to them.
    - Prove the Cramér–Chernoff bound
      $P\big(\sum_{i<n}T(Y_i)\ge nx\big)\le\exp(-n\,d(x,\mu))$ for independent observations
      $Y_i$ of law $\rho_{\eta(\mu)}$ and $x\ge\mu$ (and the lower tail), in the form of the
-     [Refactors](../Refactors/README.md) roadmap, Layer 0.3: for real random variables dominated
+     [Refactors](../../Completed/Refactors/README.md) roadmap, Layer 0.3: for real random variables dominated
      by the member of mean $\mu$. That form contains the Bandits roadmap's Layer 1.4 bound.
    - Prove the sub-Gaussian comparison: $d(\mu,\mu')\ge(\mu-\mu')^2/(2\sigma^2)$ when the family has
      variance at most $\sigma^2$ on the segment.
diff --git a/README.md b/README.md
index 9bd0a8e..183b56d 100644
--- a/README.md
+++ b/README.md
@@ -20,6 +20,13 @@ propose or review one.
 
 - [Bandit algorithms and their regret](LMLRoadmaps/Bandits/README.md)
 
+## Completed roadmaps
+
+Roadmaps the maintainers have declared complete, a judgment against the roadmap's `README.md`, are
+archived under `Completed/`. Their Lean files stay checked against the current LMLExplore pin.
+
+- [Refactors toward the generality of later layers](Completed/Refactors/README.md)
+
 ## Writing a roadmap
 
 A roadmap is a specification for material we want in LMLExplore, written so that an AI contributor