v4.32.0

v4.32.0

This release upgrades SLT to Lean and Mathlib v4.32.0 and updates the formalization for the corresponding API changes.

Highlights

• Pins lean-toolchain, lakefile.lean, and lake-manifest.json to Lean 4.32.0 and Mathlib v4.32.0.
• Updates Gaussian Sobolev cutoff measurability and Gaussian Poincare mapped-integral proofs for v4.32.0 elaboration changes.
• Updates Hanson-Wright and random-matrix measurability proofs by making pointwise multiplication and negation explicit.
• Updates tensorized Gaussian log-Sobolev measurability proofs and removes an obsolete simplification argument exposed by the v4.32.0 linters.
• Refreshes the project README and adds the repository license while preserving the existing formalized statistical-learning and random-matrix development.

Verification

• LEAN_NUM_THREADS=$(nproc) lake build completed successfully.
• Scanned SLT/ for sorry, admit, axiom, and native_decide; none were found.