[RemyDegenne]

This PR derives the sample complexity of Track-and-Stop with C-tracking from the plug-in GLRT reduction of Generalization 1.10 and deletes the private mul_le_glr_plugInCost_of_mem_thickening. It also states once, as a lemma, the argument over the rounds that the D-tracking and C-tracking proofs both repeated. This is Generalization 1.11 ("Track-and-Stop with C-tracking from the reduction"): "Derive eventually_expectedStoppingTime_cTrackAndStop_le and eventually_expectedStoppingTime_cTrackAndStop_le_of_charTime_lt from the reduction of target 1.10, with their constants as in the Conventions, and delete the private mul_le_glr_plugInCost_of_mem_thickening and the argument over the rounds that the two proofs of TrackAndStop.lean share." Target 1.10 landed in #374.

Roadmap: Generalization

All changes are in Identification/TrackAndStop.lean, and no public statement changes:

• IdentTask.eventually_expectedStoppingTime_cTrackAndStop_le is now IdentTask.eventually_expectedStoppingTime_glrt_plugInCost_le_of_isBigO with W = C. The rate κ, the thickening argument and the call to eventually_expectedStoppingTime_glrt_le are gone from the proof, which now only shows that C-tracking's proportions of pulls converge to C on good events. Its constant stays (⨅ v ∈ C, task.altCost μ v i)⁻¹ < c, and _of_charTime_lt (with task.charTime μ < c) and the union-bound and almost-sure corollaries still follow from it unchanged. Those are the constants the Conventions require.
• The private exists_tsum_measure_compl_ne_top_forall_ge_empMean'_mem is the round argument the two proofs shared. It takes a box of vectors of means around μ inside a neighbourhood W, uses forced exploration to show the empirical means stay in the box from round t₀ T on, and builds events E T with ∑ P((E T)ᶜ) < ∞ on which an almost-sure property G holds (the tracking guarantee) and the empirical means lie in W at every round k ≥ t₀ T. The forced-exploration bound is a hypothesis, so D-tracking passes DTracking.tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top and C-tracking passes CTracking.tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top. eventually_expectedStoppingTime_trackAndStop_le (D-tracking) now uses it as well.
• The private pullCount_div_mem_thickening replaces mul_le_glr_plugInCost_of_mem_thickening. It keeps only the step about proportions of pulls: if the targets are allocations ε-close to the convex set C from round t₀ on, and the pull counts follow the cumulated targets up to e, then N(T) / T is η-close to C when e + (1 + B) t₀ + ε T < η T [DK19, Lemma 6]. It no longer mentions the GLR statistic, the task or the recommendation, matching the D-tracking step dist_pullCount_div_lt from feat: one sample-complexity reduction for the plug-in GLRT, and Track-and-Stop with D-tracking from it #374.

Removed: the private mul_le_glr_plugInCost_of_mem_thickening. No public declaration is removed or renamed. The file shrinks by 36 lines (129 added, 165 removed).

What remains: nothing for Generalization 1.11. Both Track-and-Stop sample-complexity theorems now come from the one reduction, which is the Completion check "the D- and C-tracking sample-complexity theorems are derived from one reduction". Target 1.11 unblocks Identification 5.2.

Reuse: the proofs use the existing IdentTask.eventually_expectedStoppingTime_glrt_plugInCost_le_of_isBigO, Convex.exists_mem_norm_sum_sub_smul_le (Analysis/Convex/Normed.lean), exists_pi_Icc_subset_of_mem_nhds, Mathlib's Metric.hasBasis_nhdsSet_thickening (for compact C, the thickenings are a basis of 𝓝ˢ C) and the forced-exploration and tracking lemmas of DTracking.lean and CTracking.lean. The two new private lemmas are restatements of steps already on main, and I grepped LMLExplore/ and Mathlib for an existing "good events from forced exploration" lemma and found none. The statements follow [GK16, proof of Theorem 14] and [DK19, Lemma 6 and Theorem 7], which the docstrings cite.

Verification (local checks only; CI verifies the pushed PR): scope: scoped: against c4a9e04dde775bf5a60d932b093c88ab01b9246a; whole-library lake build --iofail green (8563 jobs); local-axioms: checked 1 changed module(s), 47 declaration(s); 0 violation(s); module-system, header-style and the environment lint (14 environment linters, 3 documentation checks) pass on the changed module.

🤖 Prepared with Claude Code

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	Both public Track-and-Stop sample-complexity statements are unchanged, and the C-tracking proof now goes through the plug-in reduction with W = C, using an h_conv argument of the required shape. The two new private lemmas are faithful, non-vacuous restatements of [GK16, Thm 14] and [DK19, Lemma 6] that leave no conclusion in their assumptions.
✅	reuse	approved	claude/claude-opus-5-5	The new private lemmas reuse existing results (the GLRT plug-in reduction, the D- and C-tracking forced-exploration bounds, exists_pi_Icc_subset_of_mem_nhds, Metric.hasBasis_nhdsSet_thickening) and replace the duplicated round argument and the deleted mul_le_glr_plugInCost_of_mem_thickening rather than adding parallel API. I found no existing declaration that builds these good events or that directly replaces pullCount_div_mem_thickening.
✅	scope	approved	claude/claude-opus-5-5	Refactor of merged Track-and-Stop proofs that does exactly what roadmap target Generalization 1.11 asks for: C-tracking now comes from the 1.10 reduction, mul_le_glr_plugInCost_of_mem_thickening is deleted and the shared round argument becomes one lemma. It is a single topic in a single file, with no new public mathematics.
✅	attribution	approved	claude/claude-opus-5-5	The new private lemmas cite [GK16, proof of Theorem 14 / Lemma 19] and [DK19, Lemma 6 and Theorem 7], both of which are in the file's reference list (TrackAndStop.lean:144,146), and the docstring names the reused Convex.exists_mem_norm_sum_sub_smul_le. No uncredited source is followed, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	No public declaration is added, removed, or restated; the two new lemmas are proof helpers specific to this file, kept private and used only by the D- and C-tracking proofs in TrackAndStop.lean, and mul_le_glr_plugInCost_of_mem_thickening is deleted with no compatibility surface left behind.
✅	generality	approved	claude/claude-opus-5-5	The shared round lemma's parameters (h_forced and G) each take a different value at the D-tracking and C-tracking call sites, and pullCount_div_mem_thickening is at the same level as its D-tracking sibling dist_pullCount_div_lt. The C-tracking theorem now comes from the general reduction instead of repeating it.
✅	placement	approved	claude/claude-opus-5-5	Both new private lemmas sit in Identification/TrackAndStop.lean next to the D- and C-tracking sample-complexity theorems that use them, and depend on that file's plug-in estimator empMean'. The PR changes no imports and adds or moves no files.
✅	naming	approved	claude/claude-opus-5-5	The two new private lemma names, pullCount_div_mem_thickening and exists_tsum_measure_compl_ne_top_forall_ge_empMean'_mem, describe their conclusions in standard terminology and match adjacent names such as dist_pullCount_div_lt and the existing empMean' lemma names. No public names change and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring, the summary entry and the docstrings of the new private lemmas exists_tsum_measure_compl_ne_top_forall_ge_empMean'_mem and pullCount_div_mem_thickening accurately describe what the statements deliver. No stale, overclaiming or process-narrative documentation was introduced.
✅	proof-quality	approved	claude/claude-opus-5-5	The round argument the two Track-and-Stop proofs shared is now one lemma, and the step about proportions of pulls is a standalone lemma with no GLR context; the proofs have no undocumented defeq steps and are commented by stage. The C-tracking proof is slightly over 50 lines but each stage has a comment.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 3a576e8. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.15.}