[RemyDegenne]

This PR proves the exact Ville identity for ℝ≥0∞-valued supermartingales [dlP+26, Theorems 1 and 4], with a horizon and without one, and derives from it Ville's inequality, its equality case, and the extended Ville inequality of [WR23, Theorem 4.1] for supermartingales with no integrability condition. This is EValues Layer 2.3, "The exact Ville identity and its consequences", first two bullets.

Roadmap: EValues

LMLExplore/Probability/Martingale/Centering.lean (general, Mathlib-level, next to Mathlib's Probability/Martingale/Centering.lean):

• MeasureTheory.setIntegral_stoppedValue_sub_eq_predictablePart: for an integrable process (Banach-valued, no adaptedness needed), bounded stopping times σ ≤ τ and s measurable at σ, the increments of f and of its Mathlib predictablePart from σ to τ have the same integral over s.
• MeasureTheory.Supermartingale.antitone_predictablePart: the supermartingale counterpart of Mathlib's Submartingale.monotone_predictablePart.

LMLExplore/Probability/Martingale/ExactVille.lean (namespace ProbabilityTheory, on IsENNSupermartingale/IsTestSupermartingale from Layer 2.1 and stoppedValueLimsup from Layer 2.2):

• IsENNSupermartingale.setLIntegral_eq_add_stoppedValueLimsup: exact optional stopping. For m ≤ τ ≤ N and s ∈ ℱ m, ∫⁻ s, M m is the integral of M at τ plus that of the predictable decrease, ofReal (A m - A τ) with A the predictable part of the real values.
• IsENNSupermartingale.setLIntegral_eq_add_stoppedValueLimsup_min and IsENNSupermartingale.setLIntegral_eq_add_stoppedValueLimsup_add_iInf: the same exact optional stopping at any stopping time T ≥ m (possibly infinite). With a horizon N ≥ m: ∫⁻ s, M m is M T over s ∩ {T ≤ N}, plus the decrease at T ∧ N, plus M N over s ∩ {N < T}. Without one: M T over s ∩ {T ≠ ⊤}, plus the decrease at T, plus ⨅ N ≥ m, ∫⁻ s ∩ {N < T}, M N. The exact Ville identities below are these at the hitting time.
• setLIntegral_eq_exact_ville_horizon and lintegral_zero_eq_exact_ville_horizon [dlP+26, Theorem 1]: ∫⁻ M 0 = b P(T ≤ N) + overshoot + decrease + remainder, with T = hittingAfter M (Ici b) 0. The first is stated from any time m on any ℱ m-measurable set, the second is the roadmap's statement. The identity holds for every level b : ℝ≥0∞ and every M 0 with finite expectation, so M 0 = 1 and b > 1 are special cases.
• setLIntegral_eq_exact_ville and lintegral_zero_eq_exact_ville [dlP+26, Theorem 4]: the identity without horizon. The overshoot is taken over {T ≠ ⊤}, the decrease is read at T through stoppedValueLimsup, and the remainder is ⨅ N ≥ m, ∫⁻ s ∩ {N < T}, M N, which is the limit of the finite-horizon remainders.
• mul_measure_inter_eq_setLIntegral_iff: equality in Ville's inequality holds exactly when overshoot, decrease and remainder all vanish.
• measure_inter_exists_le_le [WR23, Theorem 4.1]: P (s ∩ {∃ n ≥ m, c ≤ M n}) ≤ (∫⁻ s, min (M m) c) / c for every ℝ≥0∞-valued supermartingale, with no integrability. The proof applies the identity to the process that equals c before m and M on s ∩ {M m < c} from m on.
• IsENNSupermartingale.measure_exists_le_le, IsTestSupermartingale.measure_exists_le_le, IsTestSupermartingale.measure_exists_inv_le_le: Ville's inequality P {∃ n, c ≤ M n} ≤ ∫⁻ M 0 / c, and its level form P {∃ n, α⁻¹ ≤ M n} ≤ α for test supermartingales. These are the shapes of Suggested.lean, generalized from {P} to any finite member of the null.

The decrease is expressed with Mathlib's predictablePart of (M n).toReal, as the roadmap asks. Since the predictable part of a supermartingale is a.s. antitone, the decrease is the value at T ∧ N of the a.s. nondecreasing process n ↦ ofReal (A m - A n). All four terms are nonnegative in ℝ≥0∞. Nothing is vendored, and no existing declaration is removed or renamed. I searched Mathlib, Tau Ceti, LML, Statlib and LMLExplore/ for Ville-type statements, stopped Doob decompositions and antitonicity of predictablePart. The only related results are Mathlib's Submartingale.monotone_predictablePart and Submartingale.expected_stoppedValue_mono (real, inequality form) and LMLExplore's real Supermartingale.measure_exists_le_le (Probability/Martingale/Ville.lean), and this PR leaves them unchanged.

What remains in Layer 2.3 after this PR: the randomized form [RM26, Corollary 4.1.1], the sharp curved-boundary bound [KPL25, Theorem 2.1], and re-deriving LMLExplore's real Supermartingale.measure_exists_le_le from the new ℝ≥0∞ inequality through the bridge.

Local checks (tauceti-local-checks verify --policy ordinary, not CI) passed: scope: scoped: against 13fc17b, whole-library lake build --iofail green, local-axioms: checked 2 changed module(s), 29 declaration(s); 0 violation(s), plus module-system, header-style and environment lint. The shared memory gate on this host was stalled, so the build ran with PATH/LEAN pointing directly at the pinned toolchain.

🤖 Prepared with Claude Code

[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	The exact Ville identities (with and without horizon), the equality case, the extended Ville inequality and the test-supermartingale Ville inequalities match dlP+26 Thms 1/4, WR23 Thm 4.1 and the roadmap shape; the decrease ofReal(A m - A n) with A = predictablePart of toReal M is a.s. the sum of M_k - E[M_{k+1}|F_k], and the edge cases (b = 0, b = ∞, c = ∞, α ∈ {0, ∞}) are handled non-vacuously. The capped process M ⊓ c is a genuine supermartingale via IsENNSupermartingale.inf, and the hypotheses (finite P, finite ∫⁻ M 0) are exactly those the identity requires.
✅	reuse	approved	claude/claude-opus-5-5	No existing Mathlib or LMLExplore declaration covers the ℝ≥0∞ exact Ville identity, exact optional stopping, the extended Ville inequality, or the supermartingale counterparts of the predictable-part lemmas. The proofs reuse the relevant Mathlib API (stoppedValue_sub_eq_sum', setIntegral_condExp, tendsto_measure_iUnion_atTop, monotone convergence).
✅	scope	approved	claude/claude-opus-5-5	This PR delivers the exact Ville identity with and without a horizon, plus Ville's inequality, its conditional/extended form and its equality case, which are the targets of EValues Layer 2.3 (README.md:504-516). The helper lemmas in Centering.lean and StoppedValue.lean are direct prerequisites used in ExactVille.lean, so the PR is a single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The module docstrings credit the papers the work follows (dlP+26, Theorems 1 and 4; WR23, Theorem 4.1; Vil39; RW, Fact 7.6), with references matching the roadmap's bibliography, and the supermartingale lemmas in Centering.lean name the Mathlib results they mirror. No uncredited source or vendored material found, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The public surface matches the Layer 2.3 roadmap products, and the general infrastructure (stopped Doob decomposition, antitone predictable part, truncated-time limits) is public in its canonical files. The private helpers are proof-specific, no bodies are exposed and no compatibility layer is added.
✅	generality	approved	claude/claude-opus-5-5	Statements sit at the natural level: the Doob-decomposition identity is Banach-valued with no adaptedness, the exact Ville identities are stated from any time m on any ℱ m-measurable set with the m = 0 forms derived, and the Ville inequalities come from the extended inequality rather than being re-proved. Assumptions (finite measure, finite initial expectation, c ≠ ∞, sigma-finite filtration) are each used.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration is in its natural home: the general Doob-decomposition and antitone-predictable-part lemmas sit in Probability/Martingale/Centering.lean, matching Mathlib's file; the generic monotone-convergence lemmas sit in Process/StoppedValue.lean; and the exact Ville identity sits in Probability/Martingale/ExactVille.lean, where the EValues roadmap's suggested homes put it. No import is unused or too broad, and Ville.lean and ExactVille.lean do not share a leading CamelCase component, so the flat-siblings rule does not apply.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions and follow Mathlib precedent (Submartingale.condExp_sub_nonneg/monotone_predictablePart) and the roadmap's Suggested.lean shapes (measure_exists_le_le, measure_exists_inv_le_le); _iff/_eq suffixes match statement strength and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Both new modules open with accurate module docstrings, and every public theorem is documented with a description of its statement that matches the Lean statement without overclaiming. References agree with the roadmap's bibliography.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are readable and commented, and the shared steps are factored into helper lemmas (setLIntegral_stoppedValueLimsup_hittingAfter, tendsto_setLIntegral_natCast_lt, the two new StoppedValue lemmas); I found no undocumented change/show or reliance on accidental definitional equality. The only direct projection on a stopping-time σ-algebra (hs.2 k) matches Mathlib's own usage in Stopping.lean.

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

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

[RemyDegenne]

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

The exact Ville identity, the predictable-part lemmas and the ℝ≥0∞ Ville inequalities are new material; the one duplication is natCast_le_hittingAfter, a public cast-only wrapper around Mathlib's le_hittingAfter.

• LMLExplore/Probability/Process/HittingTime.lean:32 — natCast_le_hittingAfter restates Mathlib's le_hittingAfter, changing only the cast WithTop.some n to (n : WithTop ℕ). It is a thin wrapper added as a new module and is used only twice. Fix: Delete HittingTime.lean and its import in ExactVille.lean, and at ExactVille.lean:216 and :311 pass (fun ω ↦ (Nat.cast_withTop m).trans_le (le_hittingAfter ω)) in place of natCast_le_hittingAfter.

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 · 52s · 358.1k in (326.3k cache read, 31.8k cache write) / 4.7k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}