[DavidLedvinka]

Adapted Lean core definitions can diverge without breaking compilation. This tags 25 analogues in RandomDo/Monad/MeasurableSpace.lean and RandomDo/Monad/Notation.lean and adds GitHub Actions checks for changes to their core counterparts.

The library contains only a lightweight @[analogue ...] attribute and its annotations. The attribute imports Lean.Attributes, resolves declaration names, and stores metadata. It has no dependency on the maintenance tooling.

All maintainer code, data, tests, and documentation live in .github/upstream/:

• The Lean exporter obtains declaration source locations and checks that this workflow's origins belong to Lean core.
• baseline.json records an exact core commit and source range per mapping. The Python checker uses Git diffs to identify changes. Maintainers explicitly advance selected baselines after review, preserving unrelated baselines.
• PR CI compares against the project's pinned compiler. A weekly/manual workflow checks core's development branch and maintains one issue with a link to the full diff report. Unchanged relevant edits do not trigger repeated updates; failed checks leave the issue alone.

Normal library builds do not run these tools; this feature adds no Python or Node requirement to library builds. The scheduled workflow starts after merge to main. See .github/upstream/README.md for maintainer instructions.

The initial baseline is Lean v4.35.0. Existing declaration statements, bodies, and docstrings are unchanged. The maintainer guide records known differences in the existing randOps and loop adaptations. This detects source changes; it does not establish semantic equivalence or track unannotated helpers and surrounding context.

Validation:

• lake build --wfail, lake test, lake lint, and lake exe mk_all --check.
• Attribute tests and export/comparison of all 25 mappings against the pinned Lean commit.
• 19 offline Python tests and six mocked GitHub issue tests.
• Confirmed that the general attribute accepts non-core origins and the CI exporter rejects them.
• Parsed both workflows and exercised their relocated report/notification entrypoint with mocked APIs; checked baseline lookup when invoked outside the repository directory.