[RemyDegenne]

This PR proves the tie-breaking step of perturbed model-based planning [LWCGC24, Lemma 6]. It adds an independent random perturbation ζ to the rewards of an MDP with transition kernel P and deterministic rewards r. With probability at least 1 - δ, the optimal action values of any two distinct actions at every state then differ by more than a polynomially small margin, so every state has a unique optimal action that beats every other action by more than that margin.

Roadmap: ReinforcementLearning

Milestone: Layer 15.4 (c), [LWCGC24] Theorem 1 (perturbed plug-in). Its proof combines Lemma 6 (the separation event B_ω for the optimal policy π̂_p of (P̂, r_p)) with Lemmas 3–5 (the (s, a)-absorbing MDPs and the net over u) and Lemma 2, which is already on main from #372. After this PR, Theorem 1 still needs the (s, a)-absorbing MDP comparison (Lemma 3), the net argument showing that π̂_p is the optimal policy of one of finitely many absorbing MDPs that do not depend on the samples at (s, a) (Lemma 4), and the assembly (Lemma 5 and the theorem).

Contents:

• MarkovDecisionProcess/Basic.lean: Learning.MDP.ofDet P r hr, the MDP with transition kernel P and deterministic rewards r (roadmap Layer 15 uses M.R = Kernel.deterministic r _; this is the (P, r_p) and (P̂, r_p) of the source), with ofDet_P, ofDet_R, the simp lemma meanReward_deterministic and ae_abs_ofDet_R_le.
• MarkovDecisionProcess/Simulation.lean: optQValue_le_optQValue_of_meanReward_le and optValue_le_optValue_of_meanReward_le. For two MDPs with the same transition kernel, optimal action values and optimal values are monotone in the mean rewards. They are corollaries of the componentwise lower bound le_optQValue_sub_optQValue and sit next to it.
• MarkovDecisionProcess/Optimality.lean: Learning.MDP.integrable_optValue, the integrability of v* for every finite measure. It replaces the repeated integrable_of_abs_le (measurable_optValue hγ hR) (abs_optValue_le hγ hR) _ term, including the existing occurrences in Optimality.lean (qValue_le_optQValue, optQValue_sub_qValue_le_of_optValue_sub_value_le) and ActionElimination.lean (optQValue_lt_optValue_of_lookahead_lt), as the proof-quality review asked. These are proof-only rewrites, and no statement changes.
• MarkovDecisionProcess/TieBreaking.lean (new), deterministic part, for any measurable state space with finitely many actions:
  • raising the reward at a pair p raises v* by at most the increase D of Q* at p, and raises Q* at every other pair by at most γ D;
  • the gap Q* p - Q* q grows at rate at least 1 - γ in the reward at p (mul_meanReward_sub_le_optQValue_sub_sub_optQValue_sub). This single monotonicity statement replaces the source's phase-transition claim (95). It also fixes a slip in the source's proof of Lemma 6, which claims Q*(s, a₁) - Q*(s, a₂) > ω for both orders of a₁ ≠ a₂; the statement here uses |·|;
  • optQValue_add_lt_optValue_of_forall_lt_abs_optQValue_sub turns pairwise separation into the source's form: the optimal action is unique and beats every other action by more than ω.
• MarkovDecisionProcess/TieBreaking.lean, probabilistic part, for finite 𝓢 and 𝓐:
  • continuous_optQValue_ofDet: Q* is continuous in the rewards;
  • le_measureReal_pi_forall_lt_abs_optQValue_ofDet_sub: for independent perturbations whose laws have densities at most L, the separation is δ (1 - γ) / (2 L S A²);
  • le_measureReal_pi_cond_Icc_forall_lt_abs_optQValue_ofDet_sub: for ζ p uniform on [0, ξ], the separation is ξ δ (1 - γ) / (2 S A²), better than the source's ξ δ (1 - γ) / (3 S A²), for every δ ≥ 0.
  • The kernel P is arbitrary and fixed. The source's "unchanged for (Q̂*_p, π̂*_p)" is the instance P = P̂ given the samples, which the perturbation is independent of. Integrating over the samples is left to the Theorem 1 PR.
• MeasureTheory/Constructions/Pi.lean: Measure.pi_le_of_forall_measure_update_preimage_le. Under a product of probability measures, a measurable set whose lines along one coordinate all have measure at most c has measure at most c. It is proved from Tau Ceti's TauCeti.measurePreserving_update_prod_pi.

No declaration is removed or renamed. Sources: [LWCGC24] = G. Li, Y. Wei, Y. Chi, Y. Gu, Y. Chen, Breaking the sample size barrier in model-based reinforcement learning with a generative model (arXiv:2005.12900), Lemma 6 and Appendix B.5, cited in the module docstring. No Mathlib material is vendored.

Local checks only (tauceti-local-checks verify --policy ordinary); CI verifies the pushed PR. scope: scoped: against 34d96f1b8f111131d1e459ccaf61245f0e5ea285; whole-library lake build --iofail green (Build completed successfully (8549 jobs).); local-axioms: checked 6 changed module(s), 170 declaration(s); 0 violation(s); module-system, header-style and local-lint pass.

🤖 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 statements match [LWCGC24, Lemma 6]: the union-bound constant is correct, independence is modelled as a product measure, the density hypothesis has a uniform witness, and the deterministic monotonicity lemmas have the right directions. I tried to show that some statement is vacuous, too weak or mis-quantified and failed.
✅	reuse	approved	claude/claude-opus-5-5	The new declarations (the deterministic-reward MDP constructor, reward monotonicity of Q* and v*, the one-pair reward bounds, the product-measure line bound and the tie-breaking theorems) have no existing counterpart in Mathlib or LMLExplore; the episodic EpisodicMDP.ofDet is a constructor for a different structure. The proofs reuse the existing simulation lemmas, Tau Ceti's measurePreserving_update_prod_pi and one_sub_le_measureReal_compl_iUnion, and integrable_optValue replaces the repeated integrability term at all existing call sites.
✅	scope	approved	claude/claude-opus-5-5	The PR proves [LWCGC24] Lemma 6, a direct step of the RL Layer 15.4 (c) target (Theorem 1, perturbed plug-in, README.md:1402), and every helper it adds is used in that proof. The integrable_optValue rewrites only replace a repeated term with the new helper; together it is one coherent topic that moves the target forward.
✅	attribution	approved	claude/claude-opus-5-5	The central source [LWCGC24] (arXiv:2005.12900, Lemma 6 and Appendix B.5) is cited with a full reference in the module docstring and the main theorem docstrings, its bibliography key exists, and the departures from its proof are stated. The other additions are routine or are corollaries of results whose sources the code already credits.
✅	api-design	approved	claude/claude-opus-5-5	The new surface is minimal and fully characterized: ofDet keeps its body hidden, its rfl-proved simp lemmas plus meanReward_deterministic give simp access to its mean reward, and the general product-measure bound is public in MeasureTheory/Constructions/Pi.lean. The private helpers serve only this proof, and there is no compatibility layer.
✅	generality	approved	claude/claude-opus-5-5	The density-bounded tie-breaking theorem is the general form and the uniform case is derived from it; the deterministic monotonicity results hold on any measurable state space with finitely many actions, and the product-measure lemma sits at general measure-theory level. No unused or too-strong assumptions, special-case duplication, or speculative abstraction found.
✅	placement	approved	claude/claude-opus-5-5	Every new declaration sits in its natural home: ofDet in Basic, integrable_optValue in Optimality, the monotonicity corollaries next to le_optQValue_sub_optQValue in Simulation, the product-measure line bound in Constructions/Pi, and the Lemma 6 material in a new file in the MarkovDecisionProcess directory. Every new import is used and none is overly broad.
✅	naming	approved	claude/claude-opus-5-5	Learning.MDP.ofDet and its ofDet_P/ofDet_R simp lemmas match the existing episodic ofDet construction (Episodic/Basic.lean:102), and the other new names describe their conclusions in the file's optQValue/optValue/meanReward vocabulary. No name claims more than its statement proves, and the PR adds no notation.
✅	documentation	approved	claude/claude-opus-5-5	The prior uniqueness overclaim is fixed: the docstring and the Main statements entry now require 0 ≤ ω before promising a unique optimal action. The module and declaration docstrings in TieBreaking.lean, Basic.lean, Simulation.lean, Optimality.lean and Pi.lean accurately describe their statements.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, commented where non-trivial, close with robust automation (linarith, field_simp, gcongr, positivity), and contain no change/show or undocumented defeq. The repeated integrability term is factored into integrable_optValue and the pointwise reward comparison into meanReward_le_of_eq_of_ne.

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

_{Reviewing this diff at head 37b1c6e. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.30.}