[RemyDegenne]

This PR derives the asymptotic part of [LS, Theorem 8.1] for the asymptotically optimal UCB algorithm ucbF σ2 as the Gaussian instance of KL-UCB for exponential families, as Bandits Layer 3.4 asks ("Deduce, as the Gaussian instance, the eventual form of Layer 2.2 for σ²-sub-Gaussian rewards"; Layer 2.2: "the eventual form is also the Gaussian instance of Layer 3.4"). Until now ucbF_regret_eventually_le and UCBF.integral_pullCount_eventually_le each had their own ε-argument over the explicit finite-time bound. Now they follow from klucbFam_gaussianReal (ucbF σ2 is KL-UCB for the Gaussian family of variance σ²):

• ucbF_regret_eventually_le is klucbFam_gaussianReal_regret_eventually_le with a common variance.
• UCBF.integral_pullCount_eventually_le is KLUCBFam.integral_pullCount_eventually_le for the Gaussian family, with d(μ_a, μ*) = Δ_a² / (2σ²) (expFamilyDiv_gaussianReal).

Both keep their names and their exact statements. They move from LMLExplore/Bandits/AsymptoticallyOptimalUCB.lean to LMLExplore/Bandits/KLUCB.lean, the first file where the KL-UCB family theorems exist; KLUCB.lean already imports AsymptoticallyOptimalUCB.lean. Their old proofs are deleted. The explicit finite-time bounds UCBF.integral_pullCount_le and ucbF_regret_le stay where they are, since Layer 2.2 says "the explicit constants above keep the proof through [LS, Lemma 8.2]". The module docstrings of both files are updated. AsymptoticallyOptimalUCB.lean drops its import of LMLExplore.Bandits.Regret, which only the moved proof used. The only downstream user is Bandits/AsymptoticOptimality.lean (UCBF.isConsistent, tendsto_ucbF_regret_div_log_gaussianBandit), which already imports KLUCB and builds unchanged.

Public declarations removed or renamed: none. The two moved theorems keep their names and statements; only their module changes, from LMLExplore.Bandits.AsymptoticallyOptimalUCB to LMLExplore.Bandits.KLUCB.

Milestone: Bandits Layer 3.4 (regret of KL-UCB for exponential families and its instances). After this PR, Layer 3 has only its completion examples left: the Bernoulli boundary level U(0, c) = 1 - e^{-c} and a two-armed Bernoulli bandit.

Verification (local checks, not CI): tauceti-local-checks verify --policy ordinary passed with scope: scoped: against 7fc78707241a5393aa85a7751e472cf1cb45fca9. The whole-library lake build --iofail succeeded (8551 jobs). local-axioms: checked 2 changed module(s), 64 declaration(s); 0 violation(s). Module-system, header-style and changed-module environment lint passed.

Roadmap: Bandits

🤖 Prepared with Claude Code

[RemyDegenne]

🟡 proof-quality — request_changes claude/claude-opus-5-5

The new pull-count proof duplicates two pieces of Gaussian reasoning already in KLUCB.lean: the MGF dominance of each arm by the Gaussian family member, and the identity d(μ_a, μ*) = Δ_a² / (2σ²) from a rewrite chain. Both should become small lemmas shared with the existing proofs.

• LMLExplore/Bandits/KLUCB.lean:799 — The hdom block (lines 799-802) repeats the hdom block of klucbFam_gaussianReal_regret_eventually_le (lines 775-778), differing only in m = 0 and a common σ2. This hides a reusable fact: a sub-Gaussian arm is MGF-dominated on univ by the matching member of the Gaussian family. Fix: Add a lemma, e.g. HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal (m) (hσ2) : MGFDominatedOn id μ id ((gaussianReal m σ2).expFamily id ((gaussianReal m σ2).natParam id μ[id])) univ, and use it in both proofs.
• LMLExplore/Bandits/KLUCB.lean:809 — rwa [expFamilyDiv_gaussianReal _ hσ2, ← neg_sub, neg_sq, ← hgap, inv_div] is a five-step rewrite chain. Its first four steps redo the per-arm computation inside sum_gap_div_expFamilyDiv_gaussianReal (line 759: rw [expFamilyDiv_gaussianReal _ (hσ2 a), ← neg_sub, neg_sq, ← gap_eq_bestArm_sub]), so the identity d(μ_a, μ*) = Δ_a² / (2σ²) is stated nowhere and is rederived twice. Fix: Factor out expFamilyDiv_gaussianReal_eq_gap_sq (m) (hσ2) : (gaussianReal m σ2).expFamilyDiv id (ν a)[id] (ν (bestArm ν))[id] = gap ν a ^ 2 / (2 * σ2). Use it in the sum lemma and here, which turns this step into rwa [expFamilyDiv_gaussianReal_eq_gap_sq, inv_div] and also removes the auxiliary hgap.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 26s · 64.1k in (51.1k cache read, 13k cache write) / 2.4k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

Fixed in 7636fcb, as suggested: added HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal (for a general X/Q, mean a and generator m) and expFamilyDiv_gaussianReal_eq_gap_sq. Both hdom blocks are now one-liners using the first. The second replaces the rewrite chain in sum_gap_div_expFamilyDiv_gaussianReal, and in UCBF.integral_pullCount_eventually_le the last step is now rwa [expFamilyDiv_gaussianReal_eq_gap_sq _ hσ2, inv_div], without the auxiliary hgap.

[RemyDegenne]

AI review — changes requested

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 moved theorems keep their exact statements (σ2 is now an explicit implicit binder instead of a section variable) and are derived from the Gaussian KL-UCB results without new assumptions; no faithfulness issue found.
✅	reuse	approved	claude/claude-opus-5-5	Both moved theorems now follow directly from the existing KL-UCB family results (KLUCBFam.integral_pullCount_eventually_le, klucbFam_gaussianReal_regret_eventually_le) instead of repeating the ε-argument, and the helper the old proofs used still has another user (ThompsonSampling/Gaussian.lean:662). No duplicated or replaceable material found.
✅	scope	approved	claude/claude-opus-5-5	The PR re-proves two existing theorems (ucbF_regret_eventually_le, UCBF.integral_pullCount_eventually_le) as the Gaussian instance of KL-UCB, which is what Bandits Layer 3.4 and Layer 2.2 ask for (README.md:305, :382). It is a single-topic refactor with no new mathematics, so roadmap fit is automatic.
✅	attribution	approved	claude/claude-opus-5-5	The moved theorems keep their [LS, Theorem 8.1 / (8.2)] citations, and the KLUCB.lean references now cover Chapters 8 and 10, which credits both the moved material and the KL-UCB sources; the new proofs only combine existing in-repo declarations, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The two theorems move to KLUCB.lean with the same names and statements, and the old declarations are deleted with no compatibility alias or forwarding import. No new definitions, helpers, exposed bodies or annotations are added.
✅	generality	approved	claude/claude-opus-5-5	Both eventual ucbF bounds are now derived from the general KL-UCB family theorems via klucbFam_gaussianReal, the special-case ε-arguments are removed, and the hypotheses are unchanged and all used; the statements sit at the natural level.
✅	placement	approved	claude/claude-opus-5-5	The two eventual-regret theorems move to KLUCB.lean and sit next to klucbFam_gaussianReal_regret_eventually_le, the earliest file where the KL-UCB family results they now use exist. The removed LMLExplore.Bandits.Regret import was only used by the deleted proof, and no forwarding surface remains.
✅	naming	approved	claude/claude-opus-5-5	No new names or notation; the moved theorems keep names consistent with the adjacent KLUCB/KLUCBFam/GaussianTS integral_pullCount_eventually_le and *_regret_eventually_le family and describe their eventual ≤ conclusions.
✅	documentation	approved	claude/claude-opus-5-5	The moved theorems' docstrings match their statements and relate them to the KL-UCB family results without overclaiming. Both module docstrings are updated: one lists the moved theorems and cites Chapter 8, the other points to the new module, and no stale proof narrative is left.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	The new pull-count proof duplicates two pieces of Gaussian reasoning already in KLUCB.lean: the MGF dominance of each arm by the Gaussian family member, and the identity d(μ_a, μ*) = Δ_a² / (2σ²) from a rewrite chain. Both should become small lemmas shared with the existing proofs.

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

_{Reviewing this diff at head 8ae6d4f. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.04.}