chore(toolchain): pin the patched Lean v4.34.1

[hyperpolymath]

Follow-up to the CodeRabbit review on #36 (thread on lean-toolchain, flagged Major / security): pin v4.34.1, the patched release of the 4.34 line.

Verified against the primary source, not the bot's summary

git log v4.34.0..v4.34.1 in leanprover/lean4 shows:

• three runtime reference-count fixes:
  • fix: preserve sticky counts in deletion cascades leanprover/lean4#15241: preserve sticky counts in deletion cascades
  • fix: mark the children of objects whose single-threaded count overflowed leanprover/lean4#15288: mark the children of objects whose single-threaded count overflowed
  • [Backport releases/v4.34.0] fix: panic instead of wrapping counts in sharecommon_quick_fn leanprover/lean4#15307: panic instead of wrapping counts in sharecommon_quick_fn
• a BitVec.ofNatClamp backport
• chore: prepare release (5045d00, 2026-09-24)

marches checks only its own proofs, not untrusted input, so the practical risk was low. Still, this is a same-line patch bump, it costs nothing, and it keeps the estate's 4.34 soundness floor on the patched build.

Change

• lean-toolchain: v4.34.0 → v4.34.1
• README.adoc: the two version mentions
• STATE.adoc: a dated entry. The v4.34.0 results are now marked historical.

No source change.

Gates (v4.34.1)

$ rm -rf .lake && lake build
Build completed successfully (15 jobs).
$ grep -rnw sorry Marches/ Marches.lean ; echo $?
1
$ lake env lean Marches/BadGadget.lean
[(false, false), (true, true), (false, false), (true, true)]

Note on the stack

#38 (rung-3 docs) is independent of this PR. Both add a STATE.adoc entry at the top, so whichever merges second will need a trivial merge, which I'll handle.

CI here shows the same two pre-existing reds as main (CI startup_failure from actions.lock drift, and estate-audit from the cicd-suite pipefail bug). Both are diagnosed in #37.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX

---

Generated by Claude Code

[coderabbitai]

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 30 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: d72c1709-71ba-49d2-8cca-2663fecd3e71

📥 Commits

Reviewing files that changed from the base of the PR and between 9d3af1a and 8cc6be3.

📒 Files selected for processing: 3

• README.adoc
• STATE.adoc
• lean-toolchain

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[hyperpolymath]

estate-audit is red, but not because of this PR. It fails the same way on main and on #38, and this PR touches only lean-toolchain, README.adoc and STATE.adoc. The cause is in hyperpolymath/cicd-suite@5a10b72's Required Files Gate. Under bash -e -o pipefail, grep -vE … .github/CODEOWNERS | wc -l exits 1 on this repo's comment-only CODEOWNERS, so the step dies silently. Full reproduction is in #38. No fix exists yet; it belongs in cicd-suite. Not re-run, because it fails the same way every time.

CI (lake build) ends in startup_failure because actions.lock drifted in #34, the same as on main. Until gh actions-lock is re-run, the local gate output in the PR body is the build evidence.

---

Generated by Claude Code