feat: Reorganise the Mathematics directory

[jstoobysmith]

Made with the help of Opus 5.5.

Split ./Mathematics into ./Mathematics and ./Mathematics/ForMathlib. The latter is for results for Mathlib, whilst everything else in ./Mathematics is mathematics for physics.

AI summary

refactor(Mathematics): split out ForMathlib/, add forMathlib_lint

Physlib/Mathematics/ currently mixes two kinds of file:

• material that is the physicist's way of doing things and will stay in Physlib;
• results that are only here until they reach Mathlib.

This PR moves the second kind into Physlib/Mathematics/ForMathlib/ and adds a linter that keeps that directory upstreamable.

1. Reorganisation

These are file moves only: no declaration is renamed. Only import paths and module references in docstrings change.

• → ForMathlib/:
  • Trigonometry/, OneParameterSubgroups/, DataStructures/Matrix/LieTrace
  • Fin.lean and Fin/, List.lean and List/
  • LinearMaps, LinearPMap, OrthogonalMatrix, SchurTriangulation, FDerivCurry, HasTemperateGrowth
• → Modules/: ConjModule, CrossProduct, CrossProductMatrix
• → Groups/SO3/: SO3/Basic

2. New linter: lake exe forMathlib_lint

The linter is in scripts/forMathlib_lint.lean. It only parses import headers, so it does not need a build. It checks two rules:

1. A file in ForMathlib/ may import only from ForMathlib/, Mathlib, Batteries and Lean. It may not import anything else from Physlib, PhyslibAlpha or QuantumInfo.
2. Every file in ForMathlib/ must be imported, directly or through other ForMathlib/ files, by some file outside ForMathlib/. The library root files don't count as uses.

It is wired into lakefile.toml, lint_all, CI (build.yml) and the AGENTS.md checklist.

Definitions added (all in scripts/forMathlib_lint.lean): forMathlibPrefix, libraryDirs, isForMathlib, isLibraryModule, moduleNameOfPath, libraryImports, outsideImports, unusedModules, sortNames, main.

3. Changes needed to pass the linter

• ForMathlib/LinearMaps: its TODO note moved to the TODO section of QFT/AnomalyCancellation/Basic, its only user. This removes the Physlib.Meta.TODO.Basic import from LinearMaps.
• Six files deleted: nothing in Physlib, PhyslibAlpha or QuantumInfo imported them. Every declaration in them is removed:
  • DataStructures/FourTree/Basic: Leaf, Twig, Branch, Trunk, FourTree, fromMultiset, toMultiset, {Twig,Branch,Trunk}.card, card, card_eq_toMultiset_card, {Leaf,Twig,Branch,Trunk}.mem, mem, mem_iff_mem_toMultiset, mem_of_parts
  • DataStructures/FourTree/UniqueMap: {Leaf,Twig,Branch,Trunk}.uniqueMap4, uniqueMap4, {Twig,Branch,Trunk}.uniqueMap3, uniqueMap3, map_mem_uniqueMap{3,4}, exists_of_mem_uniqueMap{3,4}
  • Geometry/Metric/PseudoRiemannian/Defs:
    • PseudoRiemannianMetric, negDim, pseudoRiemannianMetricValToQuadraticForm, toBilinForm, toQuadraticForm, inner
    • flat, flatL, flatEquiv, sharp, sharpL, sharpEquiv
    • cotangentMetricVal, cotangentToBilinForm, cotangentToQuadraticForm
    • their API lemmas: *_apply, *_isSymm, *_nondegenerate, flat_inj, flatL_surj, flat_sharp_apply, sharp_flat_apply, apply_sharp_sharp, apply_vec_sharp, rankNeg_eq_zero, posDef_no_neg_weights, neg_weight_implies_neg_value, QuadraticMap.weightedSumSquares_basis_vector
  • Geometry/Metric/Riemannian/Defs: RiemannianMetric, tangentInnerCore, TangentSpace.metricNormedAddCommGroup, TangentSpace.metricInnerProductSpace('), norm, norm', curveLength, pos_def, toQuadraticForm_posDef, riemannian_metric_negDim_zero, norm_eq_norm_of_metricNormedAddCommGroup. Mathlib now provides Bundle.RiemannianMetric.
  • PiTensorProduct: induction_tmul, induction_assoc('), induction_tmul_mod, induction_mod_tmul, pureInl, pureInr and their update lemmas, domCoprod, tmulSymm, elimPureTensor (and its update lemmas), elimPureTensorMulLin, tmul, tmulEquiv, tmulEquiv_tmul_tprod
  • Resolvent: mem_resolventSet_of_im_ne_zero, resolventSet_eq_univ, norm_resolvent_le, contDiff_resolvent, iteratedDeriv_resolvent, norm_iteratedDeriv_resolvent_le, hasTemperateGrowth_resolvent
• Meta/Linters/DefsWithUnderscore: a comment no longer refers to the deleted FourTree file. The exemption it describes is unchanged.

Reviewer map

1. scripts/forMathlib_lint.lean, then the one-line wirings in lakefile.toml, scripts/lint_all.lean, .github/workflows/build.yml and AGENTS.md.
2. The six deletions and the LinearMaps → AnomalyCancellation/Basic TODO move.
3. The moves: skim. Git shows them as renames, with only import paths changed.

🤖 Generated with Claude Code

[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]

claim

[github-actions]

Review claim by @nateabr completed — thanks for the review.

[nateabr]

Looks good to me - approved :)

[nateabr]

A point for clarification before this merges, have you also imposed that all files in physlib/mathematics/ must be used outside mathematics?

[jstoobysmith]

No, files in ./Physlib/Mathematics need not be used outside that directory, only those in ./Physlib/Mathematics/ForMathlib. The idea here is to stop people adding things which are really for mathlib to Physlib.