feat: qualify dated Lean nightlies in CI

[ejgallego]

This PR adds reproducible qualification for dated Lean nightlies through a separate daily, pull-request, and manually triggered CI lane.

• Resolve one immutable nightly tag, validate it in an isolated checkout, and record its exact Lean/Lake identity with per-stage logs.
• Run runtime build, fast, LSP, bundle/save/replay, and mixed nightly/release workspace checks; upload the report on success or failure.
• Admit the nightly only in the temporary validation checkout, keeping the public validated-release registry unchanged.
• Isolate local Elan settings, mirror source edits and deletions, and replace prior report evidence when reproducing a run.