[RemyDegenne]

Archives the Refactors roadmap under Completed/Refactors/, so that workers no longer draw it as an area.

Merge after LeanMachineLearning/LMLExplore#74. That PR restores the roadmap's last completion check, which LMLExplore#68 broke after the roadmap's own items had merged.

Completion against the README

Each item was checked on LMLExplore main (4cc3a51):

Item	Status	Where
0.1 FTRL on normed spaces, losses in the dual	done	OnlineLearning/FTRL.lean (IsFTRLPlay, sum_apply_sub_le_ftrl, ftrl_regret_le, ftrl_regret_le_of_strongConvexOn with the operator norm, exists_ftrl, ftrl_regret_le_sqrt_of_closedBall with innerSL)
0.2 Exponential families with a statistic	done	Probability/Distributions/ExponentialFamily/ (expFamily, expFamilyMeans, natParam, expFamilyDiv); no natExpFamily… remains
0.3 Chernoff under domination	done	ExponentialFamily/Chernoff.lean (MGFDominatedAbove/Below); ExponentialFamily/Bernoulli.lean (expFamilyDiv_bernoulliMeasure_sigmoid); measureReal_sum_ge_le_exp_klBerReal derived from the family bound, boundary case direct
0.4 Run-to-stream transfer, shared and joint	done	SequentialLearning/SumRewards.lean (measure_exists_pullCount_sumRewards_pi_le and its horizon form)
1.1 Wald's identities in one file	done	SequentialLearning/Wald.lean
1.2 Probability vectors through simplex	done	Bandits/WeightAlgorithm.lean, MeasureTheory/Measure/Weighted.lean
1.3 General concentration in Probability/	done	Probability/Moments/SubGaussian/Sum.lean (the README named SubGaussianSum.lean), Analysis/SpecialFunctions/Log/InvMulLogSq.lean

Completion checks: the first three hold on main. The fourth ("no file under Bandits/ is imported by Identification/ for the reward stream transfer") holds once LMLExplore#74 merges. After it, Identification/ imports only Bandits/Instances.lean, for the Gaussian and Bernoulli arm laws.

Changes

• LMLRoadmaps/Refactors/ moved to Completed/Refactors/, with its relative links updated. The Lean module becomes Completed.Refactors.Suggested, still built by the Completed library.
• Completed/.gitkeep removed.
• README.md: a "Completed roadmaps" section listing it.
• The links to it from the Bandits and Identification READMEs point to the new location.

lake build passes locally.

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMTTvboLE9rrbLUFss1