chore: Bump v4.32.0

[NicolasRouquette]

Version bump to Lean/Mathlib v4.32.0 — tracker #1437.

This is a toolchain bump. It repairs the source breakages from the Mathlib
4.31→4.32 API drift across Physlib, QuantumInfo, and PhyslibAlpha.
No lemma or definition statement — nor any mathematical content — is added,
removed, or changed. Only proofs, instance / structure-instance syntax, and
imports are touched.

lake build (both default targets) and lake build PhyslibAlpha are green;
lake exe lint_all, TODO_to_yml mkFile, stats mkHTML,
informal mkFile mkDot mkHTML, and make_tag all pass. README Lean badge
updated.

Breakage classes fixed

1. nsmul / zsmul field proofs in hand-rolled AddMonoid /
   AddCommMonoid / AddCommGroup instances — in 4.32 ring no longer closes
   scalar-multiplication (•) goals. The custom nsmul / zsmul data is
   kept unchanged; only the recursor obligations are repaired
   (Mathematics/RatComplexNum, SpaceAndTime/Space/Module,
   StringTheory/FTheory/SU5/Fluxes, QFT/PerturbationTheory/FieldStatistics,
   QFT/AnomalyCancellation).

2. Structure refactors (data unchanged, only repackaged):

   • MonoidAlgebra and MvPolynomial are now wrapper structs, no longer defeq
     to their coefficient Finsupp — unwrapped via coeff / .ofCoeff
     (QFT/PerturbationTheory/FieldOpFreeAlgebra,
     PhyslibAlpha/…/TwoHDM/Invariants).
   • ContRepresentation gained a toMonoidHom field — nested the existing
     toFun/map_one'/map_mul' inside it (…/EuclideanGroup/SchwartzAction).
   • Mathlib.Meta.Positivity.Strictness gained an Option PartialOrder index —
     13 positivity extensions guarded with the none-case short-circuit, exactly
     as Mathlib's own evalAdd now does (QuantumInfo/…/HermitianMat/Order,
     Sqrt, LogExp).
   • LeftOrdContinuous gained an s.Nonempty hypothesis — the proof now
     case-splits on it (QuantumInfo/ForMathlib/SionMinimax).

3. Tactic drift — fun_prop / measurability metavariable goals (pinned
   with named function args) and simp / simpa / convert normal-form drift
   (SpaceAndTime/Space/IsDistBounded, QuantumMechanics/Operators/Position,
   …/SpectralTheory/SpectralMeasure, Relativity/LorentzAlgebra/ExponentialMap,
   QFT/PerturbationTheory/WickContraction/*, and several
   QuantumInfo/ForMathlib/HermitianMat/* files).

4. Deprecation renames — Mathlib.LinearAlgebra.PiTensorProduct →
   …PiTensorProduct.Basic, IsOpen.locallyPathConnectedSpace,
   Finset.le_eq_subset (dropped from simp sets),
   TwoSidedIdeal.mem_ofRingCon, the removed simpVarHead linter attribute;
   and def → lemma for the propositions the defProp linter now flags.

Reviewer map

1. Config — lean-toolchain, lakefile.toml, lake-manifest.json,
   README.md.
2. Each file under classes 1, 3, 4 is an independent, mechanical repair; no
   file depends on another. These can be skimmed.
3. Closest look: the class-2 structure-refactor adaptations are the only
   non-mechanical changes — the two wrapper-struct fixes
   (FieldOpFreeAlgebra/Basic.lean's ofListBasis_eq_ofList,
   TwoHDM/Invariants.lean's realPart) and the positivity-extension
   migration (HermitianMat/Order.lean).

Scope note: pre-existing redundant_imports / unusedArguments lint findings
in files untouched by this bump are intentionally left as-is (lint_all exits
cleanly with them, as on master).

---

AI-assisted per the repository's AI policy; commit carries the
Co-authored-by trailer.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[nateabr]

Great work on your first PR!!

Incidentally I was also working on the bump, and our work seems to be quite similar (in some instances your fixes are better). I have provided some minor suggestions that might help.

[nateabr]

Suggested change

	⟨fun μS ↦ ⇑μS.toVectorMeasure⟩

[nateabr]

The break here is really this Coefun coercion and not the downstream lemmas, you should be able to revert them to how they were before after this suggestion. Please do double check.

[NicolasRouquette]

Applied in 978ce09

[nateabr]

Suggested change

	zsmul z p := ⟨fun i => z • p.val i⟩

With this change you should be able to drop the zsmul_zero' / zsmul_succ' / zsmul_neg' blocks below

[NicolasRouquette]

Applied in 978ce09

[nateabr]

Suggested change

	nsmul n f := ⟨n * f.M, n * f.N⟩
	nsmul n f := ⟨n • f.M, n • f.N⟩

Same idea as my previous comment, switching the operators make this proof more robust to the breakage that happened here.

[NicolasRouquette]

Applied in 978ce09

[nateabr]

Suggested change

	nsmul_zero f := Fluxes.ext_iff.mpr <| by
	refine ⟨?_, ?_⟩
	· show ((0 : ℕ) : ℤ) * f.M = 0
	simp
	· show ((0 : ℕ) : ℤ) * f.N = 0
	simp
	nsmul_zero f := Fluxes.ext_iff.mpr ⟨zero_nsmul f.M, zero_nsmul f.N⟩

[NicolasRouquette]

Applied in 978ce09

[nateabr]

Suggested change

	refine ⟨?_, ?_⟩
	· show ((n + 1 : ℕ) : ℤ) * f.M = (n : ℤ) * f.M + f.M
	push_cast; ring
	· show ((n + 1 : ℕ) : ℤ) * f.N = (n : ℤ) * f.N + f.N
	push_cast; ring
	nsmul_succ n f := Fluxes.ext_iff.mpr ⟨succ_nsmul f.M n, succ_nsmul f.N n⟩

[NicolasRouquette]

Applied in 978ce09

[NicolasRouquette]

Thanks so much for the review, @nateabr — these were all spot-on and made the diff noticeably cleaner. Applied all five in 978ce09:

• SpaceAndTime/Space/Module.lean — switched zsmul to z • p.val i; with that the default zsmul_zero' / zsmul_succ' / zsmul_neg' proofs discharge, so I dropped those blocks.
• StringTheory/…/Fluxes/Basic.lean — switched nsmul to n • f.M / n • f.N and closed nsmul_zero / nsmul_succ with zero_nsmul / succ_nsmul.
• QuantumMechanics/…/SpectralMeasure.lean — you were exactly right that the CoeFun coercion was the real break. Using ⇑μS.toVectorMeasure lets comp_of_disjoint, comp_eq_of_inter, and commute go back to their original forms verbatim — the file now differs from master by just that one coercion line.

Full lake build is green (9235 jobs) and the style/declaration linters pass. Thanks again for the careful and constructive review — much appreciated!

[jstoobysmith]

Hi @NicolasRouquette! Many thanks for this PR. It looks great. There are some linter issues which need fixing (see the workflows) before we can merge this.

awaiting-author

[NicolasRouquette]

Fixed in 60528a6.

The three runPhyslibAlphaLinters unusedArguments reports are all in PhyslibAlpha/QuantumMechanics/StinespringDilation.lean, which this PR doesn't touch — it's unchanged since the 4.31 bump. So the bump is what surfaces them. The check is green on master (4.31), which means the linter counted these arguments as used there; under 4.32 it doesn't. I didn't chase down the exact 4.32-side change, but either way they're genuinely redundant — none of the operations these lemmas call requires them:

• tr₂_e₀Xe₀ — [Zero w]: tr₂ needs only [Fintype n] on the traced index.
• tracefree_version — [Zero r], [DecidableEq m]: (1 : Matrix r r R) needs [DecidableEq r] plus Zero/One R (from RCLike R), not Zero r; stinespringForm needs [Fintype r] [DecidableEq r] [Fintype m], not [DecidableEq m].
• stinespringOp_apply — [Fintype m], [DecidableEq m]: stinespringOp needs only [Fintype r] [DecidableEq r].

One thing CI didn't surface: after dropping those, a fourth declaration, heisenberg_schrõdinger, comes up with the same [Zero r]/[DecidableEq m]. It was masked because its proof is rw [tracefree_version] — while tracefree_version still required those instances, they counted as used in the caller. Once it doesn't, they're dead there too, so I removed them in the same commit; otherwise it'd just fail on the next run.

runPhyslibAlphaLinters passes cleanly locally now. The Style linters run on the new commit is waiting on a maintainer to approve workflows — mind kicking it off?

[NicolasRouquette]

Pushed c85984a to green the runLinter on Physlib step.

The failure was toolchain collateral, not a source change. The v4.32.0 #lint linters (unusedArguments, checkType) are stricter than v4.31.0's and flag 5 pre-existing declarations this PR doesn't touch — 4 are in files untouched by the bump, and the 5th (ChargeSpectrum/Basic.lean) is only edited at subset_trans (L187), not at the flagged min_exists_inductive (L333). The same CI step is green on master (still v4.31.0).

Consistent with this PR's charter (a toolchain bump — no lemma/definition statement or signature added, removed, or changed), the findings are silenced, not restructured; dropping the now-"unused" binders would alter public signatures and risk downstream breakage. The fix adds:

• @[sorryful, nolint checkType] on leviCivita_contract_self — whnf on its tensor-notation statement now exceeds the linter's 200k-heartbeat budget.
• @[nolint unusedArguments] on min_exists_inductive, lightlike_spatial_parallel_implies_proportional, integrable_spherical_of_integrable, and probability_nonneg (matching 17 existing uses in the tree).

Each carries an inline comment; the commit message has the full breakdown.

Verified locally with the exact CI command — env LEAN_ABORT_ON_PANIC=1 lake exe runPhyslibLinters reports Linting passed for Physlib / Linting passed for QuantumInfo (0 findings), and lake build -KCI is green.

The re-triggered workflows are sitting at action_required (fork PR) — could a maintainer hit Approve and run? Thanks!

[nateabr]

I have run the workflows.

FYI when you are ready for your PR to have another look, please comment (-)(awaiting-author) without the brackets. This removes the awaiting author tag and helps the maintainers keep track as they get far too many notifications from github.

[NicolasRouquette]

-awaiting-author