[RemyDegenne]

This PR adds the logarithmic sum bound of RF-Express [MDJKLV21, Lemma 9] to LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean. If 0 ≤ u k ≤ max 1 (U k) for every k < n, where U k = ∑_{i < k} u i, then ∑_{k < n} u k / max 1 (U k) ≤ 3 log (U n + 1) (Real.sum_div_max_one_le_three_mul_log). Real.sum_div_max_one_le_four_mul_log is the statement exactly as the roadmap and the source give it, for u k ∈ [0, 1] and with the constant 4. The proof telescopes the one-step bound u / max 1 U ≤ 3 (log (U + u + 1) - log (U + 1)), which follows from 1 - x⁻¹ ≤ log x (Mathlib's Real.one_sub_inv_le_log_of_pos) together with U + u + 1 ≤ 3 max 1 U.

Target: ReinforcementLearning, Layer 19.2 (RF-Express [MDJKLV21, Theorem 1]), tool bullet "$\sum_t u_{t+1}/\max(1,U_t)\le4\log(U_{T+1}+1)$ [MDJKLV21, Lemma 9]". On indexing: the source writes U_t = ∑_{l=1}^t u_l and sums over t = 0, …, T. Re-indexing from 0 (u k = u_{k+1}, n = T + 1) gives exactly the Lean statement. I checked this against the text of Lemma 9 in arXiv:2007.13442. This is the version with the 0-based indices. The hypotheses are weakened from u k ≤ 1 to u k ≤ max 1 (U k), the same hypotheses as the neighbouring doubling bound Real.sum_div_sqrt_max_one_le (LMLExplore/Analysis/Real/Sqrt.lean), and the same proof gives the constant 3. The one-step bound is private, as in that sibling. I add the new statements at the end of the file and at the end of its docstring list, so they don't overlap with the edits that the open PR #287 makes to the same file.

After this PR, the last open tools of Layer 19.2 are in open PRs: counts versus pseudo-counts in #292, the KL-to-Bernstein transport and variance transfers in #291, and the implicit-inequality inversion in #287. What remains for the milestone is the RF-Express algorithm itself, on the Layer 7.7 and Layer 14 infrastructure (statesEnv, episodic counts and stream models), and its PAC and sample-complexity theorems.

Source: this is adapted from the paper project RemyDegenne/Essakine2026Tight at commit 9c77165d56f81c1db7a9835068356bb14886a3be (Apache 2.0), file Essakine2026Tight/ForLMLExplore/Analysis/SpecialFunctions/Log/Basic.lean (Real.sum_div_max_one_le_three_mul_log, Real.sum_div_max_one_le_four_mul_log, stated there for u k ∈ [0, 1]). The paper is [EV26, Lemma 28], and the constant 3 follows that project's notes/paper-errata.md E19. The code credits the source and its reference [MDJKLV21]. No public declaration is removed or renamed.

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R25

🤖 Prepared with Claude Code

[RemyDegenne]

🟡 attribution — request_changes claude/claude-opus-5-5

The code credits [MDJKLV21, Lemma 9] and the Essakine2026Tight formalization, but leaves out [EV26, Lemma 28] and the erratum E19 behind the constant 3, both named in the description. The credit line for the adapted formalization is incomplete compared with the repo's own convention.

• LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean:446 — The description says the source is [EV26, Lemma 28] and that the constant 3 follows erratum E19 in the project's notes/paper-errata.md. Neither appears in the code, yet the sharpened constant is the main way this result differs from MDJKLV21. Fix: Cite [EV26, Lemma 28] and erratum E19 in the docstring of sum_div_max_one_le_three_mul_log, and add an [EV26] entry to the module's References, using the same wording as in Episodic/Basic.lean.
• LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean:446 — The credit for the adapted formalization says '(same author)', which is unverified and unclear, and it gives no licence, commit or full path. Fix: Follow the sibling files: give the full file path Essakine2026Tight/ForLMLExplore/Analysis/SpecialFunctions/Log/Basic.lean, then 'by Rémy Degenne, Apache 2.0', and optionally the commit 9c77165d.

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 · 19s · 30.6k in (25k cache read, 5.6k cache write) / 1.7k out tokens · reviewing this diff · rubric}

[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.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	Both theorems match [MDJKLV21, Lemma 9] after the stated 0-based re-indexing (U k = ∑_{i<k} u i = U_k, n = T+1), and the constant 3 is correct under the weakened hypothesis u k ≤ max 1 (U k), since U + u + 1 ≤ 3·max 1 U. No vacuity, misplaced content or degenerate edge case found (n = 0 gives 0 ≤ 0).
✅	reuse	approved	claude/claude-opus-5-5	Neither Mathlib nor LMLExplore already has the logarithmic sum bound; the one-step bound reuses Mathlib's Real.one_sub_inv_le_log_of_pos, and the constant-4 corollary is the exact roadmap statement.
✅	scope	approved	claude/claude-opus-5-5	Adds exactly the roadmap-listed RF-Express tool [MDJKLV21, Lemma 9] (ReinforcementLearning Layer 19.2, README.md:1667), with its sharper constant-3 form, as a single coherent topic.
🟡	attribution	changes requested	claude/claude-opus-5-5	The code credits [MDJKLV21, Lemma 9] and the Essakine2026Tight formalization, but leaves out [EV26, Lemma 28] and the erratum E19 behind the constant 3, both named in the description. The credit line for the adapted formalization is incomplete compared with the repo's own convention.
✅	api-design	approved	claude/claude-opus-5-5	The PR adds two public theorems, the general constant-3 bound and the roadmap-named constant-4 form of [MDJKLV21, Lemma 9], and keeps the one-step helper private like its sibling in Sqrt.lean. It adds no definitions, so no characteristic API or automation annotations are owed, and it leaves no compatibility surface.
✅	generality	approved	claude/claude-opus-5-5	The general constant-3 bound uses the same hypotheses as the sibling doubling bound Real.sum_div_sqrt_max_one_le, and the roadmap's constant-4 form is derived from it as a corollary, not proved again. All hypotheses are used and nothing is over-generalized.
✅	placement	approved	claude/claude-opus-5-5	The logarithmic sum bounds and their private one-step lemma belong in LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean, matching how the sqrt doubling bound is placed in Analysis/Real/Sqrt.lean. The statements are generic rather than roadmap-specific, and no imports change.
✅	naming	approved	claude/claude-opus-5-5	The new names describe their conclusions in standard Mathlib terms, match the sibling Real.sum_div_sqrt_max_one_le, and sit in the existing Real namespace. The PR adds no notation.
✅	documentation	approved	claude/claude-opus-5-5	The new module-docstring entries, the reference and both theorem docstrings accurately describe the statements, including the 0-based re-indexing of [MDJKLV21, Lemma 9] and the sharper constant 3; the cross-reference to Real.sum_div_sqrt_max_one_le resolves. No roadmap or process narrative leaks into the file.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, automation-driven (linarith/nlinarith/gcongr/omega), commented at their key steps, and free of change/show or defeq reliance. The one-step bound is factored out as a lemma and the constant-4 form is a thin corollary.

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

_{Reviewing this diff at head daceb44. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $0.79.}

[prevostad]

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	Both statements faithfully formalize [MDJKLV21, Lemma 9] after the stated 0-based reindexing (u k = u_{k+1}, n = T+1), and the constant-3 strengthening under u k ≤ max 1 (U k) is mathematically sound via 1 − 1/x ≤ log x and U + u + 1 ≤ 3·max 1 U. No vacuity, placeholder, or hypothesis-smuggling found.
✅	reuse	approved	claude/claude-opus-5-5	Both public theorems are new to Mathlib and LMLExplore, and the proof reuses Mathlib's Real.one_sub_inv_le_log_of_pos; the constant-4 corollary is the statement the roadmap names, and the induction shared with Real.sum_div_sqrt_max_one_le is too short to require a shared helper.
✅	scope	approved	claude/claude-opus-5-5	Adds the roadmap's RF-Express tool [MDJKLV21, Lemma 9] (ReinforcementLearning README line 1667) in its stated form with constant 4, plus a sharper constant-3 version from the same proof, as one coherent unit. This directly supplies a listed prerequisite of the RF-Express PAC theorem and duplicates nothing on main.
✅	attribution	approved	claude/claude-opus-5-5	The code credits [MDJKLV21, Lemma 9], [EV26, Lemma 28], erratum E19 for the constant 3, and the adapted Essakine2026Tight formalization (file, commit, author, licence). The roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The PR exposes two public theorems: the constant-4 form, which the roadmap names (ReinforcementLearning README:1667), and the reusable constant-3 generalization; the private one-step lemma is specific to the telescoping proof, as is its sibling in Real/Sqrt.lean:141. It adds no definitions, compatibility artifacts or annotation issues.
✅	generality	approved	claude/claude-opus-5-5	The general constant-3 theorem uses the same weak hypotheses as its sibling Real.sum_div_sqrt_max_one_le, and every hypothesis is used. The constant-4 form the roadmap names is derived from it as a corollary rather than proved again.
✅	placement	approved	claude/claude-opus-5-5	The two new log sum bounds are generic real inequalities, placed in SpecialFunctions/Log/Basic.lean next to similar log-sum lemmas, which mirrors the square-root version in Real/Sqrt.lean. No imports change.
✅	naming	approved	claude/claude-opus-5-5	Both public theorem names describe their conclusions in standard Mathlib terms and match the sibling Real.sum_div_sqrt_max_one_le; the Real namespace and private helper name are appropriate, and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring entries and the docstrings of both public theorems and the private helper match their statements; the 0-based/1-based index conversion is correct and the references are complete. There is no proof narration, overclaiming or roadmap/process text.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, rest on robust arithmetic automation (linarith/nlinarith/gcongr/field_simp), carry comments on the key steps, and use no change/show or definitional-equality tricks. Nothing to report from the proof-quality angle.

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

_{Reviewing this diff at head fb2753e. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $0.77.}