chore(tests): build the test library from a Lake glob, removing ComplexityTests.lean

.gitattributes

@@ -1,7 +1,7 @@
-# Generated root import aggregators are sorted lists of one-line imports.
+# Generated root import aggregators are sorted lists of one-line imports. (The test library has
+# no aggregator: Lake builds it from a glob, see `lakefile.toml`.)
 # Union merge avoids spurious 3-line context conflicts when concurrent PRs add
 # imports in the same alphabetical neighborhood; `lake exe mk_all --check` in
 # merge-queue CI still enforces canonical sort order.
 Complexity.lean merge=union
-ComplexityTests.lean merge=union
 abstracts/ComplexityAbstracts.lean merge=union

AGENTS.md

@@ -253,7 +253,7 @@ ambiguous change/import analysis fall back to all six gates. Run the default com
 submitting a PR; quick success does not satisfy that requirement.
 
 `lake exe mk_all` regenerates `Complexity.lean` after adding a file. New test files go in
-`ComplexityTests/` and must be imported from `ComplexityTests.lean`.
+`ComplexityTests/`; the test library is built from a Lake glob, so there is no aggregator to update.
 
 ## File rules
 
@@ -393,10 +393,10 @@ and [API review with explicit nonblocking nits](https://github.com/leanprover/cs
 
 `abstracts/catalogue.json` selects the public headline results. Each selected group has a checked
 `*Abstract.lean` and `*Bridge.lean` under `abstracts/ComplexityAbstracts/`, imported by the
-dedicated `ComplexityAbstracts` library. `ComplexityTests.lean` imports that library and its
-regression tests. Existing declaration namespaces remain stable across the source relocation.
-The Lean definitions and statements are the source of truth; PDFs are generated from them, with
-proof bodies omitted. There is no separately maintained paper/TeX index.
+dedicated `ComplexityAbstracts` library. `ComplexityTests/Abstracts/All.lean` imports that library,
+and its regression tests sit beside it. Existing declaration namespaces remain stable across the
+source relocation. The Lean definitions and statements are the source of truth; PDFs are generated
+from them, with proof bodies omitted. There is no separately maintained paper/TeX index.
 
 Selection has a higher bar than inclusion in the library: a headline must be a substantial proved
 endpoint with conventional, inspectable semantics, hypotheses that are satisfiable or are standard

CONTRIBUTING.md

@@ -179,10 +179,10 @@ Keep incomplete endpoints in `ROADMAP.md` and credit mathematical and formalizat
 
 Every AI-authored PR must assess its final Lean changes against the selection. Update affected
 abstracts and scope notes, or explain why the catalogue is unaffected. Proof-only changes with
-unchanged statements and scope can record that assessment without rewriting the abstract. Follow
-the repository's `lean-abstract` skill, import new abstracts in `ComplexityTests.lean`, and run their
-`#check_abstract` audits. Allow only narrow, explained foundational models; do not allowlist the
-result's class definitions or construction to evade a self-contained statement.
+unchanged statements and scope can record that assessment without rewriting the abstract. Follow the
+repository's `lean-abstract` skill, import new abstracts in `ComplexityTests/Abstracts/All.lean`,
+and run their `#check_abstract` audits. Allow only narrow, explained foundational models; do not
+allowlist the result's class definitions or construction to evade a self-contained statement.
 
 Arrange independent API, correctness and abstract reviews against the final source revision.
 Reviewers must check quantifiers, semantics, encodings, bounds, nonvacuity and readability. Record