[RemyDegenne]

This PR proves that the trajectory of a stationary policy is a Markov chain, for every run of Algorithm.markov fun _ ↦ π (π : Kernel 𝓢 𝓐 a Markov kernel) in M.env μ from a probability measure μ. The round (s, a, r) is drawn from stateRoundKernel M π s = δ_s ⊗ₘ (π ⊗ₖ M.R), and the next round from roundKernel M π r. hasLaw_trajectory_markovChainLaw says the rounds have path law markovChainLaw (stateRoundKernel M π ∘ₘ μ) (roundKernel M π). It follows from Tau Ceti's hasLaw_markovChainLaw_iff and the step kernels of the run (stepKernel_markov_env_zero, stepKernel_markov_env_add_one). Three consequences follow, each through Tau Ceti's Markov property (HasLaw.prefix_processShift_markovChainLaw):

• the Markov property of runs, hasCondDistrib_processShift_history: given the rounds before n, the rounds from n on are a trajectory of π started from the law (M.env μ).obs n of the next state. Given also the state s of round n, they have law trajKernel M π s (hasCondDistrib_processShift_history_obs);
• the states form the chain markovChainLaw μ (M.stateKernel π) (hasLaw_obs_markovChainLaw);
• the state-action pairs form the chain markovChainLaw (μ ⊗ₘ π) (M.saKernel π) (hasLaw_obs_action_markovChainLaw).

The trajectory law from a state is the kernel trajKernel M π. It equals trajMeasure from δ_s (trajKernel_apply_eq_trajMeasure, trajMeasure_markov_env). For a deterministic policy it is MDP.policyMeasure (policyMeasure_eq_trajKernel, through policyAlg_eq_markov), which is therefore measurable in the initial state (measurable_policyMeasure).

Target: ReinforcementLearning, Layer 7.2 "Markov policies". This PR proves two of its bullets: "Under a stationary policy π in M.env μ, prove that the state process is a Markov chain with kernel M.stateKernel π: its law is Tau Ceti's markovChainLaw μ (M.stateKernel π)", and "Prove that the state–action process is a Markov chain with kernel M.saKernel π … and initial law μ ⊗ₘ π". The other two bullets (Algorithm.markov and policyAlg_eq_markov) are already on main. After this PR, every bullet of Layer 7.2 is on main. Next comes Layer 7.6's iterated Markov property along an episode: the paper's item R6 (hasCondDistrib_shiftRounds_stepLaw) uses hasCondDistrib_processShift_history_obs in M.augmented.

Placement. Three general facts go in their topic files:

• ProbabilityTheory.HasCondDistrib.prodMkLeft_of_comp (Probability/HasCondDistrib.lean): from a conditional law η ∘ₖ κ given X, where f reads off Z the point η draws from, get the conditional law η (f Z) given (X, f Z). The hypothesis is the joint-law form η.map (fun z ↦ (f z, z)) = Kernel.id ×ₖ η, so no measurable singletons are needed on 𝓢;
• ProbabilityTheory.Kernel.markovChainKernel_map_prodMk_eval_zero and Kernel.markovChainKernel_map_shift (Probability/MarkovChain/MarkovProperty.lean), the kernel forms of Tau Ceti's time-0 Markov property and of markovChainLaw_map_shift_iterate at one step;
• Learning.MDP.feedbackZero_env (MarkovDecisionProcess/Basic.lean, next to obsZero_env).

The new file is MarkovDecisionProcess/Trajectory.lean. It is not MarkovChain.lean, so that it does not share a prefix with MarkovPolicy.lean. The HasCondDistrib.lean additions sit after ae_mem, away from the lines that the open PR #288 edits. No public declaration is removed or renamed.

Source: adapted from the paper project RemyDegenne/Essakine2026Tight at commit 9c77165d56f81c1db7a9835068356bb14886a3be (Apache 2.0), file Essakine2026Tight/ForLMLExplore/MarkovDecisionProcess/Markov.lean. There, the Markov property hasCondDistrib_shiftRound_trajMeasure is proved for deterministic stationary policies, by rebuilding the trajectory and using the uniqueness of the Ionescu–Tulcea law (policyKernel, shiftMeasure, consRound). Following its PAPER_ROADMAP.md note on R5, this port states it for stochastic stationary Markov policies. It is proved instead from Tau Ceti's Markov chain theory, so the source's reconstruction machinery is not ported. The module docstring credits the source.

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R5

🤖 Prepared with Claude Code