chore: create a Basic top folder

[YaelDillies]

Move a select few folders from Logic to a new Basic folder.

The goal is to finally move the material misplaced in the Data and Logic folder and to clarify the various expectations of each folder. Ultimately:

• the Basic folder will be about basic predicates on types and basic mathematical types not fitting in any other folder;
• the Data folder will be about data structures, instead of the current mix of data structures and basic mathematical types not fitting in any other folder;
• the Logic folder will be about advanced logic results not fitting in either ModelTheory or SetTheory, instead of the current mix of basic predicates on types and advanced logic results.

Many more files (~1000) could be moved, so I will do it in several PRs. Not all files should move to Basic. Some files should go to Algebra.Order instead (eg Data.Nat.Lattice) and some should be straight out deprecated (eg Data.Analysis).

Zulip discussion

---

This PR stems from discussions at the MI retreat 2026.

[github-actions]

PR summary da2e271136

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.CongrExclamation	67	58	-9 (-13.43%)

Import changes for all files

Files	Import difference
Mathlib.Logic.Denumerable	-483
Mathlib.Logic.UnivLE	-121
Mathlib.Logic.Nontrivial.Basic	-106
Mathlib.Logic.IsEmpty.Basic Mathlib.Logic.Unique	-92
Mathlib.Logic.IsEmpty	-91
Mathlib.Logic.Lemmas	-75
Mathlib.Logic.Basic	-63
Mathlib.Logic.Nontrivial.Defs	-57
3 files Mathlib.Logic.ExistsUnique Mathlib.Logic.IsEmpty.Defs Mathlib.Logic.Nonempty	-55
Mathlib.Tactic.CongrExclamation Mathlib.Tactic.Convert	-9
3 files Mathlib.Basic.ExistsUnique Mathlib.Basic.IsEmpty.Defs Mathlib.Basic.Nonempty	55
Mathlib.Basic.Nontrivial.Defs	57
Mathlib.Basic.Logic.Basic	63
Mathlib.Basic.Logic.Lemmas	75
Mathlib.Basic.IsEmpty	91
Mathlib.Basic.IsEmpty.Basic Mathlib.Basic.Unique	92
Mathlib.Basic.Nontrivial.Basic	106
Mathlib.Basic.UnivLE	121
Mathlib.Basic.Denumerable	483

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit da2e271).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit da2e271136
Reference commit fd1d54bcac

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

note: file Mathlib/Logic/Nonempty.lean` was renamed to `Mathlib/Basic/Nonempty.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/Unique.lean` was renamed to `Mathlib/Basic/Unique.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/IsEmpty/Basic.lean` was renamed to `Mathlib/Basic/IsEmpty/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/Nontrivial/Defs.lean` was renamed to `Mathlib/Basic/Nontrivial/Defs.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/Basic.lean` was renamed to `Mathlib/Basic/Logic/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/Denumerable.lean` was renamed to `Mathlib/Basic/Denumerable.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/IsEmpty.lean` was renamed to `Mathlib/Basic/IsEmpty.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/IsEmpty/Defs.lean` was renamed to `Mathlib/Basic/IsEmpty/Defs.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/UnivLE.lean` was renamed to `Mathlib/Basic/UnivLE.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/ExistsUnique.lean` was renamed to `Mathlib/Basic/ExistsUnique.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/Nontrivial/Basic.lean` was renamed to `Mathlib/Basic/Nontrivial/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Logic/Lemmas.lean` was renamed to `Mathlib/Basic/Logic/Lemmas.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

[grunweg]

I have heard Bhavik and Julia articulate a good case for this split, and how the eventual vision could look like. This would make an excellent addition to this PR description and the zulip thread. Let's wait on that being added before discussing.

[joneugster]

I think this is very reasonable, thank you for the change!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[YaelDillies]

I have heard Bhavik and Julia articulate a good case for this split, and how the eventual vision could look like. This would make an excellent addition to this PR description and the zulip thread. Let's wait on that being added before discussing.

I do not remember what they said that I haven't already incorporated in the PR description.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[grunweg]

You will find #39990 interesting: today's your lucky day as I felt like mucking up the Data stables.

[grunweg]

Does this proposal imply that Basic will in particular not import any interesting directories (such as Analysis, Algebra, Dynamics, Topology, SetTheory, etc.)? That what feels natural to me --- if you agree, can you document it (and make the DirectoryDependency linter enforce it)?

[grunweg]

Should this be discussed on zulip? (Or has it: if so, can you link to the discussion, please?)

[YaelDillies]

No, we'll need to import Algebra and Order (so please don't move more material from Data to Algebra or Order, at least for now). All others should be forbiddable.

This has been discussed in the reviewers stream on Zulip. Do you want a wider discussion than that?

[grunweg]

No, we'll need to import Algebra and Order (so please don't move more material from Data to Algebra or Order, at least for now). All others should be forbiddable.

If a file naturally belongs to Algebra, why should it not move there?
I hear your point that it might also belong to Basic, in which case that PR should not be merged. That's fine with me. (I'm certainly happy to CC you on all my Data cleaning PRs; my aim was to start on the end of "this should certainly not go into Basic".)

This has been discussed in the reviewers stream on Zulip. Do you want a wider discussion than that?

I think reviewers are a sufficient target group (though at some point, something public would be good --- other contributors should learn this exists!). Linking that discussion would be nice, though :-)

[grunweg]

Reading your previous message raises the question: how do I decide if a file belongs to Algebra, Order, (Algebra.Order) or Basic then? Let's make this clear :-)

edit: asked back on Zulip --- perhaps that is a good location for any discussions

[joneugster]

@reviewer: Here is the vision for the new folder. If unclear or incomplete, this README should be extended

[joneugster]

(there are also READMEs for Logic and Basic)

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[j-loreaux]

I just asked on Zulip, but I would like more documentation in the READMEs. As-is, I still don't have a firm grasp on the distinctions and the reasoning behind them. I would prefer not to merge this until we have clear(-ish) distinctions documented.

[YaelDillies]

Let me know what you think now.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[TwoFX]

I don't think I agree with this sentence. I think that there is a small set of data structures which are only relevant for mathlib and hence not suitable for inclusion in core or batteries. I think the differentiation should be more about the material appearing in this folder being supporting material for making mathlib possible, but not really mathematics itself.

[YaelDillies]

My opinion would be for this material to be in Basic instead, otherwise we might end up with Data.List for the basic List material that's "not mathematics" and Basic.List for the one that is (leading to bikesheddy discussions on what is mathematics and what is not, etc...). Would you be happy with that?

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.