[RemyDegenne]

This PR adds LMLExplore/EValues/Numeraire.lean (346 lines, one new file, no existing file changed). It proves the verification criteria that identify Statlib's numeraire e-variable through the effective null, for EValues Layer 1, item 2, Identifying numeraires [LRR25, Theorem 4.1, Corollary 4.2; RW, Theorem 6.15], together with the likelihood-ratio corollaries that item lists [RW, Theorem 3.20; LRR25, Corollary 3.15].

Roadmap: EValues

Milestone: EValues Layer 1.2, "Identifying numeraires". Covered here:

• the first bullet's main statement: for Q ≪ S and a Q-a.s. positive e-variable X* with P* = Q.withDensity X*⁻¹, X* is the numeraire exactly when P* ∈ effectiveSet S (isNumeraire_iff_withDensity_inv_mem_effectiveSet); P* is then Statlib's ripr Q S (IsNumeraire.ripr_eq) and is equivalent to Q (absolutelyContinuous_ripr, plus withDensity_absolutelyContinuous); and P* is maximal (IsNumeraire.eq_withDensity_inv_of_le).
• RW Theorem 6.15: the numeraire is the only e-variable that is a likelihood ratio against an equivalent member of the effective null (isNumeraire_iff_exists_ae_eq_rnDeriv; the sufficient direction isNumeraire_of_ae_eq_rnDeriv needs no Q ≪ S).
• the generating-family criterion [LRR25, Corollary 4.2], in the "⊃" form noted after it (isNumeraire_of_lintegral_div_le_one, ripr_mem_of_lintegral_div_le_one).
• the likelihood-ratio corollary: IsNumeraire (Q.rnDeriv P) {P} Q for Q ≪ P [RW, Theorem 3.20] (isNumeraire_rnDeriv). Its value klDiv Q P is already Statlib's maxUtility_singleton_eq_klDiv, so it is cited rather than restated. Without absolute continuity: ∞ on a P-null set N off which Q ≪ P, and (Q[|Nᶜ]).rnDeriv P on Nᶜ [LRR25, Corollary 3.15] (isNumeraire_piecewise_rnDeriv_cond). As the roadmap's "derive as corollaries" asks, isNumeraire_rnDeriv is the case N = ∅ of it.

All of these come from one statement that holds for every finite Q and every null: isNumeraire_iff_smul_withDensity_inv_mem_effectiveSet says that X is the numeraire iff (Q X.fsupport)⁻¹ • Q.withDensity X⁻¹ ∈ effectiveSet S (the normalisation of [LRR25, Theorem 3.13]). "Q ≪ S" is stated inline as ∀ s, MeasurableSet s → (∀ P ∈ S, P s = 0) → Q s = 0, and IsEVar.ae_ne_top_of_forall_measure_eq_zero records its consequence that e-variables are Q-a.s. finite.

What remains in Layer 1.2 after this PR: the dominated criterion [LRR25, Theorem 4.7] and the L¹ convergence of [LRR25, Corollary 4.11], which both need the bipolar theorem of Layer 1.1 [BS99]; the σ-algebra and stopping-time corollaries [RW, Proposition 3.22, Corollary 3.23, Theorem 7.11; KG22, Theorem 5], which need an ∫ᵉ/trim lemma that does not exist yet; the monotone-likelihood-ratio families [RW, Proposition 2.18]; and the GROW corollaries [GdHK24; LGH24].

Correction to the source: LRR25's Corollary 3.15 also says the RIPr is P₀ᵃ. With Statlib's ripr Q S = Q.withDensity (numeraire Q S)⁻¹, the RIPr is Q(Nᶜ) • P₀ᵃ (example: P₀ = ½δ_a + ½δ_b, Q = ½δ_b + ½δ_c gives ripr = ¼δ_b). So only the numeraire part of that corollary is stated.

Reuse: built on Statlib's isNumeraire_iff, IsNumeraire.ae_unique, isNumeraire_numeraire, ripr, ripr_mem_effectiveSet, rnDeriv_ripr, absolutelyContinuous_ripr_of_ae_ne_top, effectiveSet, on LMLExplore's mem_effectiveSet_of_le and subset_effectiveSet (EValues/EffectiveSet.lean), and on Mathlib's Measure.inv_rnDeriv, Measure.withDensity_rnDeriv_le, cond_mul_eq_inter' and withDensity_indicator. Before writing each declaration I grepped Mathlib, Statlib, TauCeti, LML and LMLExplore/ for it (e.g. ripr_eq, isNumeraire_rnDeriv, ae_ne_top_of, withDensity_inv), as well as the open EValues PRs (#401, #402, #404, #405, #409); none overlaps. No Mathlib infrastructure is vendored.

Local checks (not CI): scope: scoped: against a890e2a, whole-library lake build --iofail green, local-axioms: checked 1 changed module(s), 20 declaration(s); 0 violation(s), module-system, header style and environment lint passing.

🤖 Prepared with Claude Code

[RemyDegenne]

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

The earlier over-strong hS_prob assumption is gone, and the special cases are still derived from the general criterion. One redundant hypothesis remains: both generated-null theorems require hX₀, which already follows from h_one.

• LMLExplore/EValues/Numeraire.lean — isNumeraire_of_lintegral_div_le_one assumes hX₀ : ∀ᵐ ω ∂Q, X ω ≠ 0, but h_one : ∫⁻ (X ω)⁻¹ ∂Q = 1 already implies it: if Q {X = 0} > 0, the integral of X⁻¹ is ∞. Fix: Drop hX₀ and derive it inside the proof: (ae_lt_top hX.measurable.inv (h_one ▸ ENNReal.one_ne_top)).mono fun ω h ↦ (ENNReal.inv_lt_top.mp h).ne'.
• LMLExplore/EValues/Numeraire.lean — ripr_mem_of_lintegral_div_le_one has the same redundant hX₀. It only passes it on to isNumeraire_of_lintegral_div_le_one, alongside h_one. Fix: Remove hX₀ here as well once the previous fix is made.

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 · 31s · 52.7k in (45.4k cache read, 7.3k cache write) / 2.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[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	Every new statement matches LRR25 Theorem 4.1, Corollaries 3.15 and 4.2 and RW Theorems 3.20 and 6.15, with correct normalisation, directions of absolute continuity and positivity hypotheses. Attempts to break the edge cases (Q Nᶜ = 0, Q X.fsupport = 0, a null S strictly containing the generated family, the case without μ ≪ Q) all failed.
✅	reuse	approved	claude/claude-opus-5-5	The new numeraire criteria build on Statlib's numeraire/ripr API, LMLExplore's mem_effectiveSet_of_le/subset_effectiveSet and Mathlib's inv_rnDeriv/withDensity_rnDeriv_le/lintegral_withDensity_eq_lintegral_mul₀, and no Mathlib or LMLExplore declaration duplicates them (Statlib source was not available to grep). isNumeraire_rnDeriv is derived as the N = ∅ case of isNumeraire_piecewise_rnDeriv_cond rather than reproved.
✅	scope	approved	claude/claude-opus-5-5	The PR proves the main statements of EValues Layer 1.2 'Identifying numeraires' (LRR25 Theorem 4.1, Corollary 4.2; RW Theorem 6.15) and the likelihood-ratio corollaries listed at roadmap/LMLRoadmaps/EValues/README.md:347-366, as one topic. The one-lemma addition to MeasureTheory/Measure/WithDensity.lean is a prerequisite that Numeraire.lean uses directly.
✅	attribution	approved	claude/claude-opus-5-5	The file credits its informal sources (LRR25 Lemma 3.3, Theorem 3.13, Corollary 3.15, Theorem 4.1, Corollary 4.2; RW Theorems 3.20, 6.15) in its References section and per-declaration docstrings, matching the roadmap's sources for item 1.2. Formal dependencies are used via their APIs rather than adapted, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The general lemma lintegral_withDensity_inv_eq_lintegral_div is now public in its measure-theory home, and the only private helper is specific to the generated-null argument. The PR adds no definitions, so no characteristic API or simp/grind annotations are missing.
✅	generality	approved	claude/claude-opus-5-5	The general characterization for any finite Q and any null is proved first; Theorem 4.1, RW 6.15, Corollary 4.2 and the likelihood-ratio results are derived from it, with isNumeraire_rnDeriv as the N = ∅ case of the Corollary 3.15 theorem. Every hypothesis is used and none exceeds Mathlib convention; the one-sided RW 6.15 direction is exposed without the Q ≪ S and finiteness assumptions.
✅	placement	approved	claude/claude-opus-5-5	LMLExplore/EValues/Numeraire.lean joins the existing EValues directory with numeraire/RIPr-specific material, and the one generic lemma lintegral_withDensity_inv_eq_lintegral_div sits in the generic MeasureTheory/Measure/WithDensity.lean, with no Mathlib duplicate found. All three imports are narrow and used.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions in standard Mathlib/Statlib terminology, _iff/_eq suffixes match statement strength, and the ProbabilityTheory namespace and dot-notation lemmas (IsNumeraire.*, IsEVar.*) match the adjacent EValues files. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring and every public theorem docstring in Numeraire.lean describe their statements accurately, with sources cited and no proof or process narrative. The new WithDensity.lean lemma is documented and listed in that file's Main statements.
✅	proof-quality	approved	claude/claude-opus-5-5	The proofs reuse one shared rewriting lemma and the general smul criterion, the longer arguments carry structural comments, and nothing relies on undocumented definitional equality. No proof-quality issue clears the materiality bar.

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

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