[RemyDegenne]

Adds a target to the Generalization roadmap that proves the Track-and-Stop theorems on best arm identification with every continuity hypothesis discharged. It also pins the statement shape of the sample complexity bounds: their constant c comes with one hypothesis D⁻¹ < c, with no auxiliary rate κ.

Why.

• Hypotheses never discharged. The Track-and-Stop theorems of LMLExplore assume that the target map is continuous at the model, that the cost of the alternatives is lower semicontinuous there, and that the recommendation is locally constant. The Gaussian limit theorem also assumes that the characteristic time is finite.
  • For best arm identification, these are [GK16, Proposition 6] together with the continuity of the cost [GK16, Lemma 3]. LMLExplore proves both for one exponential family (continuousAt_of_mem_optAlloc_baiTask_restrict, continuousOn_altCost_baiTask_restrict). Yet no statement assembles them, so [GK16, Theorem 14] has no instance in LMLExplore without these hypotheses.
  • Identification 5.2 asks for the best arm identification statement, and a completion check asks for the two-armed Gaussian case. But the merged PRs #89, #126 and #134 cover 5.2 in the workers' target selection, so its best arm identification case is never picked.
• κ is not a hypothesis. eventually_expectedStoppingTime_trackAndStop_le and eventually_expectedStoppingTime_cTrackAndStop_le take a rate κ < D with 1 < κ c. This is equivalent to D⁻¹ < c (with D = inf_{v ∈ C} D(μ, v, ¬i) for C-tracking): κ is a step of the proof that leaked into the statement, and every caller rebuilds it.

Changes (only LMLRoadmaps/Generalization/):

• Conventions: sample complexity bounds take (task.altCost μ (w μ) i)⁻¹ < c, (⨅ v ∈ C, task.altCost μ v i)⁻¹ < c or task.charTime μ < c, or state the limsup. Only the generic reductions of GLR.lean keep a growth rate κ.

• Targets 1.10 and 1.11: constants as in the Conventions. The private lemmas they delete are now called mul_le_glr_plugInCost and mul_le_glr_plugInCost_of_mem_thickening; #182 renamed them.

• New target 1.25, at the end of Layer 1 so that no number changes. It discharges hw_cont, h_lsc, h_cont, hrec_eq and h_charTime on best arm identification:

  • for one exponential family: limsup_{δ→0} 𝔼[τ_δ]/log(1/δ) ≤ T*(μ) with D- and C-tracking;
  • for Gaussian arms: δ-PAC with unionBoundThreshold, and 𝔼[τ_δ]/log(1/δ) → T*(μ) at every admissible model.

  Identification 5.2 owns the general form, whose best arm identification case these statements are.

• Completion check: no Track-and-Stop theorem has a hypothesis κ, and for two Gaussian arms the limit is 8σ²/(μ_a − μ_b)².

Points to check

• The new target sits at the end of Layer 1, under its own heading, rather than after 1.11. Merged PR descriptions cite Layer 1 numbers up to 1.22.
• It needs no other target and goes in a file of its own, so it does not conflict with target 1.10, which edits TrackAndStop.lean.
• The companion PR refactor: Track-and-Stop sample complexity bounds without an auxiliary rate LMLExplore#189 removes κ from the two theorems now, ahead of 1.10 and 1.11. The Conventions then keep 1.10 and 1.11 from bringing it back.

Suggested.lean is unchanged.

Drafted with Claude Opus 5.5 at the request of the code owner.

🤖 Generated with Claude Code