Bump to version: v4.34.0

[NicolasRouquette]

Bumps mathlib and doc-gen4 to v4.34.0 and the toolchain to leanprover/lean4:v4.34.0.

Closes #1656.

Both libraries build clean and every linter CI gates on passes:

	result
lake build	9590 jobs, 0 errors, 9 warnings
lake build PhyslibAlpha	9278 jobs, 0 errors, 11 warnings
check_file_imports, check_dup_tags, sorry_lint, runPhyslibLinters	pass
runPhyslibAlphaLinters, noAlphaImports, alphaFileImports	pass
scripts/lint-style.sh, scripts/PhyslibAlpha/alphaPythonLinters.sh	pass

Deprecation warnings in Physlib/QuantumInfo are down from 147 to 9.
All 20 remaining warnings are deliberate and listed at the end.

Four commits, in the order they are worth reading:

1. chore: Bump to Lean v4.34.0 — the bump and the mechanical port.
2. fix(PauliMatrices): prove leviCivita_mul_pauliDual via rational components
   — the only proof whose strategy changed; see below.
3. chore(PhyslibAlpha): port to Lean v4.34.0 — PhyslibAlpha is not in
   defaultTargets, so lake build never reaches it. It
   has its own CI workflow and needed its own port.
4. chore(PhyslibAlpha): clear the linter warnings v4.34.0 surfaced.

This bump touches 176 files, so every section below links its declarations, call
sites and warnings straight to source — the diff is wide but shallow, and the links
are there to spare reviewers the hunt. They resolve against this PR's head commit
(1bc0543) in this repository rather than the branch on my fork, so they
survive the merge and the branch's deletion and still work for anyone reading this
PR later. They pin the code as submitted; I will regenerate them if I force-push.

Checklist (#1656)

Basics

• mathlib rev → v4.34.0 in lakefile.toml
• doc-gen4 rev → v4.34.0 in lakefile.toml
• rm -rf .lake + lake update (lake-manifest.json)
• lean-toolchain updated to leanprover/lean4:v4.34.0
• Lean version badge in README.md

Build

• lake build
• lake build PhyslibAlpha (not in defaultTargets;
  gated separately by .github/workflows/alphaBuild.yml)

Scripts

• lake exe lint_all
• lake exe TODO_to_yml mkFile — blocked, and not by this
  PR; see below
• lake exe stats mkHTML
• lake exe informal mkFile mkDot mkHTML
• lake exe make_tag
• generated files removed again

Afterwards (mine to do, not in this PR)

• tag the new version
• Zulip bump notice

Reviewer map

1. lakefile.toml, lean-toolchain,
   lake-manifest.json, README.md — the bump
   proper.
2. Physlib/Relativity/PauliMatrices/Relations.lean — the one
   proof whose strategy changed; its own commit, see below.
3. Physlib/Mathematics/LinearPMap.lean — the one new lemma, and
   the only place this PR adds API rather than adapting to it.
4. The Module-instance files (§ Declarations added) — fourteen files, one
   mechanical change each: real and complex
   Lorentz vectors, the four Weyl fermions, the
   five Standard Model fermions, Dirac,
   FiniteHilbertSpace and ReferenceFrame.Vector.
5. …/HilbertSpaces/OneDimension/Basic.lean and
   …/TensorProducts/CompleteTensorProduct.lean — the two
   places where a physlib-facing signature or characterization changed, not just
   a proof.
6. Everything else is proof-body adaptation; the two API changes sections are
   the index.

Declarations added

No declarations were removed.

Declaration	File	Why
LinearPMap.toFun_ker_eq_bot_iff	Physlib/Mathematics/LinearPMap.lean	LinearPMap.ker is now mathlib's submodule-valued kernel, so inverse_apply_eq, inverse_range and inverse_closed_iff want f.ker = ⊥. Physlib's spectral theory says f.toFun.ker = ⊥ throughout; this bridges the two spellings once instead of at each of the 21 call sites — 7 in SpectralTheory/Basic.lean, 4 in Cayley/Basic.lean, 5 in Cayley/Inverse.lean, 2 in CayleySpectralData/Construction.lean and 3 in SpectralIntegral/SpecTheorem.lean.
Lorentz.ContrMod.toFin1dℝAddEquiv, Lorentz.CoMod.toFin1dℝAddEquiv	…/RealTensor/Vector/Pre/Modules.lean	Equiv.module and Equiv.linearEquiv now take an ≃+.
Lorentz.ContrℂModule.toFin13ℂAddEquiv, Lorentz.CoℂModule.toFin13ℂAddEquiv	…/ComplexTensor/Vector/Pre/Modules.lean	as above
toFin2ℂAddEquiv ×4: LeftHanded, RightHanded, DualLeftHanded, DualRightHanded	Physlib/Relativity/Fermions/Weyl/	as above

Each toFin…AddEquiv is the existing toFin…Fun equivalence packaged with
map_add' _ _ := rfl; the old equivalences are untouched and still carry the
AddCommGroup instances. The Standard Model fermion types
(DownSinglet, LeptonDoublet,
LeptonSinglet, QuarkDoublet, UpSinglet),
Dirac, FiniteHilbertSpace and
ReferenceFrame.Vector get the same treatment inline, since each
had exactly one use.

Signature changes to watch

Both are physlib-facing, so they are called out rather than left in the diff.

CompleteTensorProduct.induction_on loses its zero
hypothesis, following mathlib renaming TensorProduct.induction_on to
TensorProduct.inductionOn and dropping its zero case:

lemma induction_on {motive : E ⊗ₕ[𝕜] F → Prop} (z : E ⊗ₕ[𝕜] F)
    (tmul : ∀ (x : E) (y : F), motive (x ⊗ₜ[𝕜] y))
    (add : ∀ x y : E ⊗[𝕜] F, motive x → motive y → motive ↑(x + y))
    (closed : IsClosed {x | motive x}) : motive z

JBAlgebra.ClosedGeneratedByOne.spectralRadius_le_norm
drops [Nontrivial E], which its new proof through spectralRadius_le_nnnorm
does not need, and which runPhyslibAlphaLinters flags as an unused
argument.

API changes adapted to — Physlib and QuantumInfo

• MemLp f p μ is now eLpNorm f p μ < ∞ alone — eLpNorm itself carries
  the a.e.-strong-measurability guard, so the old conjunction is gone. h.1
  becomes h.aestronglyMeasurable and h.2 becomes h; the
  MemHS characterizations are rebuilt on
  memHS_iff via memLp_two_iff_integrable_sq_norm. Lemmas
  that were unconditional now take a measurability hypothesis
  (eLpNorm_one_eq_lintegral_enorm, eLpNorm_eq_lintegral_rpow_enorm_toReal,
  eLpNorm_mono_enorm, Measure.map_smul), and eLpNorm_eq_zero_iff dropped
  its measurability side condition in exchange.

• Equiv.module / Equiv.linearEquiv take an ≃+ — see § Declarations
  added. This also repairs the val_smul / norm_eq_val / basis rfl lemmas
  that rest on those instances.

• LinearPMap.ker is mathlib's submodule-valued kernel — see
  toFun_ker_eq_bot_iff above.

• IsCompact.elim_finite_subfamily_closed is stated with Disjoint rather
  than _ ∩ _ = ∅.

• Signature changes: Matrix.PosSemidef.dotProduct_mulVec_zero_iff and
  ContinuousLinearMap.nonneg_iff_isPositive made their subject implicit;
  IsSelfAdjoint.le_algebraMap_norm_self takes the element explicitly with
  self-adjointness as an auto-param;
  CStarAlgebra.norm_le_norm_of_le_of_nonneg swapped its hypotheses; the
  ordered-semiring Finset.prod_le_prod is Finset.prod_le_prod₀ and
  Finset.sum_nonneg' folded into Finset.sum_nonneg;
  Unitary.conjStarAlgAut yields a StarAlgEquiv;
  IsReindexing.topologicalGroup and friends gained is prefixes.

• Module.Basis.repr_reindex no longer beta-reduces the Finsupp
  re-indexing, so the tensor-component proofs need
  Finsupp.equivMapDomain_apply before Module.Basis.repr_reindex_apply — for
  example in Kinematics/FieldStrength.lean.

• Moves: Mathlib.Data.{Real,Complex,NNReal}.Basic → Mathlib.Basic.*;
  IsTopologicalGroup (GL n R) now needs Mathlib.Topology.Algebra.Group.Units;
  mfderiv_eq_fderiv → Mathlib.Geometry.Manifold.MFDeriv.NormedSpace.

• Renames: if_pos/if_neg/dif_pos/dif_neg/if_true →
  ite_eq_left/ite_eq_right/dite_eq_left/dite_eq_right/ite_true;
  LinearMapClass.linearMap → LinearMap.ofClass; tsum_apply →
  Pi.tsum_apply; TensorProduct.induction_on → TensorProduct.inductionOn;
  AddLeftCancelMonoid.add_eq_zero → Nat.add_eq_zero_iff;
  Submodule.coe_norm → Submodule.norm_coe, whose orientation is reversed
  (coe_norm : ‖x‖ = ‖↑x‖ but norm_coe : ‖↑x‖ = ‖x‖) — a blanket rename
  silently breaks SpectralTheory/Basic.lean.

One rename has a trap worth recording. LinearMapClass.linearMap is now a
deprecated alias for LinearMap.ofClass, and an alias is a distinct
constant, so @[simp, norm_cast] LinearMap.coe_ofClass : ⇑(ofClass f) = f does
not fire under the old spelling. Channels/Dual.lean therefore
needed its call sites actually renamed; silencing the deprecation warning would
have left the simp set silently weaker.

API changes adapted to — PhyslibAlpha

Everything above applies there too. Beyond it:

• AddMonoidAlgebra is a structure with a coeff : M →₀ R field.
  MvPolynomial.coeff is gone and the argument order is reversed: coeff m p
  becomes p.coeff m. coeff_add is AddMonoidAlgebra.coeff_add and states a
  Finsupp equality, so it needs Finsupp.add_apply beside it — see
  TwoHDM/ChargeBalance.lean and
  TwoHDM/Invariants.lean, the latter also moving
  monomial_mul to monomial_mul_monomial.

• spectralRadius is defined over quasispectrum, not spectrum.
  spectralRadius_eq_of_unital bridges the two in a unital algebra, and
  le_iSup₂ then needs its f pinned explicitly — (α := ENNReal) no longer
  determines it. See JB/GeneratedByOne/Spectrum.lean.

• TensorProduct.inductionOn drops the zero case, so each
  refine/induction … with site loses one bullet. Nine sites in
  Stinespring/Dilation.lean alone.

• Argument-order and implicitness changes:
  IsSelfAdjoint.map and
  CStarAlgebra.pow_antitone swapped their arguments;
  ContinuousLinearMap.le_def and InnerProductSpace.le_def made their
  operands implicit; Filter.Tendsto.eventually no
  longer infers its predicate from the goal.

• Measure.isProbabilityMeasure_map is now the iff
  Measure.isProbabilityMeasure_map_iff, stated in the opposite direction —
  CStarAlgebra/SpectralMeasure.lean.

• Module moves: MeasureTheory.VectorMeasure.{map, mapRange} →
  Mathlib.MeasureTheory.VectorMeasure.Operations
  (one import fixed 17 errors in a single file);
  CStarAlgebra.exists_sum_four_nonneg →
  …CStarAlgebra.SpecialFunctions.PosPart; CFC.sqrt →
  …ContinuousFunctionalCalculus.Rpow.Basic;
  CStarAlgebra.norm_le_iff_le_algebraMap →
  …ContinuousFunctionalCalculus.Order; Mathlib.Data.ENNReal.* →
  Mathlib.Basic.ENNReal.*; Mathlib.MeasureTheory.Integral.SetToL1 split into
  five modules.

• convert leaves one goal fewer at several sites where the leading case is
  now closed automatically, and eLpNorm_one_eq_lintegral_enorm's new
  measurability hypothesis must have its implicit f given eta-expanded for
  rw to match — CayleySpectralData/SpecTheorem.lean.

• Space.IsDistBounded's anonymous HasTemperateGrowth
  instance is reached by infer_instance rather than by its
  autogenerated name, which changed.

• quadRep_add_square_polarized needs
  maxHeartbeats 500000 — the smallest of 300k/400k/500k/600k/800k/1M that
  passes. The file elaborates in ~28 s.

PauliMatrix.leviCivita_mul_pauliDual needed a new proof

This is the only proof in the PR whose strategy changed, so it is in its own
commit. The statement of leviCivita_mul_pauliDual is
unchanged.

Under v4.34 the old proof fails in the kernel, verbatim:

error: Physlib/Relativity/PauliMatrices/Relations.lean:159:6: (kernel) deterministic timeout
error: Physlib/Relativity/PauliMatrices/Relations.lean:170:6: (kernel) unknown constant 'PauliMatrix.leviCivita_mul_pauliDual'

(the second is the cascade into
pauliContr_mul_pauliContrDown_mul_pauliContr). It was:

  rw [pauliDual_eq_pauliCo, prodT_permT_right, contrT_permT]
  apply permT_congr
  · decide
  · rfl

prodT_permT_right and contrT_permT
leave a proof term that makes the kernel reduce the IsReindexing transport,
which goes through IsReindexing.inv σ h = Fintype.bijInv h.1.
set_option diagnostics true on the unifier shows it grinding on
Nat.rec ↦ 187008, Fin.succSuccAbove ↦ 33186, IsReindexing.toEquiv ↦ 19833,
and reporting Fin.addCases._proof_2 ↦ 2989 under "Axioms (possibly imported
non-exposed defs) that were tried to be unfolded" — Fin.addCases being the
workhorse of Fin.append, which is how the contracted color function is built.

No set_option rescues it. Measured: maxHeartbeats 1000000 +
maxRecDepth 8000 turns the timeout into (kernel) deep recursion detected;
backward.isDefEq.respectTransparency false lets elaboration finish but the
kernel still times out; adding maxRecDepth 20000 on top ran 10 minutes to
133 GB RSS before I killed it. Raising limits is not a usable workaround even
setting CI aside.

The new proof takes the route the neighboring identities in this file already
take — push both sides to rational components first:

  conv_lhs =>
    simp only [leviCivita_eq_ofRat, toTensor_dualLorentz_eq_ofRat]
    rw [prodT_ofRat_ofRat, contrT_ofRat]
  conv_rhs =>
    simp only [leviCivita_eq_ofRat, pauliCo_eq_ofRat]
    rw [prodT_ofRat_ofRat, contrT_ofRat]
  apply (Tensor.basis _).repr.injective
  ext b
  rw [ofRat_basis_repr_apply, permT_basis_repr_symm_apply, ofRat_basis_repr_apply]
  apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr
  decide +revert +kernel

toTensor_dualLorentz_eq_ofRat and
pauliCo_eq_ofRat have the same right-hand side, so after
prodT_ofRat_ofRat and contrT_ofRat the
two sides are ofRat of the same function, separated only by the identity
reindexing ![0, 1, 2, 3, 4]. Going through
ofRat_basis_repr_apply and
permT_basis_repr_symm_apply — as
pauliContr_mul_pauliContrDown_mul_pauliContr already does —
discharges that without asking the kernel to reduce Fintype.bijInv at all. The
supporting facts are leviCivita_eq_ofRat,
pauliDual_eq_pauliCo and
RatComplexNum.toComplexNum_injective.

It needs no set_option, and elaborates and kernel-checks in about 85 s.

Two things I could not make work, in case one of them is the proof you would
prefer: congr on the residual
ofRat f = permT ![0,1,2,3,4] _ (ofRat f) times out at whnf even at 10⁶
heartbeats, and permT_congr_eq_id cannot be applied
there because unifying the two color functions — they differ by
Function.update ![up, upL, upR] 0 (τ up) versus ![down, upL, upR] — is
itself the divergent reduction.

lake exe TODO_to_yml mkFile is blocked, and not by this PR

uncaught exception: import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.Basic failed,
environment already contains 'QuantumMechanics.HarmonicOscillator.potentialFunction'
from Physlib.QuantumMechanics.HarmonicOscillator.Basic

TODO_to_yml imports both libraries into one environment — it
has a PhyslibAlpha category — and they both declare
QuantumMechanics.HarmonicOscillator.potentialFunction:
Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean:186
and
PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean:175.
Both declarations are present on master at those same lines and neither file
is touched by this branch. Resolving it means renaming one of the two, which is
a content decision, so I have left it. Happy to file it separately if that is
useful.

The lint_all transitive-import section

lake exe lint_all exits 0 and every section CI gates on passes. Its last
section, (7/7) Transitive imports, reports 74 files. That
section is not gated — CI runs check_file_imports,
check_dup_tags, sorry_lint and runPhyslibLinters, not lint_all — and I
left all 74 alone, because acting on it is not safe as stated. Removing
the two imports it flags in
Physlib/SpaceAndTime/Time/Derivatives.lean
(Mathlib.Analysis.Calculus.Deriv.Inv and
Mathlib.Analysis.InnerProductSpace.Calculus) breaks that file:

Physlib/SpaceAndTime/Time/Derivatives.lean:366:6: error(lean.unknownIdentifier): Unknown identifier `differentiable_euclidean`

at this site, plus an unsolved deriv Inv.inv goal
in deriv_div. Under the module system the linter's
reachability notion and public import re-export do not agree, so its output is
advisory. Worth a separate issue rather than anything in a bump.

The 20 remaining warnings, and why each is left

• 6 × List.tfae_cons_self (Physlib) — tfae_cons_of_mem carries a
  membership side condition; a naive rename makes simp report "simp made no
  progress" in equationOfMotion_tfae
  (ClassicalMechanics/HarmonicOscillator/Basic.lean:750,752,754) and
  SimplePendulum.equationOfMotion_tfae
  (SimplePendulum/Hamiltonian.lean:312,315,319).
• 3 × the peel syntax — Matrix.lean:720,
  LimSupInf.lean:177, Filter.lean:49;
  gconvert/congr! restructure the proof.
• 7 × stdSimplex (PhyslibAlpha) — Convexity.StdSimplex is a
  structure, not a set, so this changes PhyslibAlpha's own API and its users,
  not just a name. Five in OrderUnit/State/Convex.lean
  (lines 50, 56, 61, 66, 73) and two in
  Measurement/Basic.lean (lines 70, 82).
• 4 × automatically included section variable(s) unused (PhyslibAlpha) —
  stoneCandidateDomainPred_add,
  rankOne_self_diagonal,
  hilbertSchmidtPartial_apply and
  mul_rankOne_apply_left. Each already carries
  @[nolint unusedArguments], and stoneCandidateDomainPred_add's docstring
  states the parameter is retained deliberately so the lemma matches
  stoneCandidateDomain.

None of these belong in a bump; all four groups are easy follow-ups.

Notes on this PR

Produced with AI assistance (Claude Opus 5); the commits carry a
Co-authored-by trailer. Per AI-POLICY.md §1.7 and
§2.2 I have reviewed the diff and vouch for it.

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[nateabr]

Thank you for working on this bump, a suggestion below on how we could fix lake exe TODO_to_yml

Within scripts/MetaPrograms/TODO_to_yml.lean there is a line in the last section:

let env ← importModules (loadExts := true) #[Physlib, QuantumInfo, PhyslibAlpha] {} 0`

This loads Physlib, QuantumInfo, and PhyslibAlpha into one Lean environment. Since Physlib and Alpha both expose QuantumMechanics.HarmonicOscillator.potentialFunction, Lean rejects the second declaration (you had already called this out in your zulip message).

The diff of this PR does not change the script itself so I am not able to suggest code but could we try implementing the follwing schematic in the file I mentioned.

environment A: Physlib + QuantumInfo → collect TODO records
environment B: PhyslibAlpha → collect TODO records
merge the two record lists → global tag check → one YAML file

let me know if this makes sense

[zhikaip]

just a heads-up: I happen to be doing some performance improvements, and my improvements apply to your proposed change in PauliMatrix.leviCivita_mul_pauliDual as well. If #1664 gets merged first you might need to rebase on that, apologies for the inconvenience

[jstoobysmith]

@nateabr what is your opinion on this? Should we fix the Todo thing now? Or merge this first? If the latter would you mind doing a full review?

[nateabr]

@jstoobysmith I actually have gone through this in detail before and I believe this looks good and is ready to merge. I am happy to do the todo fix as a follow up

[jstoobysmith]

Ive approved this

[jstoobysmith]

@zhikaip Is it okay if we merge this one first?

[zhikaip]

Sure I will rebase my branch. Merging now