chore: bump Lean toolchain to v4.33.0-rc2

[kim-em]

Summary

• bump Lean and Batteries from v4.32.2 to v4.33.0-rc2
• mirror every applicable kernel hardening change in the release range
• adapt the verification and experimental libraries to rc2's API/elaboration changes
• add executable regressions for the new kernel invariants

This is directly stacked on the merge commit of #30. We are intentionally tracking the release candidate rather than master; the original plan to track master became unnecessary once v4.33.0-rc2 was available.

Kernel audit

Audit command:

git log --format='%h %s' v4.32.2..v4.33.0-rc2 -- src/kernel

It identifies 14 commits. The two first landed on both release branches under different cherry-pick hashes, so they appear in this range even though #30 already audited them.

Upstream	Assessment and corresponding evidence
d8b1897832 / #14633, check binder types before extending the local context	Already matched: inferLambda and inferLet call ensureSort before withLocalDecl. The now-stale binder-order entry was removed from divergences.md.
be0966703b / #14632, harden kernel invariants	Added all four Quot name checks; duplicate-name validation for mutual blocks; structure-name validation in projection reduction; exception-producing nested restoration in place of assertions. Projection indices are Lean Nats throughout lean4lean, so there is no narrowing boundary to guard; regressions exercise 2^32 as both stuck during reduction and rejected during inference.
1bb3bcfdad / #14631, compare projection structure names	EquivManager.isEquiv and TypeChecker.isDefEqCore' now compare structure name and index; the corresponding verification proofs were updated. Tests cover valid reduction, wrong-name non-reduction/non-equivalence, and oversized indices.
792b3a6d69 / #14621, recheck nested-inductive output	Restored constructor types are checked in the final environment under declaration level parameters. Every restored recursor type and rule RHS is checked under that recursor's own level parameters. Existing aux2nested checks remain under the elimination local context.
39f44348a1 / #14616, reserve _nested names	Original inductive and constructor types are scanned before elimination; both Expr.const names and Expr.proj structure names below _nested are rejected. Both forms have regressions.
303a57ceb5 / #14615, normalize inductive-predicate decisions	The three native-kernel sites correspond to checkConstructors, isLargeEliminator, and isKTarget; all now use isAlwaysZero. The Sort (imax 1 0) regression confirms no large-elimination universe is introduced.
c8f4a42ded / #14613, normalize Prop recognition	lean4lean's isProp already used normalized level reasoning. The divergence documentation now describes only lean4lean's deliberately more conservative uncertain-level behavior. The same imax regression covers this classification.
189dc27892 / #14608, mutual universe parameters	addMutual requires every member to have the first member's exact level-parameter list. A mismatched block and a valid control are tested.
b4e8db15bb / #14607, reject fvars/mvars before nested elimination	Original inductive and constructor types are validated before ElimNestedInductive.run, preventing elimination from hiding either kind. Both paths have regressions.
f839b65ba4 / #14577, missing nested-inductive declaration check	Already audited in #30 and retained: nested applications are checked against the post-declaration environment, covered by Lean4Lean.Tests.NestedInductive. The broader #14621 rechecks now add another defensive layer.
472f5c03e9 / #14498, opaque values containing fvars	Already implemented and tested in #30. Lean4Lean.Tests.DeclFVar continues to cover definition, theorem, and opaque value paths, including valid controls.
85e209a57b / #13956, deterministic maxRecDepth	lean4lean already has deterministic explicit fuel for mutually recursive checker calls and structurally recursive loops. FuelConfig and divergences.md now explain the mapping; a regression checks low-fuel failure and high-fuel success.
9ebb35b4af / #14203, delete unused C++ code	No Lean implementation analogue and therefore no source change.
fa69f38200 / #14094, use std::optional	C++-only representation refactor; lean4lean already uses Option, so no source change.

I also inspected the Lean-level Level, Expr, and Declaration changes. The universe algorithm itself is unchanged in this range; the relevant non-kernel compatibility changes are the Lean.Nat.imax namespace move and rc2's split implicit_reducible transparency behavior. The latter required marking erased/index-only aliases so implicit argument checking can unfold them without changing typeclass synthesis behavior.

Validation

• lake build — 148 jobs
• lake build Lean4Lean.Experimental — 68 jobs
• lake build Lean4Lean.Tests.KernelHardening
• lake exe lean4lean Init.Core — checked 1,035 declarations
• lake exe lean4lean --fresh Init.System.IO — checked 43,609 declarations
• git diff --check
• no added sorry declarations