chore: bump Lean toolchain to v4.32.2

[kim-em]

This PR bumps the Lean toolchain to v4.32.2, mirrors the one kernel change in the interval that lean4lean did not already have, and pins the legacy do elaborator in the four files whose proofs depend on the shape do notation elaborates to.

git log v4.31.0..v4.32.2 -- src/kernel lists exactly two commits, and the diff over that range touches only environment.cpp (1 insertion) and inductive.cpp (15 insertions, 3 deletions). Both are fixes, and both are covered:

• fix: kernel to check opaque values for fvars, in v4.32.1 and v4.32.2. It adds check_no_metavar_no_fvar(*this, v.get_name(), v.get_value()) to environment::add_opaque, between check_constant_val and checker.check. Lean4Lean.addOpaque now calls checkNoMVarNoFVar env v.name v.value in exactly that position.

• fix: missing check at kernel inductive declaration, in v4.32.2 only. Already mirrored on master: Lean4Lean/Inductive/Add.lean type checks the nested applications I Ds against the post-declaration environment, using Result.lctx for C++'s m_params_lctx, and Lean4Lean.Tests.NestedInductive pins that an ill-typed dropped parameter is rejected. No change needed here.

lean4lean had the #14498 bug verbatim rather than by loose transcription, so this is a real fix and not a formality. addOpaque runs checkConstantVal and the value's checkType inside a single M.run, so both share one TypeChecker.State exactly as the C++ kernel shares one type_checker. A type that beta-reduces to False but whose inference pushes a free variable through the local context leaves that variable's type in inferTypeI. The value can then name the variable: inference answers from the cache instead of the already popped local context, and the declaration is accepted with type False. The leaked variable is _kernel_fresh.2, the same name the lean4 test for this issue uses, because TypeChecker.State.ngen has the same prefix and starts at the same index.

Lean4Lean.Tests.OpaqueFVar pins both directions and discriminates the fix: with the checkNoMVarNoFVar line removed it fails with "opaque value containing a free variable was accepted", and with it present the build is clean.

Worth flagging separately, because it is live on master right now: the same hole exists in addTheorem and in the safe branch of addDefinition, where it is not a lean4 bug at all. add_theorem and add_definition have called check_no_metavar_no_fvar on the value for a long time, and lean4lean does not. The identical cache-priming declaration is accepted as a theorem and as a safe definition. Verify front-end declaration checking already adds both calls, so this PR deliberately leaves them alone rather than widening scope, but that PR is still a draft.

The remainder of the diff is not a kernel change. feat: make new do elaborator the default flipped backward.do.legacy to false in v4.32.0, which reshapes the terms do notation produces: join points become have __do_jp instead of the lets that extract_lets destructures, and if chains are inlined. Lean4Lean/TypeChecker.lean, Lean4Lean/EquivManager.lean and Lean4Lean/Verify/TypeChecker/Reduce.lean are affected because the Verify proofs pin the elaborated shape of the implementation, and Lean4Lean/Experimental/ShapeLogRel.lean because it proves things about Option-monad do/return definitions the same way. Each of those four files now sets backward.do.legacy true with a comment saying why. This keeps the elaborated implementation identical to v4.31.0, which is the conservative choice for a kernel, and it is the whole of the fix: the single pin in ShapeLogRel.lean cleared all 38 errors in that file. Migrating the proofs to the new elaborator is follow-up work and a much larger change, tracked in Migrate the Verify proofs off the legacy do elaborator, which each pin points at.

Also refresh the toolchain-pinned Lean.Level divergence link, whose claim is about the current toolchain, and make stringProof a theorem for the new linter.defProp. fix: align Lean/Level.lean and kernel/level.cpp normalization rules is still open, so that divergence note stands.

Validated with lake build, lake build Lean4Lean.Experimental, and both CI replay commands: lean4lean Init.Core checked 1036 declarations and lean4lean --fresh Init.System.IO checked 43721. No statement changes and no new sorrys.

🤖 Prepared with Claude Code