[RemyDegenne]

This PR proves the asymptotic sample-complexity reduction of the plug-in GLRT for any topological space of models, any estimator, any sampling rule and thresholds $\beta_T(h,\delta)\le\log(1/\delta)+f(T)$ with $f(T)=o(T)$. It then derives the D-tracking sample complexity of Track-and-Stop from that reduction and deletes the private mul_le_glr_plugInCost. This is Generalization 1.10 ("One sample-complexity reduction, and Track-and-Stop with D-tracking"): "Prove the asymptotic reduction of Identification 4.4 for any topological space of models, estimator and thresholds with $\beta_t(h,\delta)\le\log(1/\delta)+f(t)$, $f(t)=o(t)$, from the merged IdentTask.eventually_expectedStoppingTime_glrt_le … and IsCompact.exists_forall_mem_thickening_lt_of_lowerSemicontinuousWithinAt. Derive from it eventually_expectedStoppingTime_trackAndStop_le and eventually_expectedStoppingTime_trackAndStop_le_of_charTime_lt … and delete the private mul_le_glr_plugInCost."

Roadmap: Generalization

New declarations, all in Identification/TrackAndStop.lean, in a new section "Sample complexity of the plug-in GLRT" placed after the plug-in statistic it is about:

• IdentTask.exists_mem_nhds_mul_le_glr_plugInCost covers one step. Take a compact W of allocations with $(\theta',w)\mapsto D(\theta',w,\neg i)$ lower semicontinuous at every $(\theta,w)$, $w\in W$, a rate $\kappa$ below $D(\theta,w,\neg i)$ on $W$, and a recommendation equal to $i$ near $\theta$. Then there are neighbourhoods $U$ of $\theta$ and $V$ of $W$ such that, after $n\ne0$ rounds, $\hat\theta_n\in U$ and $N/n\in V$ give $\mathrm{GLR}_n\ge\kappa n$. This is the lower-semicontinuity step, done once.
• IdentTask.eventually_expectedStoppingTime_glrt_plugInCost_le is the reduction of Identification 4.4 (asymptotic) with $g=0$. Its hypothesis is the roadmap's convergence of the allocations: for all neighbourhoods $U$ of $\theta$ and $V$ of $W$ there are events $E_T$ with $\sum_TP(E_T^c)<\infty$ on which, for all large $T$, $\hat\theta_T\in U$ and $N(T)/T\in V$. Its conclusion is $\mathbb E[\tau_\delta]\le c\log(1/\delta)$ for all small $\delta$, for every $c>(\inf_{w\in W}D(\theta,w,\neg i))^{-1}$. The constant is taken directly, as the Conventions ask, and the rate $\kappa$ is a step of the proof.
• IdentTask.eventually_expectedStoppingTime_glrt_plugInCost_le_of_isBigO is the same bound for thresholds $\log(r(T)/\delta)$ with $r(T)=O(T^p)$. It is derived from the previous theorem in the same way as the existing _of_isBigO forms in GLR.lean and AlmostSure.lean, and it is the form Track-and-Stop uses.

Restated through the reduction, with unchanged statements:

• IdentTask.eventually_expectedStoppingTime_trackAndStop_le is now the reduction with W = {w μ}. Its proof only shows that D-tracking's allocations converge on the good events of forced exploration ([GK16, Lemma 19] and the tracking bound abs_pullCount_div_sub_le). Its constant stays (task.altCost μ (w μ) i)⁻¹ < c, and _of_charTime_lt (with task.charTime μ < c) and the union-bound corollaries still follow from it unchanged.
• IdentTask.eventually_mul_le_glr_plugInCost (AlmostSure.lean, the almost-sure form [GK16, Proposition 13]) now follows from exists_mem_nhds_mul_le_glr_plugInCost instead of repeating the thickening argument. That leaves the expectation and almost-sure reductions with a single lower-semicontinuity step.

Removed: the private mul_le_glr_plugInCost. It is replaced by the private dist_pullCount_div_lt, the D-tracking-specific step that keeps only the proportions-of-pulls part (with the exploration threshold $\sqrt k-K/2$ and the constants of this proof), and no longer mentions the GLR statistic. No public declaration is removed or renamed.

What remains: Generalization 1.11, which derives the two C-tracking theorems from this reduction with $W=w^*(\mu,\neg i)$ and deletes mul_le_glr_plugInCost_of_mem_thickening and the round argument the two proofs share. This PR does not touch C-tracking.

Reuse: the reduction is built on the existing IdentTask.eventually_expectedStoppingTime_glrt_le (GLR.lean), IsCompact.exists_forall_mem_thickening_lt_of_lowerSemicontinuousWithinAt, ENNReal.exists_nnreal_lt_one_lt_mul_of_inv_lt, glr_plugInCost_eq_mul, eventually_log_le_mul_of_isBigO and log_div_le_log_one_div_add_log. I grepped Mathlib, Tau Ceti, LML and Statlib for an expected-stopping-time or plug-in GLR reduction and found nothing. The statements follow [GK16, proof of Theorem 14] (Garivier and Kaufmann, COLT 2016), which the docstrings cite.

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

🤖 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	The reduction's hypotheses and constant match the existing GLR reduction, its convergence hypothesis is proved for D-tracking rather than assumed, and every Track-and-Stop and almost-sure statement is unchanged.
✅	reuse	approved	claude/claude-opus-5-5	The new plug-in GLRT reduction builds on the existing eventually_expectedStoppingTime_glrt_le and IsCompact.exists_forall_mem_thickening_lt_of_lowerSemicontinuousWithinAt, and its lower-semicontinuity step is factored into one lemma that the almost-sure and D-tracking proofs now share. No existing declaration is duplicated; the remaining C-tracking copy is scheduled for roadmap item 1.11.
✅	scope	approved	claude/claude-opus-5-5	The PR implements Generalization target 1.10 directly: a general plug-in GLRT reduction, D-tracking Track-and-Stop derived from it, and deletion of the private mul_le_glr_plugInCost. The AlmostSure.lean change reuses the new one-step lemma, so the PR stays a single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The new plug-in GLRT reduction and the Track-and-Stop restatement cite [GK16, proof of Theorem 14] in their docstrings and the module overview, with the full reference in the file's References section; the rest is internal refactoring and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The PR adds the plug-in GLRT reduction lemma and its two expected-stopping-time theorems as public declarations, which the roadmap and C-tracking (1.11) need, and deletes the old private helper without leaving an alias. The new private dist_pullCount_div_lt is a D-tracking-specific application of the public abs_pullCount_div_sub_le, so keeping it private is correct.
✅	generality	approved	claude/claude-opus-5-5	The plug-in GLRT reduction is stated for any topological model space, estimator, compact allocation set and sampling rule, with the lower-semicontinuity step proved once and D-tracking derived as the singleton case. No unused or overly strong assumptions, and no proof duplicated for a special case.
✅	placement	approved	claude/claude-opus-5-5	The plug-in GLRT reduction lemmas are placed right after plugInCost and glr_plugInCost_eq_mul in Identification/TrackAndStop.lean, which defines the statistic they are about, and the D-tracking helper stays next to its only user. The PR changes no imports and adds no shim or forwarding module.
✅	naming	approved	claude/claude-opus-5-5	The new names describe their conclusions and match the existing eventually_expectedStoppingTime_glrt_le{,_of_isBigO} and eventually_mul_le_glr_plugInCost names; no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new public declarations and the reworked module docstring in TrackAndStop.lean and AlmostSure.lean describe their statements accurately, without overclaiming or stale references to the deleted lemma. No documentation issues meet the materiality bar.
✅	proof-quality	approved	claude/claude-opus-5-5	The lower-semicontinuity step is now factored into a single lemma shared by the expectation and almost-sure reductions, and the D-tracking step is reduced to a GLR-free proportions lemma; the proofs use explicit rewrite lemmas, with no change/show or hidden definitional equality. The long Track-and-Stop proof has comments marking each stage.

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

_{Reviewing this diff at head 1c2e7a5. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.08.}