[RemyDegenne]

The sample complexity bounds of Track-and-Stop now take their constant directly. They used to take a rate κ that appears only in the hypotheses.

Before: eventually_expectedStoppingTime_trackAndStop_le took {κ c : ℝ≥0} (hκ : κ < task.altCost μ (w μ) i) (hκc : 1 < κ * c), and eventually_expectedStoppingTime_cTrackAndStop_le took (hκ : ∀ v ∈ C, κ < task.altCost μ v i) (hκc : 1 < κ * c). A κ with κ < D and 1 < κ c exists exactly when D⁻¹ < c, so κ is a step of the proof, and every caller had to rebuild it.

After:

• eventually_expectedStoppingTime_trackAndStop_le takes {c : ℝ≥0} (hc : (task.altCost μ (w μ) i)⁻¹ < c).
• eventually_expectedStoppingTime_cTrackAndStop_le takes {c : ℝ≥0} (hc : (⨅ v ∈ C, task.altCost μ v i)⁻¹ < c).
• Both proofs choose κ with the new public lemma ENNReal.exists_nnreal_lt_one_lt_mul_of_inv_lt (D⁻¹ < c → ∃ κ : ℝ≥0, κ < D ∧ 1 < κ * c, for D : ℝ≥0∞ and c : ℝ≥0), in the new file LMLExplore/Basic/ENNReal/Inv.lean (mirroring Mathlib's Mathlib/Basic/ENNReal/Inv.lean). It replaces the private exists_lt_answerValue_one_lt_mul of TrackAndStop.lean, which did the same through T*(μ).
• The two _of_charTime_lt corollaries no longer build κ. They rewrite T*(μ) < c into the new hypothesis: at an optimal allocation, D(μ, w(μ), ¬i)⁻¹ = T*(μ), and on the optimal allocations the infimum is at least D(μ, ¬i).
• The docstrings state the bounds as c > D(μ, w(μ), ¬i)⁻¹. The D-tracking docstring also says that the constant does not depend on p, whereas [GK16, Theorem 14] has a factor α ∈ [1, e/2] for r(t) = O(t^α); the review of this theorem in Review: LMLExplore.Identification.IdentTask.eventually_expectedStoppingTime_trackAndStop_le LMLExplore-evidence#1 noted that the docstring left this out.

The two theorems keep their names, and their only callers are in TrackAndStop.lean. The generic reductions of GLR.lean keep their rate κ, which there is a hypothesis: the growth κ T of the statistic.

The companion roadmap change, LeanMachineLearning/LMLRoadmaps#14, makes "no auxiliary rate" a convention of the Generalization roadmap, so that targets 1.10–1.11 keep this form.

Checked locally:

• lake build --iofail;
• #lint in LMLExplore over TrackAndStop and GaussianThreshold passes.

Roadmap: Identification

🤖 Generated 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.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The new hypotheses D(μ,w(μ),¬i)⁻¹ < c and (⨅ v ∈ C, D(μ,v,¬i))⁻¹ < c are equivalent to the old existentials over κ (including D = ⊤, D = 0, empty C, and an unattained infimum, since 1 < κc is strict), and the corollary statements are unchanged. The docstrings, including the note on GK16's α factor, match the formal statements.
✅	reuse	approved	claude/claude-opus-5-5	The new ENNReal.exists_nnreal_lt_one_lt_mul_of_inv_lt generalises and replaces the deleted private exists_lt_answerValue_one_lt_mul, using Mathlib's lt_iff_exists_nnreal_btwn and inv_lt_iff_inv_lt; grep of Mathlib and LMLExplore finds no existing copy and no parallel API. The corollaries reuse charTime_eq_inv_answerValue, mem_optAlloc_iff, iInf₂_le and le_iInf₂ rather than re-deriving them.
✅	scope	approved	claude/claude-opus-5-5	Single-topic refactor of already-merged Track-and-Stop sample-complexity theorems: the auxiliary rate κ becomes the equivalent hypothesis D⁻¹ < c, and the κ-construction lemma is relocated and generalised from the existing private lemma. No new mathematics; roadmap fit is automatic and the PR is one coherent unit.
✅	attribution	approved	claude/claude-opus-5-5	Hypothesis-only refactor; GK16 and DK19 remain cited in both rewritten docstrings and the module doc (References at TrackAndStop.lean:122-126), and the new p-independence remark is sourced to GK16 Theorem 14. The new ENNReal helper lemma is a routine inequality step needing no credit, and the roadmap is credited only in the description.
✅	api-design	approved	claude/claude-opus-5-5	The general lemma ENNReal.exists_nnreal_lt_one_lt_mul_of_inv_lt is now public in LMLExplore/Basic/ENNReal/Inv.lean, a path matching Mathlib's, and the old private helper is gone. Both sample complexity theorems take the constant directly through a single hypothesis, with no compatibility layer left.
✅	generality	approved	claude/claude-opus-5-5	Replacing the rate κ with D⁻¹ < c keeps the D-tracking hypothesis equivalent and weakens the C-tracking one via the infimum over C, and both _of_charTime_lt corollaries are derived from the general theorems by rewriting. The new ENNReal helper sits at the natural level for its callers, and Mathlib has no equivalent.
✅	placement	approved	claude/claude-opus-5-5	The new general lemma ENNReal.exists_nnreal_lt_one_lt_mul_of_inv_lt sits in LMLExplore/Basic/ENNReal/Inv.lean, matching the Mathlib file it extends and the existing Basic/ENNReal/BigOperators.lean, and imports only Mathlib.Basic.ENNReal.Inv. The old private helper is fully removed, and the one new import in TrackAndStop.lean is used at lines 399 and 693.
✅	naming	approved	claude/claude-opus-5-5	The new lemma ENNReal.exists_nnreal_lt_one_lt_mul_of_inv_lt names its conclusion ∃ κ : ℝ≥0, κ < D ∧ 1 < κ * c and its hypothesis D⁻¹ < c in Mathlib vocabulary (compare ENNReal.lt_iff_exists_nnreal_btwn), belongs in the ENNReal namespace, and does not clash with any Mathlib name; the two theorems keep names that still describe their conclusions. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new ENNReal file and lemma are documented accurately, and the two Track-and-Stop theorem docstrings and module lists state the new hypotheses c > D(μ, w(μ), ¬i)⁻¹ and c > (inf_{v ∈ C} D(μ, v, ¬i))⁻¹ correctly, with no stale κ-rate wording. The earlier finding is resolved: the PR description now names the public lemma and its new file.
✅	proof-quality	approved	claude/claude-opus-5-5	Choosing κ is factored into one reusable lemma, ENNReal.exists_nnreal_lt_one_lt_mul_of_inv_lt, used by both main theorems, and the corollaries reach the new hypothesis with short single-step rewrites. There is no change/show, undocumented defeq, or brittle simpa.

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

_{Reviewing this diff at head fa3d2b3. rubrics @ 32ce206. CLI @ 32ce206. Review spend: $4.65.}