[RemyDegenne]

Layer 4.2 asks for the union-bound thresholds log(C t^α / δ) of [GK16, Proposition 12] with an explicit constant C(α, K). No such constant exists: C has to depend on δ. This amends the target, and Layer 4.4 so that the corrected thresholds are still covered by the sample-complexity bounds.

Why. The proof of [GK16, Proposition 12] (Appendix C) bounds the probability of error by ∑_t e^{K+1} (β(t, δ)² log t / K)^K e^{-β(t, δ)}. For β(t, δ) = log(C t^α / δ) this is (δ / C) ∑_t (e^{K+1} / K^K) (log²(C t^α / δ) log t)^K / t^α. The condition the paper then puts on C uses log²(C t^α), without the δ. The sum with the δ grows like log(1/δ)^{2K} as δ → 0, so the argument gives a C of that order, that is log C = O(log log(1/δ)). This is erratum E2 of the paper project RemyDegenne/Garivier2016Optimal.

Layer 4.4 stated its bounds for thresholds β_t(h, δ) ≤ log(1/δ) + f(t), with f(t) = o(t). With C depending on δ, the Proposition 12 thresholds are no longer of that form. Neither are the other exponential-family thresholds of Layer 4.2: [KK21] has log(1/δ) + O(log log(1/δ)), and [LS, Lemma 33.7] has x_δ = (1 + o(1)) log(1/δ). Layer 5.2 asks for Track-and-Stop to be δ-PAC with the thresholds of Layer 4.2 and asymptotically optimal through Layer 4.4, which needs Layer 4.4 to cover them. The proof of [GK16, Theorem 14] goes through with an extra term g(δ) = o(log(1/δ)).

Changes (only LMLRoadmaps/Identification/README.md)

• Layer 4.2, item 2: the thresholds of [GK16, Proposition 12] with an explicit C(α, K, δ) such that log C(α, K, δ) = O(log log(1/δ)). The item now says that no C independent of δ works, and where the paper's proof drops the δ.
• Layer 4.4, expected sample complexity: thresholds β_t(h, δ) ≤ log(1/δ) + g(δ) + f(t) with g(δ) = o(log(1/δ)) and f(t) = o(t). The thresholds of item 2 and log(r(t)/δ) with r(t) = O(t^α) are cases. LMLExplore's IdentTask.eventually_expectedStoppingTime_glrt_le is the case g = 0.

Points to check

• That no constant independent of δ works is the code owner's assessment, made while checking the statements of the Garivier2016Optimal paper project. What a reader can check directly is the gap in the proof.
• log C = O(log log(1/δ)) is what the paper's argument gives once the δ is kept: C of order log(1/δ)^{2K}. A sharper argument might give a smaller C; the target asks only for this order.
• LMLExplore's IdentTask.eventually_expectedStoppingTime_glrt_le has the narrower g = 0 form. This PR does not schedule its restatement in LMLRoadmaps/Generalization/; a companion PR can add that target.

Suggested.lean is unchanged.

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

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMToRcTS8JUy4ChhSPh