chore: bump toolchain to v4.35.0-rc3

[kim-em]

This PR follows TauCeti to v4.35.0-rc3.

lean-eval downloads TauCeti's published build outputs rather than compiling TauCeti, and Lake only reuses them when this project pins the same toolchain and Mathlib revision as the pinned TauCeti commit. So those move together: TauCeti to 522706e83ca349c3d6bde045e56778d17354ae8d, Mathlib to the 5e0c4e5239cb0a2d86d68a884bf52cfd963fce22 that commit uses, and the toolchain to v4.35.0-rc3. That TauCeti commit is the most recent on main whose build had finished, so its outputs are published.

The explicit Cli require goes away and Cli comes transitively from Mathlib. It was pinned here at exactly Mathlib's revision, so when Mathlib's Cli moved the two disagreed and lake exe cache get computed wrong hashes, reporting mathlib: failed to fetch cache. Taking it transitively resolves to the same commit but via Mathlib's own tag, so they cannot drift apart again.

lean-eval-generator is repinned at a61cd80bc45b16c4f8f900a15f5c80f32e75aad6, the merge of leanprover/lean-eval-generator#10 "fix: use the String API that survives v4.35.0-rc3". v4.35.0-rc3 removes String.trim and String.dropRight, and a Lake dependency builds with the root project's toolchain, so without that fix the lean-eval executable does not build here even though the generator pins v4.33.0 itself.

Six catalog modules need adapting. Five of them pass a coefficient category to singularHomologyFunctor or singularChainComplexFunctor and leave its universe to be inferred from the coefficient object; at this toolchain, instance search for ∀ J, HasColimitsOfShape (Discrete J) C runs while that universe is still a metavariable, and searching with one exhausts the 20000 synthInstance heartbeats. Each now writes the universe its coefficient object already forces: ModuleCat.{0} ℝ, ModuleCat.{0} ℤ, AddCommGrpCat.{0}. The sixth, HoneycombConnectiveConstant.walkCount_six, reduces a Decidable instance over all 3 ^ 6 direction words; elaborator reduction now needs 556236 heartbeats against a default of 200000, so it evaluates in the kernel instead, which costs 37538 heartbeats and half the wall time and no longer needs the maxRecDepth bump.

generated/ is deliberately untouched. scripts/generate_projects_external.py reads the root lean-toolchain, and regenerate-main.yml triggers on merge to main when that file changes, so the project toolchains follow from the trusted regenerator rather than from a hand edit here.

Verification: scripts/fetch_dependency_caches.sh --restore . passes, which is the check that matters for the pins, since it treats a TauCeti cache miss as an error rather than a silent rebuild. lake exe lean-eval check-problem-build reports the whole catalog clean aside from the expected sorry warnings; that is the run to trust, because the problem modules sit outside the LeanEval library target and lake build LeanEval never reaches them. lake build LeanEval EvalTools and lake build lean-eval are also clean, and the three lake exe lean-eval validators CI runs (validate-manifest --structure-only, validate-generated-catalog, validate-submission) all pass.

🤖 Prepared with Claude Code