[RemyDegenne]

This PR adds the episode-level environments of ReinforcementLearning Layer 7.7 "Episodes as rounds". Each round of the interaction is a whole episode of an episodic MDP M with horizon H, started from an initial law μ.

LMLExplore/MarkovDecisionProcess/Episodic/Policy.lean adds the deterministic H-step policies Policy 𝓢 𝓐 H = Fin H → 𝓢 → 𝓐 of Layer 7.6, with measurability as a separate hypothesis. It also adds Policy.extend (the policy extended beyond the horizon), Policy.measurable_extend, Policy.extend_injective and Policy.toKernel π hπ, the deterministic Markov policy of π. EpisodicMDP.value_toKernel_fin connects these to the values on main.

LMLExplore/MarkovDecisionProcess/Episodic/EpisodeEnv.lean contains the rest:

• an episode of a Markov policy π : ℕ → Kernel 𝓢 𝓐 is the run of augMarkovPolicy π in M.augmented from μ.map (·, 0). M.statesLaw H μ π is the law of its state sequence and M.episodeLaw H μ π the joint law of its states and rewards, with map_fst_episodeLaw. Every run has these laws (hasLaw_statesLaw, hasLaw_episodeLaw);
• hasCondDistrib_obs_fst_add_one_states: along every run of π started at the step h₀, the state of round n + 1 has conditional law ∫ P_{h₀+n}(· | s_n, a) dπ_{h₀+n}(a | s_n) given all the past states s_0, …, s_n. This is the new mathematical content. It is proved from the run lemmas on main, by gluing the action and next-state kernels with LML's HasCondDistrib.compProd and integrating out the action;
• under M.statesLaw H μ π, the first state has law μ (hasLaw_statesLaw_zero), and the state of step h + 1 has the conditional law above given s_0, …, s_h (hasCondDistrib_statesLaw). The expected return of an episode is ∫ V^π_0 dμ (integral_sum_episodeLaw, from integral_sum_feedback_eq_integral_value);
• for finite 𝓢 and countable 𝓐: the kernels statesKernel M H μ and episodeKernel M H μ from H-step policies, and the environments statesEnv M H μ and episodeEnv M H μ, both Environment.bandit of those kernels. LML at the pinned version has no stationaryEnv; Environment.bandit ν is LML's stationary environment without observations. Also map_fst_episodeKernel ("forgetting the rewards maps its episode laws to those of statesEnv M H μ"), the run lemmas hasCondDistrib_feedback_statesEnv and hasCondDistrib_feedback_episodeEnv, and BPIAlg 𝓢 𝓐 H (Layer 19.1: an IdentAlg in statesEnv with an H-step policy as output).

Milestone: ReinforcementLearning Layer 7.7 "Episodes as rounds". This PR delivers its first three bullets: statesEnv M H μ, episodeEnv M H μ and the forgetting map. It generalizes the source's statesEnv M H s₁ to an initial law. Consumers: the open PR #298 (Layer 14.1) says that restating its episodic counts "inside statesEnv/episodeEnv waits for those environments (Layer 7.7)". Layer 14.2 ("In statesEnv, every round contains H visits") and Layer 14.6 (the KL decomposition in statesEnv) consume them too, and hasCondDistrib_statesLaw is the within-episode law that 14.2 and 14.6 read the visits from. What remains of 7.7 after this PR is its fourth bullet: for finite 𝓐, a stochastic Markov policy has the episode law of a random H-step policy.

Relation to the paper project and to open work. This is item R7 of the paper project. It also includes the Policy and Policy.extend part of R6, because R7 needs it. The rest of R6 is the iterated Markov property along an episode (stepLaw, hasCondDistrib_shiftRounds_stepLaw), which builds on the open PRs #295 and #297, so it is not here. For the same reason, the source's backward recursion stateSeqLaw_succ is not ported. The source derives hasCondDistrib_statesLaw from that iterated Markov property; here it is proved directly from the run lemmas on main, for stochastic Markov policies instead of deterministic ones, so it needs neither open PR. The transfer of a conditional law to an image measure is done inline in hasCondDistrib_statesLaw, not as a public lemma, because #297 adds that lemma (HasCondDistrib.of_comp_hasLaw). No open PR touches MarkovDecisionProcess/Episodic/. No public declaration is removed or renamed.

Source: adapted from the paper project RemyDegenne/Essakine2026Tight at commit 8fb2a20561a128c83e61e9fc0245b85b7d8d6ce4 (Apache 2.0), files Essakine2026Tight/ForLMLExplore/MarkovDecisionProcess/Episodic/Basic.lean and StepLaw.lean: Policy, Policy.extend, statesLaw, statesKernel, statesEnv, BPIAlg. Following the paper roadmap's note on R7, the environments take an initial law μ instead of a fixed initial state, and statesLaw is defined for Markov policies through augMarkovPolicy and Algorithm.markov instead of the source's augPolicy and policyMeasure. Both module docstrings credit the source.

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R7

🤖 Prepared with Claude Code

[RemyDegenne]

🟡 proof-quality — request_changes claude/claude-opus-5-5

Earlier findings on duplicated setup and on proofs closing by unstated definitional equality are fixed. One proof still relies on a long chain of named kernel rewrites.

• LMLExplore/MarkovDecisionProcess/Episodic/EpisodeEnv.lean:150 — comap_map_fst_snd_compProd_augmented still rewrites with Kernel.map_apply', Kernel.snd_apply', Kernel.compProd_apply and Kernel.comp_apply' in one rw, each with hand-built measurability arguments (measurable_fst ht, measurable_snd (measurable_fst ht)), before a 9-lemma simp. This breaks on any Mathlib rename or signature change. Fix: Let simp unfold the kernels (e.g. simp [Kernel.map_apply', Kernel.snd_apply', Kernel.compProd_apply, Kernel.comp_apply', ht, …] with measurability/fun_prop discharging the side goals). Or split it into small lemmas giving (κ ⊗ₖ η).snd.map Prod.fst applied at a point.

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 · 25s · 59.6k in (32.7k cache read, 26.9k cache write) / 1.9k 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	stale (re-run pending)	claude/claude-opus-5-5	The definitions and theorems state the intended episode laws, the within-episode Markov property and the expected return; nothing is vacuous, assumed instead of proved, or a placeholder. Junk values for a non-probability μ follow main's existing MDP.env convention, and every substantive statement requires IsProbabilityMeasure μ.
♻️	reuse	stale (re-run pending)	claude/claude-opus-5-5	No duplication found: the new definitions and lemmas (Policy, statesLaw, episodeLaw, statesEnv, episodeEnv) have no existing counterpart in LMLExplore and build on the existing API (value_deterministic_of_lt, augMarkovPolicy, Kernel.deterministic, Environment.bandit, HasCondDistrib.compProd); Mathlib has no Fin.snoc measurability lemma that would replace the private measurable_snocStates. LML sources were not in the checkout, so the absence of an LML-side duplicate is unconfirmed.
♻️	scope	stale (re-run pending)	claude/claude-opus-5-5	The PR delivers the first three bullets of ReinforcementLearning Layer 7.7 (statesEnv, episodeEnv and the forgetting map), together with the Layer 7.6 Policy definitions it needs and the one-line Layer 19.1 BPIAlg built on statesEnv. It is one coherent topic with a real roadmap path and does not duplicate main.
♻️	attribution	stale (re-run pending)	claude/claude-opus-5-5	Both new modules credit the prior formalization (entropy-mdp: URL, file, author, licence, which definitions were adapted and how they differ) and the paper [EV26], in the same style as the existing episodic MDP files. The roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The prior finding is fixed: statesKernel_apply and episodeKernel_apply now carry @[simp], so the feedback lemmas reduce to statesLaw/episodeLaw automatically. Every new definition has the lemmas that characterize it (run laws, the forgetting map, _def/_apply, measurability), the private helpers serve only this file's proofs, and Policy/toKernel hold no unused data.
♻️	generality	stale (re-run pending)	claude/claude-opus-5-5	Statements sit at the natural level: the laws and the within-episode conditional law are stated for stochastic Markov policies, and only the environments use deterministic H-step policies; each extra assumption (Nonempty 𝓢 for MDP.env, Nonempty 𝓐 for Policy.extend, Finite/Countable/MeasurableSingletonClass for measurable_of_countable on Policy) is needed. value_toKernel_of_lt is derived from the general value_deterministic_of_lt rather than re-proved.
♻️	placement	stale (re-run pending)	claude/claude-opus-5-5	Both new files sit in the existing MarkovDecisionProcess/Episodic/ directory, build only on earlier Episodic files (Value.lean, Basic.lean), and import only the LML modules they use (IdentificationAlg for IdentAlg, StationaryEnv for hasCondDistrib_feedback_bandit). No declaration is misplaced and no import is unused or overly broad.
✅	naming	approved	claude/claude-opus-5-5	The prior _of_lt misnomer is fixed: the lemma is now value_toKernel_fin, consistent with extend_fin. All other names describe their conclusions, sit in the same Learning.MDP.Episodic namespace as the adjacent episodic files, and the PR introduces no notation.
♻️	documentation	stale (re-run pending)	claude/claude-opus-5-5	Both new files have module docstrings that are accurate, credit their sources, and contain no process narrative; every public definition and main theorem has a docstring matching its statement.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	Earlier findings on duplicated setup and on proofs closing by unstated definitional equality are fixed. One proof still relies on a long chain of named kernel rewrites.

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

_{Reviewing this diff at head 1e7a915. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.90.}