[RemyDegenne]

This pull request proves that n observations are worth exactly n times one when one observation already attains the smallest relative entropy to the null. It adds the new file LMLExplore/EValues/BipolarRate/SingleLetter.lean, and adds the two general bounds mul_maxLogGrowth_one_le and maxLogGrowth_one_le_bipolarRate to LMLExplore/EValues/BipolarRate.lean, after maxLogGrowth_le_mul_bipolarRate. No declaration is removed or renamed.

Main declarations

For a probability measure Q₁ and a null S₁ of probability measures on any measurable space:

• mul_maxLogGrowth_one_le: n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n, by iterating maxLogGrowth_add_le (the members of the null need only be finite measures).
• maxLogGrowth_one_le_bipolarRate: maxLogGrowth Q₁ S₁ 1 ≤ bipolarRate Q₁ S₁.
• bipolarRate_eq_maxLogGrowth_one_of_le and maxLogGrowth_eq_mul_of_bipolarRate_le: the same conclusions under the weaker hypothesis bipolarRate Q₁ S₁ ≤ maxLogGrowth Q₁ S₁ 1 (the second for n ≠ 0 and a null of finite measures); the KL forms below are derived from them through bipolarRate_le_iInf_klDiv.
• bipolarRate_eq_maxLogGrowth_one_of_iInf_klDiv_le and bipolarRate_eq_iInf_klDiv_of_iInf_klDiv_le_maxLogGrowth_one: if ⨅ P ∈ S₁, klDiv Q₁ P ≤ maxLogGrowth Q₁ S₁ 1, then the bipolar rate is both.
• maxLogGrowth_eq_mul_of_iInf_klDiv_le_maxLogGrowth_one: under the same hypothesis, maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1 for every n ≠ 0.

The KL statements are [EVR26, Note 11, Theorem 9], re-proved on LMLExplore's API.

Roadmap coverage (EValues, Layer 6, item 1)

Covered: in the third bullet, "for any nonempty S₁, if KL_inf(Q₁, S₁) ≤ a 1 then a n = n * a 1 for every n, so that d = KL_inf(Q₁, S₁)". No semicontinuity, convexity or compactness of the null is assumed; [RR26, Proposition 4.5] gives the hypothesis for a weakly compact convex null.

Notes for reviewers

• The statement is for n ≠ 0, as maxLogGrowth_le_mul_bipolarRate, and so needs no nonemptiness of the null, which the roadmap assumes to include n = 0. For an empty null and n = 0 the left side is ⊤ and the right side 0.
• The hypothesis is written with the infimum in ℝ≥0∞ coerced to EReal, the form of the conclusion of bipolarRate_le_iInf_klDiv.
• The new file sits in LMLExplore/EValues/BipolarRate/, beside Semicontinuity.lean from feat: the bipolar rate equals the smallest relative entropy to the null under lower semicontinuity [RR26, Theorem 4.1] #414.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R38

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

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

⚠️ 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	All five new statements correctly formalize EVR26 Note 11 Theorem 9 and the roadmap clause: the bounds come from superadditivity (maxLogGrowth_add_le) and the n = 1 term of the bipolarRate supremum, and the KL hypothesis matches the conclusion of bipolarRate_le_iInf_klDiv. Restricting to n ≠ 0 avoids the empty-null, n = 0 counterexample, the assumptions are no stronger than needed, and no statement is vacuous.
✅	reuse	approved	claude/claude-opus-5-5	No duplication: the new declarations are short combinations of existing BipolarRate API (maxLogGrowth_div_le_bipolarRate, maxLogGrowth_le_mul_bipolarRate, bipolarRate_le_iInf_klDiv, maxLogGrowth_add_le via EReal.nsmul_le_of_superadditive), and none of them is already stated in LMLExplore or Mathlib. The nearest existing result, bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le in Semicontinuity.lean, has a different (semicontinuity) hypothesis and does not replace these.
✅	scope	approved	claude/claude-opus-5-5	Directly proves the EValues Layer 6 item 1 clause at roadmap README.md:903-904 (KL_inf ≤ a 1 implies a n = n * a 1 and d = KL_inf) as one new file plus two helpers it needs in Basic.lean. Single topic; no duplicate of existing main results found.
✅	attribution	approved	claude/claude-opus-5-5	SingleLetter.lean credits its main source, [EVR26, Note 11, Theorem 9], with its Lean library EValuesResearch in the module docstring, the References section and each KL-form theorem, and credits RR26 for the side remark; the two lemmas added to Basic.lean are routine and need no credit. The roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The five new public theorems duplicate no existing declaration, and their arguments follow the conventions of maxLogGrowth_add_le, maxLogGrowth_div_le_bipolarRate and bipolarRate_le_iInf_klDiv. The PR adds no definitions, so there is no characteristic API or body exposure to judge, and conditional (in)equalities need no simp or grind annotations.
✅	generality	approved	claude/claude-opus-5-5	The general forms (hypothesis bipolarRate ≤ maxLogGrowth 1, a null of finite measures) are stated first, and the KL-hypothesis versions are one-line corollaries whose probability-measure assumption comes only from bipolarRate_le_iInf_klDiv. Every assumption matches the lemma it feeds, and no special case is proved twice.
✅	placement	approved	claude/claude-opus-5-5	The two general lemmas sit in BipolarRate/Basic.lean next to maxLogGrowth_le_mul_bipolarRate, and the results that depend on the single-observation hypothesis are in their own BipolarRate/SingleLetter.lean, whose one import (BipolarRate.Basic) is used. On the PR head the BipolarRate/ directory already has Basic.lean, so no flat Foo.lean sits beside Foo/.
✅	naming	approved	claude/claude-opus-5-5	Theorem names describe their conclusions in the terminology of adjacent BipolarRate declarations (maxLogGrowth_le_mul_bipolarRate, bipolarRate_le_iInf_klDiv, bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le), with _eq/_le matching statement strength. The namespace matches sibling files and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The earlier overclaim is fixed: the module docstring now credits the weaker bipolar-rate hypothesis only with bipolarRate = maxLogGrowth 1 and the n-fold equality for n ≠ 0. All new declarations and the new file are documented accurately, with no proof or process narrative.
✅	proof-quality	approved	claude/claude-opus-5-5	Each new proof is a short composition of existing BipolarRate lemmas (le_antisymm, trans, gcongr) or a single small simpa instantiating maxLogGrowth_div_le_bipolarRate at n = 1 or EReal.nsmul_le_of_superadditive. There are no change/show steps, no reliance on undocumented definitional equality, no brittle rewrite chains and no hidden reusable facts.

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

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