Move the Refactors roadmap to Completed

LMLRoadmaps/Refactors/README.md → 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.

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

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.

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