[DavidLedvinka]

Start the rebuild with two files under RandomDo/MeasurableSpaceMonad, so the polymorphic foundation can be reviewed as complete additions alongside the existing implementation.

• Core.lean contains the functor and monad operations, conditional laws, and derived lemmas from RandomDo/Monad/MeasurableSpace.lean. It corrects the simplifier and grind registrations to refer to the measurable space monad laws.
• Notation.lean contains the basic rdo adapter from RandomDo/Monad/Notation.lean, supporting binding, branching, mutation, and early return. ForIn interfaces and loop notation are deferred to a later file.

Both module docstrings include Main definitions and Notation sections. Core also explains the hierarchy and the omission of a general function-space Applicative interface, citing the unit-interval evaluation-map obstruction in Aumann's original Borel structures for function spaces (1961), §3, with a direct link to the unnumbered example before Lemma 3.1 in the author-hosted reprint. The explanation distinguishes measurability for each fixed continuation in bind from jointly measurable function application. The new declarations use the MeasureTheory namespace, with mapping, bind, and rdo notation enabled by open MeasureTheory (or open scoped MeasureTheory). The two rdo parsers have equal priority so elaboration can select the applicable monad interface. Legacy tests import their original modules explicitly to avoid ambiguity between the old global classes and the rebuilt classes. Importing either new module does not pull in the original monad classes, concrete Measure semantics, or sampling implementations.

Review Core.lean first, followed by Notation.lean. Review revisions are recorded in separate commits. The existing RandomDo target builds both modules, and the separate TestNext target checks polymorphic reasoning, basic notation, mutable state, and the import boundary. CI builds TestNext explicitly and accepts PRs targeting codex/rebuild-* branches for subsequent dependent PRs.

Validation:

• lake build --wfail RandomDo TestNext
• lake test (passes with the existing trace.computable style warning in Test/Computable.lean)
• lake lint
• lake exe mk_all --check