diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md
index 63e1f4a168..c03277e3e4 100644
--- a/.github/CODE_QUALITY.md
+++ b/.github/CODE_QUALITY.md
@@ -34,7 +34,7 @@ The generated module-system indexes import every library file, so building them
 
 Current checks:
 
-- every `.lean` file under `LeanPool/`, plus `LeanPool.lean`, is reachable from `LeanPool.lean`
+- Lake discovers every `.lean` file under `LeanPool/`; every project source is also reachable from its public `Imports.lean`
 - every content `.lean` file except `LeanPool.lean` has the exact four-line file header
 - content files do not contain `set_option`, `nolint` waivers, broad `import Mathlib`, `sorry`, `admit`, unchecked declarations (`axiom`, `constant`, `unsafe`, `partial`, `opaque`, `@[extern]`), or diagnostic commands (`#check`, `#print`, `#eval`, `#reduce`, `#guard_msgs`, `#lint`)
 - content files do not manipulate elaborator options programmatically: option-API tokens (`withOptions`, `modifyOptions`, `withRecDepth`, `withCurrHeartbeats`, `KVMap`/`Options`/`Option` setters, ...) and gated option names (`maxRecDepth`, `maxHeartbeats`, `maxSynthPendingDepth`, `linter.*`) are forbidden in code (comments are fine) — ``withOptions (fun o => o.set `maxRecDepth 100000)`` inside an elaborator is still `set_option maxRecDepth 100000`
@@ -42,7 +42,7 @@ Current checks:
 - the style-linter allowlist `scripts/nolints-style.txt` has no active entries
 - no Lean content file exceeds 10000 non-blank, non-comment code lines
 - no theorem/lemma proof body exceeds 200 non-blank, non-comment code lines, using the current text heuristic
-- `LeanPool/projects.yml` exists, is valid YAML, and contains a `projects` list
+- `LeanPool/projects/` contains one valid YAML mapping per project, with its filename matching the unique slug; duplicate fields, nested cards, and mixed old/new registries fail validation
 - project entries have required fields: `slug`, `title`, `entry_module`, `authors`, `source`, `status`, `provenance`, `main_declarations`, and `tags`
 - project entries also carry documentation metadata: `summary`, `branch`, `main_results`, and `msc`
 - project `status` is `verified`
@@ -52,16 +52,16 @@ Current checks:
 - project summaries and branches are nonempty strings, MSC codes are a nonempty string list, and `main_results` is a nonempty list of `declaration` / `informal` entries
 - project `main_results[*].declaration` values include every `main_declarations` entry, so compact project cards and richer documentation metadata cannot drift
 - project `slug` and `entry_module` values are unique
-- every registered project `entry_module` is imported directly by `LeanPool.lean`
+- every registered project `entry_module` is imported by its project’s public `Imports.lean`
 - every project has a top-level entry file `LeanPool/<Project>.lean`, including projects with nested registered entry modules
 - every nested registered entry module is reachable through its top-level entry file's imports
 - every top-level project module `LeanPool/Foo.lean`, except `LeanPool/Basic.lean`, belongs to the namespace of a registered `entry_module`
 - project entry modules and listed main declarations resolve in Lean
-- generated entry-point project cards match `LeanPool/projects.yml`
+- generated entry-point project cards match `LeanPool/projects/*.yaml`
 - public declarations depend only on the allowed axiom set: `Classical.choice`, `propext`, and `Quot.sound`
 - a Lean environment audit (run via `lake env lean --run` with extensions disabled, so project notation cannot interfere) walks **every** declaration compiled into a pool module — including elaborator auxiliaries and generated declarations the textual scans cannot see — and rejects any that references option-manipulating constants, embeds a gated option-name literal (however the `Name` was assembled), directly references an axiom-injecting constant (`sorryAx`, `ofReduceBool`, ...), or is itself an axiom declared inside a pool module (which is how `native_decide` and `addDecl`-of-an-axiom backdoors surface)
 
-The checker also has `--write-project-cards` to regenerate entry-point module docstrings from `LeanPool/projects.yml`.
+The checker also has `--write-project-cards` to regenerate entry-point module docstrings from `LeanPool/projects/*.yaml`.
 
 ### 3. PR Separation
 
@@ -69,13 +69,12 @@ The checker also has `--write-project-cards` to regenerate entry-point module do
 
 Content files are:
 
-- `LeanPool.lean`
 - `LeanPool/**/*.lean`
-- `LeanPool/projects.yml`
+- `LeanPool/projects/*.yaml`
 
 A PR may touch only content files or only non-content files. Mixing these categories fails CI, except that a Lean/Mathlib version bump may pair content with the toolchain, manifest, lakefile, their `docbuild/` equivalents, and this workflow.
 
-Branch protection to require these checks before merge is future work.
+Branch protection requires the build, separation and documentation gates; the merge queue validates their combined result on current main.
 
 ### 4. Python CI
 
@@ -148,7 +147,7 @@ The following items are documented goals but are not fully implemented or enforc
 - branch protection requiring the CI gates before merge
 - scheduled Lean/Mathlib update checks
 - LeanExplore semantic dedup comments in PRs; the prototype CLI is [`python/lean_pool/semantic_dedup.py`](../python/lean_pool/semantic_dedup.py)
-- controlled tag vocabulary for `LeanPool/projects.yml`; tags are currently only checked as nonempty strings
+- controlled tag vocabulary for `LeanPool/projects/*.yaml`; tags are currently only checked as nonempty strings
 - generated domain/status indexes
 - directory index-file policy: every directory under `LeanPool/` containing Lean files should have an import-only index file with a module docstring
 - AST-aware proof-size measurement; the current 200-line proof cap uses a text heuristic
diff --git a/.github/merge-queue-ruleset.json b/.github/merge-queue-ruleset.json
new file mode 100644
index 0000000000..3d1999ce47
--- /dev/null
+++ b/.github/merge-queue-ruleset.json
@@ -0,0 +1,84 @@
+{
+  "name": "Validated merge queue",
+  "target": "branch",
+  "enforcement": "disabled",
+  "bypass_actors": [],
+  "conditions": {
+    "ref_name": {
+      "include": [
+        "refs/heads/main"
+      ],
+      "exclude": []
+    }
+  },
+  "rules": [
+    {
+      "type": "deletion"
+    },
+    {
+      "type": "non_fast_forward"
+    },
+    {
+      "type": "pull_request",
+      "parameters": {
+        "dismiss_stale_reviews_on_push": false,
+        "require_code_owner_review": false,
+        "require_last_push_approval": false,
+        "required_approving_review_count": 0,
+        "required_review_thread_resolution": true
+      }
+    },
+    {
+      "type": "required_status_checks",
+      "parameters": {
+        "strict_required_status_checks_policy": false,
+        "required_status_checks": [
+          {
+            "context": "Build project",
+            "integration_id": 15368
+          },
+          {
+            "context": "Content / non-content separation",
+            "integration_id": 15368
+          },
+          {
+            "context": "Documentation preflight",
+            "integration_id": 15368
+          },
+          {
+            "context": "Lint (ruff)",
+            "integration_id": 15368
+          },
+          {
+            "context": "Test (pytest)",
+            "integration_id": 15368
+          },
+          {
+            "context": "actionlint",
+            "integration_id": 15368
+          },
+          {
+            "context": "SHA-pinned Actions",
+            "integration_id": 15368
+          },
+          {
+            "context": "Verify minimal Lean files",
+            "integration_id": 15368
+          }
+        ]
+      }
+    },
+    {
+      "type": "merge_queue",
+      "parameters": {
+        "check_response_timeout_minutes": 240,
+        "grouping_strategy": "ALLGREEN",
+        "max_entries_to_build": 3,
+        "max_entries_to_merge": 10,
+        "merge_method": "SQUASH",
+        "min_entries_to_merge": 1,
+        "min_entries_to_merge_wait_minutes": 0
+      }
+    }
+  ]
+}
diff --git a/.github/workflows/auto-rebase.yml b/.github/workflows/auto-rebase.yml
index fe81893a8f..c1fab26091 100644
--- a/.github/workflows/auto-rebase.yml
+++ b/.github/workflows/auto-rebase.yml
@@ -46,6 +46,7 @@ permissions:
 
 jobs:
   list:
+    if: vars.USE_MERGE_QUEUE != 'true'
     runs-on: ubuntu-latest
     name: List open PRs
     outputs:
diff --git a/.github/workflows/content-pr-guard.yml b/.github/workflows/content-pr-guard.yml
index ef0200a79f..19fad3876c 100644
--- a/.github/workflows/content-pr-guard.yml
+++ b/.github/workflows/content-pr-guard.yml
@@ -4,6 +4,8 @@ name: PR Separation Guard
 # Lean/Mathlib version bumps may also include their Lake/toolchain metadata.
 
 on:
+  merge_group:
+    types: [checks_requested]
   pull_request:
     types: [opened, synchronize, reopened]
   workflow_dispatch:
@@ -22,7 +24,7 @@ concurrency:
   # the input PR number; otherwise group by the live PR number as before.
   group: >-
     content-pr-guard-${{ github.event.pull_request.number ||
-      inputs.pr_number }}
+      inputs.pr_number || github.ref }}
   cancel-in-progress: true
 
 jobs:
@@ -30,7 +32,22 @@ jobs:
     runs-on: ubuntu-latest
     name: Content / non-content separation
     steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+
+      - name: Check every PR in the combined queue commit
+        if: github.event_name == 'merge_group'
+        env:
+          BASE_SHA: ${{ github.event.merge_group.base_sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.queue_guard
+          --base "$BASE_SHA" --head "$HEAD_SHA"
+
       - name: Reject mixed content and non-content changes
+        if: github.event_name != 'merge_group'
         env:
           GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           REPO: ${{ github.repository }}
@@ -42,7 +59,13 @@ jobs:
           printf '%s\n' "$files" | sed 's/^/  /'
           echo
 
-          content_re='^(LeanPool\.lean|LeanPool/.+\.lean|LeanPool/projects\.yml)$'
+          base=$(gh api "repos/$REPO/pulls/$PR_NUMBER" --jq '.base.sha')
+          content_re='^(LeanPool\.lean|LeanPool/.+\.lean|LeanPool/projects\.yml|LeanPool/projects/[A-Za-z0-9_-]+\.yaml)$'
+          if ! git cat-file -e "$base:LeanPool/projects.yml" 2>/dev/null \
+            && printf '%s\n' "$files" | grep -qx 'LeanPool.lean'; then
+            echo '::error::LeanPool.lean is fixed; PRs must not edit the shared root.'
+            exit 1
+          fi
           content="$(printf '%s\n' "$files" | { grep -E "$content_re" || true; })"
           non_content="$(printf '%s\n' "$files" | { grep -vE "$content_re" || true; })"
 
@@ -63,9 +86,8 @@ jobs:
 
             echo "::error::This PR mixes content and non-content changes."
             echo "Content files may be changed only in content-only PRs:"
-            echo "  - LeanPool.lean"
             echo "  - LeanPool/**/*.lean"
-            echo "  - LeanPool/projects.yml"
+            echo "  - LeanPool/projects/*.yaml"
             echo "(Exception: a version bump may also touch lean-toolchain,"
             echo " lake-manifest.json, and lakefile.toml.)"
             echo
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index f61289433f..1ab56b13c3 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -1,11 +1,14 @@
 name: Documentation
 
 on:
+  merge_group:
+    types: [checks_requested]
   push:
     branches:
       - main
     paths:
       - '**/*.lean'
+      - 'LeanPool/projects/**'
       - 'LeanPool/projects.yml'
       - 'lakefile.toml'
       - 'lake-manifest.json'
@@ -22,28 +25,6 @@ on:
   pull_request:
     branches:
       - main
-    paths:
-      - 'README.md'
-      # Attribution-only and CI-only PRs must still produce the required
-      # `Documentation preflight` check.
-      - 'NOTICE.extra.yml'
-      - '.github/workflows/lean_action_ci.yml'
-      - 'scripts/ci/**'
-      - '**/*.lean'
-      - 'LeanPool/projects.yml'
-      - 'lakefile.toml'
-      - 'lake-manifest.json'
-      - 'lean-toolchain'
-      - 'docbuild/**'
-      - 'python/lean_pool/exposition/**'
-      - 'python/lean_pool/quality.py'
-      - 'python/lean_pool/validation_cache.py'
-      - 'python/lean_pool/ci_artifacts.py'
-      - 'python/lean_pool/ci_cache.py'
-      - 'python/lean_pool/rebase_fastpath.py'
-      - 'scripts/exposition/**'
-      - '.github/workflows/notice.yml'
-      - '.github/workflows/docs.yml'
   workflow_dispatch:
     inputs:
       preview:
@@ -81,6 +62,11 @@ jobs:
         with:
           fetch-depth: 0
 
+      - name: Install Python tooling runtime
+        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+        with:
+          enable-cache: true
+
       - name: Identify compiled Lean sources
         id: build-identity
         run: |
@@ -91,9 +77,9 @@ jobs:
       - name: Detect README-only change
         id: scope
         env:
-          BASE_SHA: ${{ github.event.pull_request.base.sha }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
           EVENT_NAME: ${{ github.event_name }}
-          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
         run: |
           set -euo pipefail
           readme_only=false
@@ -113,10 +99,10 @@ jobs:
           GH_TOKEN: ${{ github.token }}
           REPOSITORY: ${{ github.repository }}
           PR_NUMBER: ${{ github.event.pull_request.number }}
-          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
-          BASE_SHA: ${{ github.event.pull_request.base.sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
         run: |
-          decision=$(PYTHONPATH=python python3 -m lean_pool.rebase_fastpath decide \
+          decision=$(PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath decide \
             --workflow docs.yml --repository "$REPOSITORY" --number "$PR_NUMBER" \
             --head "$HEAD_SHA" --base "$BASE_SHA")
           echo "rebase_only=$(echo "$decision" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" >> "$GITHUB_OUTPUT"
@@ -188,7 +174,7 @@ jobs:
 
       - name: Check regenerated LeanPool root without Lean
         if: steps.rebase.outputs.rebase_only == 'true'
-        run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath check-index
+        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index
 
   # Runs in parallel with the doc-gen4 build; its (small) artifact is merged
   # into the Pages tree by the `deploy` job. Restores the root build cache but
diff --git a/.github/workflows/exposition-verify.yml b/.github/workflows/exposition-verify.yml
index 420356b851..6e641f7e02 100644
--- a/.github/workflows/exposition-verify.yml
+++ b/.github/workflows/exposition-verify.yml
@@ -7,17 +7,14 @@ name: Exposition Verify
 # fast; this is the correctness gate for the builder itself).
 
 on:
+  merge_group:
+    types: [checks_requested]
   schedule:
     - cron: '40 6 * * 1'
   workflow_dispatch:
   pull_request:
     branches:
       - main
-    paths:
-      - 'python/lean_pool/exposition/**'
-      - 'python/lean_pool/ci_artifacts.py'
-      - 'scripts/exposition/**'
-      - '.github/workflows/exposition-verify.yml'
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
@@ -28,10 +25,75 @@ permissions:
   actions: read
 
 jobs:
+  scope:
+    runs-on: ubuntu-latest
+    outputs:
+      applicable: ${{ steps.scope.outputs.applicable }}
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - id: scope
+        env:
+          EVENT: ${{ github.event_name }}
+          BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
+        run: |
+          applicable=true
+          if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then
+            applicable=false
+            if [ "$EVENT" = pull_request ]; then
+              files=$(git diff --name-only "$BASE"...HEAD)
+            else
+              files=$(git diff --name-only "$BASE"..HEAD)
+            fi
+            if printf '%s\n' "$files" | grep -Eq '^(python/lean_pool/(exposition/|ci_artifacts.py$)|scripts/exposition/|.github/workflows/exposition-verify.yml$)'; then
+              applicable=true
+            fi
+          fi
+          echo "applicable=$applicable" >> "$GITHUB_OUTPUT"
+  # Waiting for another workflow must not consume the six-hour runner window
+  # needed by extraction and real minimal-file verification.
+  build-ready:
+    needs: scope
+    if: needs.scope.outputs.applicable == 'true' && github.event_name == 'pull_request'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          persist-credentials: false
+      - name: Wait for matching Lean CI build
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
+          BUILD_EVENT: ${{ github.event_name }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_artifacts wait
+          --head "$BUILD_HEAD" --event "$BUILD_EVENT" --wait-seconds 18000
   verify:
+    needs: [scope, build-ready]
+    if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false')
     runs-on: ubuntu-latest
     name: Verify minimal Lean files
     steps:
+      - name: Require successful change classification
+        env:
+          SCOPE_RESULT: ${{ needs.scope.result }}
+          APPLICABLE: ${{ needs.scope.outputs.applicable }}
+          BUILD_READY_RESULT: ${{ needs.build-ready.result }}
+          EVENT: ${{ github.event_name }}
+        run: |
+          if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then
+            echo "::error::Change classification failed; required validation cannot be skipped."
+            exit 1
+          fi
+          case "$EVENT:$BUILD_READY_RESULT" in
+            pull_request:success|merge_group:skipped|schedule:skipped|workflow_dispatch:skipped) ;;
+            *)
+              echo "::error::Build preparation failed; required validation cannot be skipped."
+              exit 1
+              ;;
+          esac
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
 
@@ -79,7 +141,7 @@ jobs:
           fi
 
       - name: Reuse matching Lean CI build
-        if: steps.pool-build.outputs.cache-hit != 'true' && github.event_name != 'pull_request'
+        if: steps.pool-build.outputs.cache-hit != 'true' && github.event_name != 'merge_group'
         env:
           GH_TOKEN: ${{ github.token }}
           BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
@@ -87,6 +149,23 @@ jobs:
         run: >-
           PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore
           --head "$BUILD_HEAD" --event "$BUILD_EVENT"
+          --pull-request-artifact --wait-seconds 0
+
+      - name: Install uv
+        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+        with:
+          enable-cache: true
+
+      - name: Reuse successful queued PR builds
+        if: github.event_name == 'merge_group'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
+        run: >-
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
+          --base "$BASE_SHA" --head "$HEAD_SHA"
 
       - name: Build pool
         run: ~/.elan/bin/lake build LeanPool
@@ -130,11 +209,6 @@ jobs:
           include-hidden-files: true
           retention-days: 7
 
-      - name: Install uv
-        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
-        with:
-          enable-cache: true
-
       - name: Generate site data
         run: |
           cd python
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 54b8c99cd4..62c752b08f 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -24,6 +24,8 @@ name: Lean Action CI
 # single-job workflow used.
 
 on:
+  merge_group:
+    types: [checks_requested]
   push:
     branches:
       - main
@@ -32,8 +34,12 @@ on:
       - 'lakefile.toml'
       - 'lean-toolchain'
       - 'lake-manifest.json'
+      - 'LeanPool/projects/**'
       - 'LeanPool/projects.yml'
       - 'python/lean_pool/quality.py'
+      - 'python/lean_pool/registry.py'
+      - 'python/lean_pool/indexes.py'
+      - 'python/lean_pool/queue_build.py'
       - 'python/lean_pool/validation_cache.py'
       - 'python/lean_pool/ci_artifacts.py'
       - 'python/lean_pool/ci_cache.py'
@@ -54,29 +60,6 @@ on:
       # PR #301 added a 210-file project onto `bump/v4.33.0-rc1` and got no
       # build, no linters, and no quality checks at all.
       - 'bump/**'
-    paths:
-      - 'README.md'
-      # Attribution-only PRs must still produce the required checks.
-      - 'NOTICE.extra.yml'
-      - '**/*.lean'
-      - 'lakefile.toml'
-      - 'lean-toolchain'
-      - 'lake-manifest.json'
-      - 'LeanPool/projects.yml'
-      - 'python/lean_pool/quality.py'
-      - 'python/lean_pool/validation_cache.py'
-      - 'python/lean_pool/ci_artifacts.py'
-      - 'python/lean_pool/ci_cache.py'
-      - 'python/lean_pool/ci_pr_build.py'
-      - 'python/lean_pool/ci_validation_artifacts.py'
-      - 'python/lean_pool/rebase_fastpath.py'
-      - 'python/pyproject.toml'
-      - 'python/uv.lock'
-      - 'scripts/nolints-style.txt'
-      - 'scripts/ci/**'
-      - '.github/CODE_QUALITY.md'
-      - '.github/workflows/notice.yml'
-      - '.github/workflows/lean_action_ci.yml'
   workflow_dispatch:
     inputs:
       force_full:
@@ -103,6 +86,7 @@ jobs:
     outputs:
       build_revision: ${{ steps.build-identity.outputs.revision }}
       base_build_revision: ${{ steps.build-identity.outputs.base_revision }}
+      minimal_build: ${{ steps.plan.outputs.minimal_build }}
       mode: ${{ steps.plan.outputs.mode }}
       matrix: ${{ steps.plan.outputs.matrix }}
       reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }}
@@ -113,10 +97,15 @@ jobs:
         with:
           fetch-depth: 0
 
+      - name: Install Python tooling runtime
+        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+        with:
+          enable-cache: true
+
       - name: Identify compiled Lean sources
         id: build-identity
         env:
-          BASE_REF: ${{ github.event.pull_request.base.sha || github.sha }}
+          BASE_REF: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.sha }}
         run: |
           set -euo pipefail
           revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)
@@ -139,14 +128,14 @@ jobs:
         id: plan
         env:
           EVENT_NAME: ${{ github.event_name }}
-          BASE_SHA: ${{ github.event.pull_request.base.sha }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
           BEFORE_SHA: ${{ github.event.before }}
           FORCE_FULL: ${{ inputs.force_full }}
           CACHE_MATCHED: ${{ steps.lake-cache.outputs.cache-matched-key }}
           GH_TOKEN: ${{ github.token }}
           REPOSITORY: ${{ github.repository }}
           PR_NUMBER: ${{ github.event.pull_request.number }}
-          PR_HEAD: ${{ github.event.pull_request.head.sha }}
+          PR_HEAD: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
         run: |
           set -euo pipefail
           diff_available=true
@@ -155,6 +144,9 @@ jobs:
           changed_files="$RUNNER_TEMP/changed-files.txt"
           : > "$changed_files"
           case "$EVENT_NAME" in
+            merge_group)
+              git diff --name-only "$BASE_SHA"..HEAD > "$changed_files"
+              ;;
             pull_request)
               git diff --name-only "$BASE_SHA"...HEAD > "$changed_files"
               ;;
@@ -171,6 +163,11 @@ jobs:
               diff_available=false
               ;;
           esac
+          minimal_build=false
+          if [ "$EVENT_NAME" = pull_request ] && grep -Eq '^(python/lean_pool/(exposition/|ci_artifacts.py$)|scripts/exposition/|.github/workflows/exposition-verify.yml$)' "$changed_files"; then
+            minimal_build=true
+          fi
+          echo "minimal_build=$minimal_build" >> "$GITHUB_OUTPUT"
           cold=false
           if [ -z "$CACHE_MATCHED" ]; then cold=true; fi
           plan=$(CHANGED_FILES_PATH="$changed_files" DIFF_AVAILABLE="$diff_available" \
@@ -178,8 +175,8 @@ jobs:
                  python3 scripts/ci/plan-build-shards.py)
           reuse_run_id=""
           previous_head=""
-          if [ "$EVENT_NAME" = "pull_request" ] && [ "$FORCE_FULL" != "true" ]; then
-            reuse=$(PYTHONPATH=python python3 -m lean_pool.rebase_fastpath decide \
+          if [ "$EVENT_NAME" = "pull_request" ] && [ "$FORCE_FULL" != "true" ] && [ "$minimal_build" != true ]; then
+            reuse=$(PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath decide \
               --repository "$REPOSITORY" --number "$PR_NUMBER" \
               --head "$PR_HEAD" --base "$BASE_SHA")
             if [ "$(echo "$reuse" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" = true ]; then
@@ -249,7 +246,8 @@ jobs:
           LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1'
         run: >-
           uv run --project python --group test pytest -q
-          python/tests/test_ci_pr_build.py -k 'test_lake_'
+          python/tests/test_ci_pr_build.py python/tests/test_indexes.py
+          -k 'test_lake_'
 
       - name: Install Mathlib cache
         id: mathlib-cache
@@ -275,8 +273,11 @@ jobs:
           REPOSITORY: ${{ github.repository }}
           BEFORE_SHA: ${{ github.event.before }}
         run: |
-          if git cat-file -e "$BEFORE_SHA" 2>/dev/null; then
-            PYTHONPATH=python python3 -m lean_pool.rebase_fastpath restore-main \
+          if PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build \
+            --repository "$REPOSITORY" --base "$BEFORE_SHA" --head "$GITHUB_SHA" --merged; then
+            echo 'Restored the successfully merged queue build.'
+          elif git cat-file -e "$BEFORE_SHA" 2>/dev/null; then
+            PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath restore-main \
               --repository "$REPOSITORY" --head "$BEFORE_SHA" --base "$GITHUB_SHA"
           fi
 
@@ -287,14 +288,25 @@ jobs:
           GH_TOKEN: ${{ github.token }}
           PR_NUMBER: ${{ github.event.pull_request.number }}
           PR_BRANCH: ${{ github.head_ref }}
-          PR_HEAD: ${{ github.event.pull_request.head.sha }}
-          PR_BASE: ${{ github.event.pull_request.base.sha }}
+          PR_HEAD: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
+          PR_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
           CURRENT_RUN: ${{ github.run_id }}
         run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_pr_build
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.ci_pr_build
           --number "$PR_NUMBER" --branch "$PR_BRANCH"
           --head "$PR_HEAD" --base "$PR_BASE" --current-run "$CURRENT_RUN"
 
+      - name: Reuse successful queued PR builds
+        if: github.event_name == 'merge_group'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
+        run: >-
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
+          --base "$BASE_SHA" --head "$HEAD_SHA"
+
       - name: Build project
         id: compilation
         run: |
@@ -306,13 +318,14 @@ jobs:
           fi
 
       # Publish once compilation succeeds, so docs can overlap the later
-      # linters/quality checks without compiling the same PR a second time.
+      # linters/quality checks. Rare PRs requiring the minimal-file gate share
+      # this exact-tree output too, avoiding a second cold whole-pool build.
       - name: Package build for documentation
-        if: github.event_name != 'pull_request'
+        if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true')
         run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack
 
       - name: Share build with documentation
-        if: github.event_name != 'pull_request'
+        if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true')
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
           name: lean-pool-build
@@ -344,6 +357,17 @@ jobs:
       - name: Install validation dependencies
         run: cd python && uv sync --locked
 
+      - name: Reuse successful queued PR validation
+        if: github.event_name == 'merge_group'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
+        run: >-
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
+          --base "$BASE_SHA" --head "$HEAD_SHA" --receipts
+
       - name: Lint
         run: |
           cd python
@@ -371,15 +395,15 @@ jobs:
           retention-days: 14
 
       - name: Package PR project build for later rebases
-        if: github.event_name == 'pull_request'
+        if: github.event_name == 'pull_request' || github.event_name == 'merge_group'
         continue-on-error: true
         env:
-          BASE_SHA: ${{ github.event.pull_request.base.sha }}
-          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
-        run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA"
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
+        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA"
 
       - name: Retain PR project build
-        if: github.event_name == 'pull_request'
+        if: github.event_name == 'pull_request' || github.event_name == 'merge_group'
         continue-on-error: true
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
@@ -591,6 +615,14 @@ jobs:
         with:
           enable-cache: true
 
+      - name: Check compiled artifact dependency tracking with pinned Lean
+        env:
+          LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1'
+        run: >-
+          uv run --project python --group test pytest -q
+          python/tests/test_ci_pr_build.py python/tests/test_indexes.py
+          -k 'test_lake_'
+
       - name: Install Mathlib cache
         id: mathlib-cache
         run: |
@@ -626,6 +658,17 @@ jobs:
       # With the shard outputs in place this is mostly cache replay; it
       # builds the root module and anything a shard missed or failed to
       # deliver, so the assembled pool is complete regardless.
+      - name: Reuse successful queued PR builds
+        if: github.event_name == 'merge_group'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
+        run: >-
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
+          --base "$BASE_SHA" --head "$HEAD_SHA"
+
       - name: Build project
         id: compilation
         run: |
@@ -637,13 +680,14 @@ jobs:
           fi
 
       # Publish once compilation succeeds, so docs can overlap the later
-      # linters/quality checks without compiling the same PR a second time.
+      # linters/quality checks. Rare PRs requiring the minimal-file gate share
+      # this exact-tree output too, avoiding a second cold whole-pool build.
       - name: Package build for documentation
-        if: github.event_name != 'pull_request'
+        if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true')
         run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack
 
       - name: Share build with documentation
-        if: github.event_name != 'pull_request'
+        if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true')
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
           name: lean-pool-build
@@ -675,6 +719,17 @@ jobs:
       - name: Install validation dependencies
         run: cd python && uv sync --locked
 
+      - name: Reuse successful queued PR validation
+        if: github.event_name == 'merge_group'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
+        run: >-
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
+          --base "$BASE_SHA" --head "$HEAD_SHA" --receipts
+
       - name: Lint
         run: |
           cd python
@@ -702,15 +757,15 @@ jobs:
           retention-days: 14
 
       - name: Package PR project build for later rebases
-        if: github.event_name == 'pull_request'
+        if: github.event_name == 'pull_request' || github.event_name == 'merge_group'
         continue-on-error: true
         env:
-          BASE_SHA: ${{ github.event.pull_request.base.sha }}
-          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
-        run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA"
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
+        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA"
 
       - name: Retain PR project build
-        if: github.event_name == 'pull_request'
+        if: github.event_name == 'pull_request' || github.event_name == 'merge_group'
         continue-on-error: true
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
@@ -806,6 +861,11 @@ jobs:
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
+      - name: Install uv
+        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+        with:
+          enable-cache: true
+
       - name: Reuse newly merged projects while the main cache warms
         if: steps.main-build.outputs.cache-hit != 'true'
         continue-on-error: true
@@ -813,9 +873,9 @@ jobs:
           GH_TOKEN: ${{ github.token }}
           REPOSITORY: ${{ github.repository }}
           PREVIOUS_HEAD: ${{ needs.plan.outputs.previous_head }}
-          BASE_SHA: ${{ github.event.pull_request.base.sha }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
         run: >-
-          PYTHONPATH=python python3 -m lean_pool.rebase_fastpath restore-main
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath restore-main
           --repository "$REPOSITORY" --head "$PREVIOUS_HEAD" --base "$BASE_SHA"
 
       - name: Restore previously validated PR modules
@@ -827,7 +887,7 @@ jobs:
           PREVIOUS_HEAD: ${{ needs.plan.outputs.previous_head }}
           REPOSITORY: ${{ github.repository }}
         run: >-
-          PYTHONPATH=python python3 -m lean_pool.rebase_fastpath restore
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath restore
           --repository "$REPOSITORY" --run-id "$RUN_ID" --head "$PREVIOUS_HEAD"
 
       - name: Install Lean
@@ -837,10 +897,13 @@ jobs:
           use-github-cache: false
           use-mathlib-cache: false
 
-      - name: Install uv
-        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
-        with:
-          enable-cache: true
+      - name: Check compiled artifact dependency tracking with pinned Lean
+        env:
+          LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1'
+        run: >-
+          uv run --project python --group test pytest -q
+          python/tests/test_ci_pr_build.py python/tests/test_indexes.py
+          -k 'test_lake_'
 
       - name: Install Mathlib cache
         run: |
@@ -849,7 +912,7 @@ jobs:
           fi
 
       - name: Check generated index
-        run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath check-index
+        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index
 
       - name: Build combined Lean root
         run: |
@@ -907,9 +970,9 @@ jobs:
       - name: Package PR project build for later rebases
         continue-on-error: true
         env:
-          BASE_SHA: ${{ github.event.pull_request.base.sha }}
-          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
-        run: PYTHONPATH=python python3 -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA"
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
+        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA"
 
       - name: Retain PR project build
         continue-on-error: true
diff --git a/.github/workflows/notice.yml b/.github/workflows/notice.yml
index 08956468a5..afe5ff1718 100644
--- a/.github/workflows/notice.yml
+++ b/.github/workflows/notice.yml
@@ -1,31 +1,28 @@
 name: Generated metadata
 
-# README.md and NOTICE are deterministic views of repository content. A
-# maintainer credential pushes their refresh directly to main so these small,
-# mechanical updates do not create a second PR for every content merge.
-
+# Generated files travel through the same protected queue as other changes.
+# Keep an existing metadata PR fixed while it is being checked. A subsequent
+# merge or scheduled refresh picks up content accepted since it was created.
 on:
   push:
-    branches:
-      - main
-    # The generated commit changes only README.md and NOTICE, neither of which
-    # is an input below, so it cannot trigger a commit loop.
+    branches: [main]
     paths:
       - 'LeanPool/**'
       - 'NOTICE.extra.yml'
       - 'python/lean_pool/notice.py'
       - 'python/lean_pool/stats.py'
       - '.github/workflows/notice.yml'
+  pull_request_target:
+    types: [closed]
+    paths: ['README.md', 'NOTICE']
+  schedule:
+    - cron: '17 * * * *'
   workflow_dispatch:
 
 concurrency:
-  # README and NOTICE share one writer. Runs queue rather than cancel so a
-  # newer merge cannot interrupt an older run while it is publishing.
   group: generated-metadata-main
   cancel-in-progress: false
 
-# The direct push uses REBASE_TOKEN. Keep the run's automatic GITHUB_TOKEN
-# read-only so it is not a second write credential.
 permissions:
   contents: read
 
@@ -38,53 +35,45 @@ jobs:
         with:
           fetch-depth: 0
           ref: main
-          # REBASE_TOKEN is a maintainer PAT. Main's protection allows the
-          # maintainer identity to publish these generated-only commits.
           token: ${{ secrets.REBASE_TOKEN }}
-
       - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
         with:
           enable-cache: true
-
       - name: Install dependencies
         run: cd python && uv sync --locked
-
-      - name: Regenerate and publish
+      - name: Publish one protected metadata PR
+        env:
+          GH_TOKEN: ${{ secrets.REBASE_TOKEN }}
+          REPO: ${{ github.repository }}
         run: |
           set -euo pipefail
-          git config user.name "github-actions[bot]"
-          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
-
-          # A content merge can advance main after checkout. Each retry starts
-          # from the new tip and regenerates both files, so the eventual commit
-          # includes every merged project and never needs a force-push.
-          for attempt in 1 2 3 4 5; do
-            echo "Publish attempt $attempt of 5."
-            git fetch origin main
-            git checkout --detach origin/main
-
-            (cd python && uv run python -m lean_pool.stats --repo ..)
-            (cd python && uv run python -m lean_pool.notice --repo ..)
-
-            unexpected="$(git diff --name-only \
-              | { grep -vE '^(NOTICE|README\.md)$' || true; })"
-            if [ -n "$unexpected" ]; then
-              echo "::error::Generators changed files outside README.md and NOTICE."
-              printf '%s\n' "$unexpected"
-              exit 1
-            fi
-            if git diff --quiet -- README.md NOTICE; then
-              echo "Generated metadata is already up to date."
-              exit 0
-            fi
-
-            git add README.md NOTICE
-            git commit -m "chore: refresh generated metadata"
-            if git push origin HEAD:main; then
-              exit 0
-            fi
-            echo "Main advanced during publish; regenerating from its new tip."
-          done
-
-          echo "::error::Could not publish generated metadata after five attempts."
-          exit 1
+          existing=$(gh pr list -R "$REPO" --state open --head codex/generated-metadata --json number --jq '.[0].number // empty')
+          if [ -n "$existing" ]; then
+            echo "Metadata PR #$existing is already being checked; retaining its head."
+            exit 0
+          fi
+          git fetch origin main
+          git checkout -b codex/generated-metadata origin/main
+          (cd python && uv run python -m lean_pool.stats --repo ..)
+          (cd python && uv run python -m lean_pool.notice --repo ..)
+          unexpected=$(git diff --name-only | { grep -vE '^(NOTICE|README\.md)$' || true; })
+          if [ -n "$unexpected" ]; then
+            echo '::error::Metadata generators changed other files.'
+            exit 1
+          fi
+          if git diff --quiet; then
+            echo 'Generated metadata is already current.'
+            exit 0
+          fi
+          git config user.name 'github-actions[bot]'
+          git config user.email '41898282+github-actions[bot]@users.noreply.github.com'
+          git add README.md NOTICE
+          git commit -m 'Refresh generated project statistics and attribution'
+          # The fixed branch may remain after its previous PR merged. Replace
+          # only that completed automation branch, never main or an open PR.
+          git push --force-with-lease origin HEAD:codex/generated-metadata
+          gh pr create -R "$REPO" --head codex/generated-metadata --base main \
+            --title 'Refresh generated project statistics and attribution' \
+            --body 'Regenerates README statistics and NOTICE from the accepted project cards and attribution notes. No proof sources change.'
+          gh pr merge -R "$REPO" codex/generated-metadata --squash --auto \
+            --match-head-commit "$(git rev-parse HEAD)"
diff --git a/.github/workflows/partial-port-audit.yml b/.github/workflows/partial-port-audit.yml
index 46f858e336..c27d6e68d5 100644
--- a/.github/workflows/partial-port-audit.yml
+++ b/.github/workflows/partial-port-audit.yml
@@ -5,7 +5,7 @@ on:
     paths:
       - 'LeanPool.lean'
       - 'LeanPool/**/*.lean'
-      - 'LeanPool/projects.yml'
+      - 'LeanPool/projects/**'
 
 permissions:
   contents: read
diff --git a/.github/workflows/python_ci.yml b/.github/workflows/python_ci.yml
index 87f2878fc8..223d086863 100644
--- a/.github/workflows/python_ci.yml
+++ b/.github/workflows/python_ci.yml
@@ -1,6 +1,8 @@
 name: Python CI
 
 on:
+  merge_group:
+    types: [checks_requested]
   push:
     branches:
       - main
@@ -14,19 +16,7 @@ on:
   pull_request:
     branches:
       - main
-    paths:
-      - 'python/**'
-      # NOTICE is generated (notice.yml); the pytest suite asserts the
-      # committed file matches its inputs, which catches hand-edits to
-      # either. LeanPool/projects.yml is deliberately absent: it is a
-      # content path, and a content PR cannot also update NOTICE, so
-      # gating on it here would be unsatisfiable. notice.yml regenerates
-      # after merge instead.
-      - 'NOTICE'
-      - 'NOTICE.extra.yml'
-      - '.github/workflows/python_ci.yml'
-      - '.github/workflows/lean_action_ci.yml'
-      - '.github/workflows/docs.yml'
+
   workflow_dispatch:
 
 concurrency:
@@ -37,10 +27,48 @@ permissions:
   contents: read
 
 jobs:
+  scope:
+    runs-on: ubuntu-latest
+    outputs:
+      applicable: ${{ steps.scope.outputs.applicable }}
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - id: scope
+        env:
+          EVENT: ${{ github.event_name }}
+          BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
+        run: |
+          applicable=true
+          if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then
+            applicable=false
+            if [ "$EVENT" = pull_request ]; then
+              files=$(git diff --name-only "$BASE"...HEAD)
+            else
+              files=$(git diff --name-only "$BASE"..HEAD)
+            fi
+            if printf '%s\n' "$files" | grep -Eq '^(python/|NOTICE$|NOTICE.extra.yml$|.github/workflows/(python_ci|lean_action_ci|docs).yml$)'; then
+              applicable=true
+            fi
+          fi
+          echo "applicable=$applicable" >> "$GITHUB_OUTPUT"
   lint:
+    needs: scope
+    if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false')
     runs-on: ubuntu-latest
     name: Lint (ruff)
     steps:
+      - name: Require successful change classification
+        env:
+          SCOPE_RESULT: ${{ needs.scope.result }}
+          APPLICABLE: ${{ needs.scope.outputs.applicable }}
+        run: |
+          if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then
+            echo "::error::Change classification failed; required validation cannot be skipped."
+            exit 1
+          fi
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
         with:
           persist-credentials: false
@@ -59,11 +87,23 @@ jobs:
         run: cd python && uv run ruff format --check .
 
   test:
+    needs: scope
+    if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false')
     runs-on: ubuntu-latest
     name: Test (pytest)
     steps:
+      - name: Require successful change classification
+        env:
+          SCOPE_RESULT: ${{ needs.scope.result }}
+          APPLICABLE: ${{ needs.scope.outputs.applicable }}
+        run: |
+          if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then
+            echo "::error::Change classification failed; required validation cannot be skipped."
+            exit 1
+          fi
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
         with:
+          fetch-depth: 0
           persist-credentials: false
 
       - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
@@ -73,6 +113,20 @@ jobs:
       - name: Install test dependencies
         run: cd python && uv sync --locked --group test
 
+      - name: Validate authored attribution and regenerate the combined test view
+        if: github.event_name == 'pull_request' || github.event_name == 'merge_group' || github.event_name == 'push'
+        env:
+          GH_TOKEN: ${{ github.token }}
+          EVENT: ${{ github.event_name }}
+          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }}
+          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha || github.sha }}
+        run: |
+          arguments=()
+          if [ "$EVENT" = pull_request ]; then arguments+=(--pull-request); fi
+          if [ "$EVENT" = push ]; then arguments+=(--main-push); fi
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_notice \
+            --base "$BASE_SHA" --head "$HEAD_SHA" "${arguments[@]}"
+
       - name: Pytest
         run: |
           cd python
diff --git a/.github/workflows/workflow_lint.yml b/.github/workflows/workflow_lint.yml
index 7640cfd6de..e8930e4776 100644
--- a/.github/workflows/workflow_lint.yml
+++ b/.github/workflows/workflow_lint.yml
@@ -1,6 +1,8 @@
 name: Workflow Lint
 
 on:
+  merge_group:
+    types: [checks_requested]
   push:
     branches:
       - main
@@ -9,8 +11,7 @@ on:
   pull_request:
     branches:
       - main
-    paths:
-      - '.github/**'
+
   workflow_dispatch:
 
 permissions:
diff --git a/.greptile/files.json b/.greptile/files.json
index da33836c13..c657891dba 100644
--- a/.greptile/files.json
+++ b/.greptile/files.json
@@ -14,15 +14,15 @@
     },
     {
       "path": ".github/REVIEW_RULES.md",
-      "description": "Shared rules for the repository's independent GPT-5.6 review rubrics."
+      "description": "Shared rules for the repository's independent LLM review rubrics."
     },
     {
       "path": ".github/CODE_QUALITY.md",
       "description": "Deterministic gates and code-quality conventions; avoid duplicating mechanical checks."
     },
     {
-      "path": "LeanPool/projects.yml",
-      "description": "Project registry used to check catalog consistency, prior overlap, and the established level of pooled projects."
+      "path": "python/lean_pool/registry.py",
+      "description": "Loads the independent YAML project cards under LeanPool/projects/. Check those cards for catalog consistency, prior overlap, and the established level of pooled projects."
     }
   ]
 }
diff --git a/.zenodo.json b/.zenodo.json
index 2645775113..638639c579 100644
--- a/.zenodo.json
+++ b/.zenodo.json
@@ -1,6 +1,6 @@
 {
   "title": "Lean Pool",
-  "description": "Lean Pool is a curated archive of Lean 4 formalizations that fall outside Mathlib's scope. It sits between Mathlib's high-bar human review and \"anything that compiles\": projects are admitted via deterministic linters (no sorry/admit, no extra axioms, no unsafe/partial) and LLM review, and are kept building against the latest Mathlib. The goal is an arXiv-style index of formal-mathematics developments that would otherwise bit-rot in abandoned repositories. Individual pooled projects remain the work of their original authors, recorded in LeanPool/projects.yml, the NOTICE file, and the per-file headers.",
+  "description": "Lean Pool is a curated archive of Lean 4 formalizations that fall outside Mathlib's scope. It sits between Mathlib's high-bar human review and \"anything that compiles\": projects are admitted via deterministic linters (no sorry/admit, no extra axioms, no unsafe/partial) and LLM review, and are kept building against the latest Mathlib. The goal is an arXiv-style index of formal-mathematics developments that would otherwise bit-rot in abandoned repositories. Individual pooled projects remain the work of their original authors, recorded in LeanPool/projects/, the NOTICE file, and the per-file headers.",
   "upload_type": "software",
   "access_right": "open",
   "license": "Apache-2.0",
@@ -20,7 +20,7 @@
   "related_identifiers": [
     {
       "relation": "isSupplementTo",
-      "identifier": "https://github.com/Vilin97/lean-pool",
+      "identifier": "https://github.com/LeanPool/lean-pool",
       "scheme": "url"
     }
   ]
diff --git a/AGENTS.md b/AGENTS.md
index 20b87c50e3..db356f2865 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -6,21 +6,21 @@ This file is a concatenation of README.md and CONTRIBUTING.md.
 
 # lean-pool
 
-[![Lean Action CI](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml)
-[![Documentation](https://img.shields.io/badge/docs-online-blue)](https://vilin97.github.io/lean-pool/)
-[![Exposition](https://img.shields.io/badge/exposition-online-8a4fff)](https://vilin97.github.io/lean-pool/exposition/)
+[![Lean Action CI](https://github.com/LeanPool/lean-pool/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/LeanPool/lean-pool/actions/workflows/lean_action_ci.yml)
+[![Documentation](https://img.shields.io/badge/docs-online-blue)](https://leanpool.github.io/lean-pool/)
+[![Exposition](https://img.shields.io/badge/exposition-online-8a4fff)](https://leanpool.github.io/lean-pool/exposition/)
 [![Zulip](https://img.shields.io/badge/Zulip-Lean_Pool-6492FE?logo=zulip&logoColor=white)](https://leanprover.zulipchat.com/#narrow/channel/619231-Lean-Pool)
-[![Semantic Search](https://img.shields.io/badge/semantic_search-Octo-2f80ed)](https://octo.axiomatic-ai.com/search?scopes=repo%3AVilin97%2Flean-pool)
-[![License](https://img.shields.io/github/license/Vilin97/lean-pool)](LICENSE)
+[![Semantic Search](https://img.shields.io/badge/semantic_search-Octo-2f80ed)](https://octo.axiomatic-ai.com/search?scopes=repo%3ALeanPool%2Flean-pool)
+[![License](https://img.shields.io/github/license/LeanPool/lean-pool)](LICENSE)
 [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20513444.svg)](https://doi.org/10.5281/zenodo.20513444)
 [![arXiv](https://img.shields.io/badge/arXiv-2609.25199-b31b1b)](https://arxiv.org/abs/2609.25199)
 
-Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://vilin97.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://vilin97.github.io/lean-pool/exposition/).
+Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://leanpool.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://leanpool.github.io/lean-pool/exposition/).
 
 Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search).
 
 <!-- BEGIN STATS -->
-**273** formalization projects · **5,801,081** lines of Lean
+**289** formalization projects · **9,933,135** lines of Lean
 <!-- END STATS -->
 
 <sub>(stats above are refreshed automatically by the [generated-metadata workflow](.github/workflows/notice.yml) — edit [`python/lean_pool/stats.py`](python/lean_pool/stats.py), not the numbers)</sub>
@@ -57,10 +57,10 @@ compile-cost report. Failed or zero-phase timed runs show unavailable timing
 and are excluded from totals; errors and any successfully measured heartbeat
 counts remain visible.
 
-Import PRs can be refreshed automatically after other projects merge. The
-[rebase helper](python/lean_pool/rebase.py) resolves conflicts in the project registry
-and generated index, preserving module headers and public imports when the index uses them.
-Conflicts in proof files require a manual rebase.
+Accepted PRs enter GitHub’s merge queue. CI checks the combined changes against
+current main without repeatedly updating authors’ branches. Each project owns
+its YAML card and public `Imports.lean`; there is no shared import list to edit.
+Conflicts in the same proof files still require a manual repair.
 
 ### Credits
 
@@ -110,7 +110,7 @@ If you would like to withdraw your project from Lean Pool, open an issue.
 There are two paths:
 
 - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt).
-- **Open a content PR.** Add your project under `LeanPool/<YourProject>/`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool/<YourProject>/Imports.lean`, which publicly imports every project source, and the single project import added to `LeanPool.lean`.
+- **Open a content PR.** Add your project under `LeanPool/<YourProject>/`, register it in [`LeanPool/projects/<slug>.yaml`](LeanPool/projects/) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool/<YourProject>/Imports.lean`, which publicly imports every project source. Lake discovers all pool modules automatically; keep `LeanPool.lean` unchanged. To use a project, import `LeanPool.<YourProject>.Imports`.
 
 Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.)
 
@@ -135,7 +135,7 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 ## Pull requests
 
-- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool.lean`, `LeanPool/**/*.lean`, and `LeanPool/projects.yml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml).
+- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool/**/*.lean` and `LeanPool/projects/<slug>.yaml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml).
 - **Never change the checks or gates.** Do not modify `.github/workflows/`, `.github/CODE_QUALITY.md`, `python/lean_pool/quality.py`, `scripts/nolints-style.txt`, the `[leanOptions]`/lint settings in `lakefile.toml`, or any other CI step or linter config — and do not add a waiver of any kind (a `size-limit-ok` comment, a `nolints-style.txt` entry, `set_option linter.X false`, etc.) — unless explicitly asked. If a check fails, fix the code, not the check. This applies to everyone, and especially to AI agents.
 - **Branches.** `yourname/description` for solo work; `feature/`/`fix/` prefixes when shared. Open PRs early (draft + `WIP` is fine) and use `Closes #123` to link issues.
 
diff --git a/CITATION.cff b/CITATION.cff
index 01342e7c8c..864ca72af6 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -31,8 +31,8 @@ keywords:
   - theorem proving
   - interactive theorem proving
 license: Apache-2.0
-repository-code: "https://github.com/Vilin97/lean-pool"
-url: "https://vilin97.github.io/lean-pool/"
+repository-code: "https://github.com/LeanPool/lean-pool"
+url: "https://leanpool.github.io/lean-pool/"
 version: 0.1.0
 date-released: "2026-06-02"
 
diff --git a/CLAUDE.md b/CLAUDE.md
index 20b87c50e3..db356f2865 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -6,21 +6,21 @@ This file is a concatenation of README.md and CONTRIBUTING.md.
 
 # lean-pool
 
-[![Lean Action CI](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml)
-[![Documentation](https://img.shields.io/badge/docs-online-blue)](https://vilin97.github.io/lean-pool/)
-[![Exposition](https://img.shields.io/badge/exposition-online-8a4fff)](https://vilin97.github.io/lean-pool/exposition/)
+[![Lean Action CI](https://github.com/LeanPool/lean-pool/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/LeanPool/lean-pool/actions/workflows/lean_action_ci.yml)
+[![Documentation](https://img.shields.io/badge/docs-online-blue)](https://leanpool.github.io/lean-pool/)
+[![Exposition](https://img.shields.io/badge/exposition-online-8a4fff)](https://leanpool.github.io/lean-pool/exposition/)
 [![Zulip](https://img.shields.io/badge/Zulip-Lean_Pool-6492FE?logo=zulip&logoColor=white)](https://leanprover.zulipchat.com/#narrow/channel/619231-Lean-Pool)
-[![Semantic Search](https://img.shields.io/badge/semantic_search-Octo-2f80ed)](https://octo.axiomatic-ai.com/search?scopes=repo%3AVilin97%2Flean-pool)
-[![License](https://img.shields.io/github/license/Vilin97/lean-pool)](LICENSE)
+[![Semantic Search](https://img.shields.io/badge/semantic_search-Octo-2f80ed)](https://octo.axiomatic-ai.com/search?scopes=repo%3ALeanPool%2Flean-pool)
+[![License](https://img.shields.io/github/license/LeanPool/lean-pool)](LICENSE)
 [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20513444.svg)](https://doi.org/10.5281/zenodo.20513444)
 [![arXiv](https://img.shields.io/badge/arXiv-2609.25199-b31b1b)](https://arxiv.org/abs/2609.25199)
 
-Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://vilin97.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://vilin97.github.io/lean-pool/exposition/).
+Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://leanpool.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://leanpool.github.io/lean-pool/exposition/).
 
 Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search).
 
 <!-- BEGIN STATS -->
-**273** formalization projects · **5,801,081** lines of Lean
+**289** formalization projects · **9,933,135** lines of Lean
 <!-- END STATS -->
 
 <sub>(stats above are refreshed automatically by the [generated-metadata workflow](.github/workflows/notice.yml) — edit [`python/lean_pool/stats.py`](python/lean_pool/stats.py), not the numbers)</sub>
@@ -57,10 +57,10 @@ compile-cost report. Failed or zero-phase timed runs show unavailable timing
 and are excluded from totals; errors and any successfully measured heartbeat
 counts remain visible.
 
-Import PRs can be refreshed automatically after other projects merge. The
-[rebase helper](python/lean_pool/rebase.py) resolves conflicts in the project registry
-and generated index, preserving module headers and public imports when the index uses them.
-Conflicts in proof files require a manual rebase.
+Accepted PRs enter GitHub’s merge queue. CI checks the combined changes against
+current main without repeatedly updating authors’ branches. Each project owns
+its YAML card and public `Imports.lean`; there is no shared import list to edit.
+Conflicts in the same proof files still require a manual repair.
 
 ### Credits
 
@@ -110,7 +110,7 @@ If you would like to withdraw your project from Lean Pool, open an issue.
 There are two paths:
 
 - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt).
-- **Open a content PR.** Add your project under `LeanPool/<YourProject>/`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool/<YourProject>/Imports.lean`, which publicly imports every project source, and the single project import added to `LeanPool.lean`.
+- **Open a content PR.** Add your project under `LeanPool/<YourProject>/`, register it in [`LeanPool/projects/<slug>.yaml`](LeanPool/projects/) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool/<YourProject>/Imports.lean`, which publicly imports every project source. Lake discovers all pool modules automatically; keep `LeanPool.lean` unchanged. To use a project, import `LeanPool.<YourProject>.Imports`.
 
 Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.)
 
@@ -135,7 +135,7 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 ## Pull requests
 
-- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool.lean`, `LeanPool/**/*.lean`, and `LeanPool/projects.yml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml).
+- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool/**/*.lean` and `LeanPool/projects/<slug>.yaml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml).
 - **Never change the checks or gates.** Do not modify `.github/workflows/`, `.github/CODE_QUALITY.md`, `python/lean_pool/quality.py`, `scripts/nolints-style.txt`, the `[leanOptions]`/lint settings in `lakefile.toml`, or any other CI step or linter config — and do not add a waiver of any kind (a `size-limit-ok` comment, a `nolints-style.txt` entry, `set_option linter.X false`, etc.) — unless explicitly asked. If a check fails, fix the code, not the check. This applies to everyone, and especially to AI agents.
 - **Branches.** `yourname/description` for solo work; `feature/`/`fix/` prefixes when shared. Open PRs early (draft + `WIP` is fine) and use `Closes #123` to link issues.
 
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 6a9a282d86..5426a5e591 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -11,7 +11,7 @@ If you would like to withdraw your project from Lean Pool, open an issue.
 There are two paths:
 
 - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt).
-- **Open a content PR.** Add your project under `LeanPool/<YourProject>/`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool/<YourProject>/Imports.lean`, which publicly imports every project source, and the single project import added to `LeanPool.lean`.
+- **Open a content PR.** Add your project under `LeanPool/<YourProject>/`, register it in [`LeanPool/projects/<slug>.yaml`](LeanPool/projects/) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool/<YourProject>/Imports.lean`, which publicly imports every project source. Lake discovers all pool modules automatically; keep `LeanPool.lean` unchanged. To use a project, import `LeanPool.<YourProject>.Imports`.
 
 Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.)
 
@@ -36,7 +36,7 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 ## Pull requests
 
-- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool.lean`, `LeanPool/**/*.lean`, and `LeanPool/projects.yml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml).
+- **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool/**/*.lean` and `LeanPool/projects/<slug>.yaml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml).
 - **Never change the checks or gates.** Do not modify `.github/workflows/`, `.github/CODE_QUALITY.md`, `python/lean_pool/quality.py`, `scripts/nolints-style.txt`, the `[leanOptions]`/lint settings in `lakefile.toml`, or any other CI step or linter config — and do not add a waiver of any kind (a `size-limit-ok` comment, a `nolints-style.txt` entry, `set_option linter.X false`, etc.) — unless explicitly asked. If a check fails, fix the code, not the check. This applies to everyone, and especially to AI agents.
 - **Branches.** `yourname/description` for solo work; `feature/`/`fix/` prefixes when shared. Open PRs early (draft + `WIP` is fine) and use `Closes #123` to link issues.
 
diff --git a/Makefile b/Makefile
index 8aebb6d158..69df983029 100644
--- a/Makefile
+++ b/Makefile
@@ -29,7 +29,7 @@ lint-fix:
 	cd python && uv run ruff check --fix
 	cd python && uv run ruff format
 
-# Verify LeanPool.lean imports the full file set (CI gate).
+# Verify every project aggregate contains its complete source set (CI gate).
 check:
 	lake exe mk_all --check
 
diff --git a/NOTICE b/NOTICE
index d0403815e0..837699fa08 100644
--- a/NOTICE
+++ b/NOTICE
@@ -8,11 +8,11 @@ file for the full license text.
 
 Lean Pool is an aggregation of third-party Lean 4 formalizations. Each project
 under LeanPool/ is the work of its original authors, who retain copyright as
-recorded in the per-file headers and in LeanPool/projects.yml. This NOTICE file
+recorded in the per-file headers and in the project registry. This NOTICE file
 records, for every pooled project, the upstream repository it was imported from
 and the license under which it was originally published.
 
-This file is generated by python/lean_pool/notice.py from LeanPool/projects.yml
+This file is generated by python/lean_pool/notice.py from the project registry
 and NOTICE.extra.yml. Do not edit it by hand -- edit those inputs instead.
 
 
@@ -172,6 +172,7 @@ Apache License, Version 2.0, and are redistributed here under the same license.
   LeanPool/MatchingLogic             https://github.com/eveil-labs/matching-logic-lean
   LeanPool/MaxFlowMinCut             https://github.com/jtraverso/erdos-81-chordal-clique-partitions
   LeanPool/MetricCodes               https://github.com/openai/ten-proofs
+  LeanPool/MicrowaveNetworks         https://github.com/matteonerini/formalizing-analog-computing
   LeanPool/MinModulusUniqueMultisetSum
                                      https://github.com/jarfo/min-modulus
   LeanPool/MinimumDegreeMatching     https://github.com/jtraverso/erdos-81-chordal-clique-partitions
@@ -379,6 +380,7 @@ MIT permission notice that follows them.
       "Copyright (c) 2026" with no name; the repository owner of record is
       "SamuelSchlesinger".
 
+  LeanPool/SmallUndecidableGroups    https://github.com/32805433/Adian-Rabin
   LeanPool/SteinhausThreeGap         https://github.com/dkunert/three-gap-theorem-lean
       Copyright (c) 2026 Dirk Kunert
 
diff --git a/README.md b/README.md
index a18b1c1b61..d943d82585 100644
--- a/README.md
+++ b/README.md
@@ -4,16 +4,16 @@
 
 # lean-pool
 
-[![Lean Action CI](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/Vilin97/lean-pool/actions/workflows/lean_action_ci.yml)
-[![Documentation](https://img.shields.io/badge/docs-online-blue)](https://vilin97.github.io/lean-pool/)
-[![Exposition](https://img.shields.io/badge/exposition-online-8a4fff)](https://vilin97.github.io/lean-pool/exposition/)
+[![Lean Action CI](https://github.com/LeanPool/lean-pool/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/LeanPool/lean-pool/actions/workflows/lean_action_ci.yml)
+[![Documentation](https://img.shields.io/badge/docs-online-blue)](https://leanpool.github.io/lean-pool/)
+[![Exposition](https://img.shields.io/badge/exposition-online-8a4fff)](https://leanpool.github.io/lean-pool/exposition/)
 [![Zulip](https://img.shields.io/badge/Zulip-Lean_Pool-6492FE?logo=zulip&logoColor=white)](https://leanprover.zulipchat.com/#narrow/channel/619231-Lean-Pool)
-[![Semantic Search](https://img.shields.io/badge/semantic_search-Octo-2f80ed)](https://octo.axiomatic-ai.com/search?scopes=repo%3AVilin97%2Flean-pool)
-[![License](https://img.shields.io/github/license/Vilin97/lean-pool)](LICENSE)
+[![Semantic Search](https://img.shields.io/badge/semantic_search-Octo-2f80ed)](https://octo.axiomatic-ai.com/search?scopes=repo%3ALeanPool%2Flean-pool)
+[![License](https://img.shields.io/github/license/LeanPool/lean-pool)](LICENSE)
 [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20513444.svg)](https://doi.org/10.5281/zenodo.20513444)
 [![arXiv](https://img.shields.io/badge/arXiv-2609.25199-b31b1b)](https://arxiv.org/abs/2609.25199)
 
-Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://vilin97.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://vilin97.github.io/lean-pool/exposition/).
+Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://leanpool.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://leanpool.github.io/lean-pool/exposition/).
 
 Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search).
 
@@ -55,10 +55,10 @@ compile-cost report. Failed or zero-phase timed runs show unavailable timing
 and are excluded from totals; errors and any successfully measured heartbeat
 counts remain visible.
 
-Import PRs can be refreshed automatically after other projects merge. The
-[rebase helper](python/lean_pool/rebase.py) resolves conflicts in the project registry
-and generated index, preserving module headers and public imports when the index uses them.
-Conflicts in proof files require a manual rebase.
+Accepted PRs enter GitHub’s merge queue. CI checks the combined changes against
+current main without repeatedly updating authors’ branches. Each project owns
+its YAML card and public `Imports.lean`; there is no shared import list to edit.
+Conflicts in the same proof files still require a manual repair.
 
 ### Credits
 
diff --git a/lakefile.toml b/lakefile.toml
index a260cee58d..12f2de6891 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -17,6 +17,7 @@ rev = "v4.35.0-rc3"
 
 [[lean_lib]]
 name = "LeanPool"
+globs = ["LeanPool.*"]
 
 [[lean_exe]]
 name = "mk_all"
diff --git a/python/ci-performance.md b/python/ci-performance.md
index 16e754f387..19beaf6e62 100644
--- a/python/ci-performance.md
+++ b/python/ci-performance.md
@@ -6,9 +6,9 @@ about 88 minutes for Mathlib and 94–101 minutes for pool documentation data.
 Two per-commit Lean caches were about 5 GiB each against a 10 GB cache limit.
 HTML rendering itself took about four minutes.
 
-Examples: [warm main run](https://github.com/Vilin97/lean-pool/actions/runs/35231792853),
-[cold main run](https://github.com/Vilin97/lean-pool/actions/runs/35253856245),
-[project PR run](https://github.com/Vilin97/lean-pool/actions/runs/35263858983).
+Examples: [warm main run](https://github.com/LeanPool/lean-pool/actions/runs/35231792853),
+[cold main run](https://github.com/LeanPool/lean-pool/actions/runs/35253856245),
+[project PR run](https://github.com/LeanPool/lean-pool/actions/runs/35263858983).
 
 ## Cache ownership
 
diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py
index cf9b5bdfd3..118778695e 100644
--- a/python/lean_pool/aggregator/__main__.py
+++ b/python/lean_pool/aggregator/__main__.py
@@ -236,12 +236,13 @@ def clone(
 )
 @click.option(
     "--projects-yml",
+    "--projects",
     "projects_yml_path",
-    type=click.Path(dir_okay=False, path_type=Path),
+    type=click.Path(dir_okay=True, path_type=Path),
     default=DEFAULT_PROJECTS_YML,
     show_default=True,
     help=(
-        "Path to LeanPool/projects.yml. Each project's optional "
+        "Project-card directory or historical registry file. Each project's optional "
         "`source.github_repo` field marks the upstream candidate as "
         "merged, putting a ✓ in the In Pool column. Pass a missing "
         "path to leave the column blank for every row."
diff --git a/python/lean_pool/aggregator/render.py b/python/lean_pool/aggregator/render.py
index ad18405bf1..5c1d818b58 100644
--- a/python/lean_pool/aggregator/render.py
+++ b/python/lean_pool/aggregator/render.py
@@ -24,6 +24,7 @@
 import yaml
 
 from lean_pool.aggregator.reservoir import Build, Package, ReservoirManifest
+from lean_pool.registry import load_document
 
 
 class Decision(TypedDict, total=False):
@@ -193,13 +194,13 @@ def count_lean_loc(clones_dir: Path, key: str) -> int | None:
 def load_pool_repos(projects_yml_path: Path) -> set[str]:
     """Load canonical GitHub keys for projects already merged into lean-pool.
 
-    Reads ``LeanPool/projects.yml`` and collects the
+    Reads the project registry and collects the
     ``source.github_repo`` field of each project that has one. Keys are
     normalised via :func:`canonical_key` so they match the keys produced
     by :func:`package_key` for Reservoir entries.
 
     Args:
-        projects_yml_path: Path to ``LeanPool/projects.yml``.
+        projects_yml_path: Project-card directory or historical registry file.
 
     Returns:
         Set of canonical ``owner/name`` keys. Empty if the file is
@@ -207,11 +208,15 @@ def load_pool_repos(projects_yml_path: Path) -> set[str]:
         fields. A malformed file is logged but not fatal so renderer
         output keeps working when ``projects.yml`` is being edited.
     """
-    if not projects_yml_path.is_file():
+    if (
+        not projects_yml_path.is_file()
+        and not projects_yml_path.is_dir()
+        and not (projects_yml_path.parent / "projects").is_dir()
+    ):
         return set()
     try:
-        data = yaml.safe_load(projects_yml_path.read_text()) or {}
-    except yaml.YAMLError as exc:
+        data = load_document(projects_yml_path)
+    except (yaml.YAMLError, ValueError, OSError) as exc:
         logger.warning("%s: invalid YAML: %s", projects_yml_path, exc)
         return set()
     if not isinstance(data, dict):
diff --git a/python/lean_pool/ci_artifacts.py b/python/lean_pool/ci_artifacts.py
index 0b234b0697..903239e556 100644
--- a/python/lean_pool/ci_artifacts.py
+++ b/python/lean_pool/ci_artifacts.py
@@ -223,6 +223,19 @@ def wait_for_artifact(repository: str, run: dict, wait_seconds: int) -> int | No
         time.sleep(min(20, max(0, deadline - time.monotonic())))
 
 
+def wait_for_build(repository: str, head: str, event: str, wait: int) -> int | None:
+    """Allow the producer workflow to appear, within one bounded waiting window."""
+    deadline = time.monotonic() + wait
+    while True:
+        run = matching_run(repository, head, event)
+        remaining = max(0, deadline - time.monotonic())
+        if run is not None:
+            return wait_for_artifact(repository, run, int(remaining))
+        if remaining == 0:
+            return None
+        time.sleep(min(20, remaining))
+
+
 def _pipe_payload(source: BinaryIO, destination: BinaryIO) -> None:
     """Feed the ZIP entry into the decompressor without materializing another file."""
     with destination:
@@ -282,10 +295,18 @@ def download_build(root: Path, repository: str, artifact: int) -> bool:
                 return _restore_archive(root, _artifact_payload(source, name))
 
 
-def reuse_build(root: Path, repository: str, head: str, event: str, wait: int) -> bool:
+def reuse_build(
+    root: Path,
+    repository: str,
+    head: str,
+    event: str,
+    wait: int,
+    *,
+    pull_request_artifact: bool = False,
+) -> bool:
     """Best-effort reuse; unavailable CI never removes the regular Lake build step."""
-    # PRs retain project rebase artifacts but do not publish this full archive.
-    if event == "pull_request":
+    # Only PRs requiring full minimal-file verification publish this archive.
+    if event == "pull_request" and not pull_request_artifact:
         LOGGER.info(
             "PRs do not publish full build artifacts; using the regular Lake build"
         )
@@ -323,14 +344,26 @@ def main() -> None:
     pack = commands.add_parser("pack")
     pack.add_argument("--output", type=Path, default=Path(ARCHIVE_NAME))
     restore = commands.add_parser("restore")
-    restore.add_argument("--repository", default=os.environ.get("GITHUB_REPOSITORY"))
-    restore.add_argument("--head", required=True)
-    restore.add_argument("--event", required=True)
-    restore.add_argument("--wait-seconds", type=int, default=7200)
+    waiting = commands.add_parser("wait")
+    for command in (restore, waiting):
+        command.add_argument(
+            "--repository", default=os.environ.get("GITHUB_REPOSITORY")
+        )
+        command.add_argument("--head", required=True)
+        command.add_argument("--event", required=True)
+        command.add_argument("--wait-seconds", type=int, default=7200)
+    restore.add_argument("--pull-request-artifact", action="store_true")
     arguments = parser.parse_args()
     logging.basicConfig(level=logging.INFO, format="ci-artifacts: %(message)s")
     if arguments.command == "pack":
         pack_build(Path.cwd(), arguments.output)
+    elif arguments.command == "wait":
+        wait_for_build(
+            arguments.repository,
+            arguments.head,
+            arguments.event,
+            arguments.wait_seconds,
+        )
     else:
         reuse_build(
             Path.cwd(),
@@ -338,6 +371,7 @@ def main() -> None:
             arguments.head,
             arguments.event,
             arguments.wait_seconds,
+            pull_request_artifact=arguments.pull_request_artifact,
         )
 
 
diff --git a/python/lean_pool/ci_validation_artifacts.py b/python/lean_pool/ci_validation_artifacts.py
index 16d75c544e..90ce8fde1f 100644
--- a/python/lean_pool/ci_validation_artifacts.py
+++ b/python/lean_pool/ci_validation_artifacts.py
@@ -52,6 +52,9 @@ def source_runs(
     """Promote merged PR passes on main; otherwise recover main's published passes."""
     result = []
     if event == "push":
+        queued = successful_queue_run(repository, head)
+        if queued is not None:
+            result.append((queued, True))
         for pull in github_json(f"repos/{repository}/commits/{head}/pulls"):
             if (
                 pull.get("merged_at")
@@ -76,6 +79,20 @@ def source_runs(
     return result
 
 
+def successful_queue_run(repository: str, head: str) -> int | None:
+    """Find the latest exact-head queue attempt; never hide a newer failure."""
+    query = urlencode({"event": "merge_group", "head_sha": head, "per_page": 10})
+    runs = github_json(
+        f"repos/{repository}/actions/workflows/lean_action_ci.yml/runs?{query}"
+    )["workflow_runs"]
+    latest = max(
+        (run for run in runs if run["head_sha"] == head),
+        key=lambda run: run["id"],
+        default=None,
+    )
+    return latest["id"] if latest and latest.get("conclusion") == "success" else None
+
+
 def download_receipts(repository: str, run: int) -> dict | None:
     """Read one bounded JSON member; never extract artifact paths into the checkout."""
     artifacts = github_json(
diff --git a/python/lean_pool/exposition/SCHEMA.md b/python/lean_pool/exposition/SCHEMA.md
index 5e81b01986..0b31d0b91b 100644
--- a/python/lean_pool/exposition/SCHEMA.md
+++ b/python/lean_pool/exposition/SCHEMA.md
@@ -9,7 +9,7 @@ steps:
    (JSONL). Kernel-level dependency edges are pre-resolved to human-written
    declarations; compiler-generated auxiliaries are tunnelled through.
 2. **Generator** (`python -m lean_pool.exposition`): reads the dump, the
-   project registry (`LeanPool/projects.yml`) and the Lean sources; computes
+   project registry (`LeanPool/projects/`) and the Lean sources; computes
    per-project layered layouts and stats; emits the static site.
 
 ## Extractor dump (JSONL, one line per declaration)
@@ -52,14 +52,14 @@ module ("Basic") with no registry card.
 Relative bases from `p/<Project>/index.html`: exposition root `../..`,
 doc-gen4 root `../../..`. doc-gen4 page for a non-private declaration
 `Foo.bar` in module `LeanPool.A.B`: `<docs-root>/LeanPool/A/B.html#Foo.bar`.
-GitHub source: `https://github.com/Vilin97/lean-pool/blob/main/<LeanPool/A/B.lean>#L<line>-L<endLine>`.
+GitHub source: `https://github.com/LeanPool/lean-pool/blob/main/<LeanPool/A/B.lean>#L<line>-L<endLine>`.
 
 ## `data/projects/<Project>.json` (shard)
 
 ```json
 {"schema": 1,
  "project": "ABCExceptions",
- "title": "…",                 // from projects.yml; null for pseudo-projects
+ "title": "…",                 // from project cards; null for pseudo-projects
  "provenance": "human",        // "human" | "AI" | "mix" | null
  "stats": {"nodes": 235, "loc": 4120, "edges": 817, "maxDepth": 14, "avgDepth": 3.71,
            "kinds": {"lemma": 120, "theorem": 75, "def": 37, "structure": 3}},
@@ -95,7 +95,7 @@ count of `LeanPool/<Project>.lean` plus every `.lean` file under
 ### Card metadata (schema 1.1, additive)
 
 Each shard additionally carries the project's registry card (from
-`LeanPool/projects.yml`, matched via `entry_module`'s last component;
+`LeanPool/projects/`, matched via `entry_module`'s last component;
 `card` is `null` for pseudo-projects):
 
 ```json
diff --git a/python/lean_pool/exposition/__main__.py b/python/lean_pool/exposition/__main__.py
index d00ae05ab9..0d87d0818b 100644
--- a/python/lean_pool/exposition/__main__.py
+++ b/python/lean_pool/exposition/__main__.py
@@ -25,7 +25,7 @@
     "repo_root",
     type=click.Path(exists=True, file_okay=False, path_type=Path),
     required=True,
-    help="Repository root containing LeanPool/ sources and projects.yml.",
+    help="Repository root containing LeanPool/ sources and project cards.",
 )
 @click.option(
     "--out",
diff --git a/python/lean_pool/exposition/extract.py b/python/lean_pool/exposition/extract.py
index 89c3bf6450..4c880911c3 100644
--- a/python/lean_pool/exposition/extract.py
+++ b/python/lean_pool/exposition/extract.py
@@ -21,6 +21,7 @@
 from pathlib import Path
 
 from lean_pool.exposition.source_text import SourceFile, module_skeleton
+from lean_pool.indexes import discovers_modules, project_modules
 
 LOGGER = logging.getLogger(__name__)
 OUTPUTS = ("declarations.jsonl", "commands.jsonl")
@@ -43,6 +44,11 @@ def file_digest(path: Path) -> str:
 
 def projects(root: Path) -> list[str]:
     """Read the generated index, including module-system import modifiers."""
+    if discovers_modules(root):
+        names = sorted(project_modules(root))
+        if any(not (root / f"LeanPool/{name}.lean").is_file() for name in names):
+            raise ValueError("project is missing its entry module")
+        return names
     source = SourceFile.from_text((root / "LeanPool.lean").read_text())
     names = sorted(
         {name.split(".")[1] for name in module_skeleton(source).local_imports}
diff --git a/python/lean_pool/exposition/generate.py b/python/lean_pool/exposition/generate.py
index 5660c79bcb..c37479e4db 100644
--- a/python/lean_pool/exposition/generate.py
+++ b/python/lean_pool/exposition/generate.py
@@ -1,7 +1,7 @@
 """Orchestrate generation of the static exposition site.
 
 Reads the extractor JSONL dump, the project registry
-(``LeanPool/projects.yml``) and the Lean sources under the repository root,
+(``LeanPool/projects/``) and the Lean sources under the repository root,
 computes per-project layered layouts and statistics, and writes the site
 described in ``SCHEMA.md``: ``data/projects/<Project>.json`` shards,
 ``data/index.json``, ``data/decls.json``, static assets copied verbatim from
@@ -20,8 +20,6 @@
 from datetime import UTC, datetime
 from pathlib import Path
 
-import yaml
-
 from lean_pool.exposition.cones import compute_cone_metrics
 from lean_pool.exposition.layout import compute_layout
 from lean_pool.exposition.source_text import (
@@ -30,6 +28,7 @@
     module_skeleton,
     statement_slice,
 )
+from lean_pool.registry import load_document
 
 logger = logging.getLogger(__name__)
 
@@ -43,7 +42,7 @@
 
 @dataclass
 class ProjectCard:
-    """Registry metadata for one project (from ``LeanPool/projects.yml``)."""
+    """Registry metadata for one project (from the project registry)."""
 
     title: str | None
     provenance: str | None
@@ -136,10 +135,13 @@ def _card_payload(entry: dict) -> dict:
 
 def load_project_cards(projects_yml_path: Path) -> dict[str, ProjectCard]:
     """Load registry metadata per project, keyed by entry-module last component."""
-    if not projects_yml_path.is_file():
+    if (
+        not projects_yml_path.is_file()
+        and not (projects_yml_path.parent / "projects").is_dir()
+    ):
         logger.warning("project registry not found: %s", projects_yml_path)
         return {}
-    data = yaml.safe_load(projects_yml_path.read_text(encoding="utf-8")) or {}
+    data = load_document(projects_yml_path)
     cards: dict[str, ProjectCard] = {}
     for entry in data.get("projects", []):
         entry_module = entry.get("entry_module") or ""
diff --git a/python/lean_pool/exposition/static/assets/graph.js b/python/lean_pool/exposition/static/assets/graph.js
index aa060fa43d..2ec855281c 100644
--- a/python/lean_pool/exposition/static/assets/graph.js
+++ b/python/lean_pool/exposition/static/assets/graph.js
@@ -17,7 +17,7 @@
   const MAX_LABEL_PX = 400; // widen the left label cull by one label width
   const KINDS = ['theorem', 'lemma', 'def', 'abbrev', 'instance', 'structure',
     'class', 'inductive', 'axiom', 'opaque'];
-  const GITHUB_BLOB = 'https://github.com/Vilin97/lean-pool/blob/main/';
+  const GITHUB_BLOB = 'https://github.com/LeanPool/lean-pool/blob/main/';
   const MONO = 'ui-monospace, SFMono-Regular, Menlo, Consolas, monospace';
 
   // ----- DOM ----------------------------------------------------------------
@@ -1424,7 +1424,7 @@
 
   // ----- minimal Lean file --------------------------------------------------------
 
-  const RAW_BASE = 'https://raw.githubusercontent.com/Vilin97/lean-pool/';
+  const RAW_BASE = 'https://raw.githubusercontent.com/LeanPool/lean-pool/';
   const PLAYGROUND_URL_LIMIT = 128000; // characters; beyond this, download only
 
   function fetchModuleSource(moduleIndex) {
diff --git a/python/lean_pool/exposition/static/assets/landing.js b/python/lean_pool/exposition/static/assets/landing.js
index d9e7ed8520..fe3693630e 100644
--- a/python/lean_pool/exposition/static/assets/landing.js
+++ b/python/lean_pool/exposition/static/assets/landing.js
@@ -253,7 +253,7 @@
     footer.append(`generated ${date} · commit `);
     const link = document.createElement("a");
     link.className = "mono";
-    link.href = `https://github.com/Vilin97/lean-pool/commit/${encodeURIComponent(data.commit || "")}`;
+    link.href = `https://github.com/LeanPool/lean-pool/commit/${encodeURIComponent(data.commit || "")}`;
     link.textContent = sha;
     footer.appendChild(link);
   }
diff --git a/python/lean_pool/exposition/static/decls/index.html b/python/lean_pool/exposition/static/decls/index.html
index 3600c40ec9..9940cd5908 100644
--- a/python/lean_pool/exposition/static/decls/index.html
+++ b/python/lean_pool/exposition/static/decls/index.html
@@ -15,7 +15,7 @@
       <a href="../">Projects</a>
       <a href="./" aria-current="page">Declarations</a>
       <a href="../../">API docs</a>
-      <a href="https://github.com/Vilin97/lean-pool">GitHub</a>
+      <a href="https://github.com/LeanPool/lean-pool">GitHub</a>
     </nav>
   </header>
 
diff --git a/python/lean_pool/exposition/static/index.html b/python/lean_pool/exposition/static/index.html
index 99511c2696..97c5f9a520 100644
--- a/python/lean_pool/exposition/static/index.html
+++ b/python/lean_pool/exposition/static/index.html
@@ -15,7 +15,7 @@
       <a href="./" aria-current="page">Projects</a>
       <a href="decls/">Declarations</a>
       <a href="../">API docs</a>
-      <a href="https://github.com/Vilin97/lean-pool">GitHub</a>
+      <a href="https://github.com/LeanPool/lean-pool">GitHub</a>
     </nav>
   </header>
 
diff --git a/python/lean_pool/exposition/templates/project.html b/python/lean_pool/exposition/templates/project.html
index ddb3bc5b93..8669f77766 100644
--- a/python/lean_pool/exposition/templates/project.html
+++ b/python/lean_pool/exposition/templates/project.html
@@ -13,7 +13,7 @@
       <a href="../../index.html">Projects</a>
       <a href="../../decls/index.html">Declarations</a>
       <a href="../../../index.html">API docs</a>
-      <a href="https://github.com/Vilin97/lean-pool" target="_blank" rel="noopener">GitHub</a>
+      <a href="https://github.com/LeanPool/lean-pool" target="_blank" rel="noopener">GitHub</a>
     </nav>
   </header>
   <section class="info-strip">
diff --git a/python/lean_pool/exposition/verify.py b/python/lean_pool/exposition/verify.py
index 33254df1dd..fe68f0aae2 100644
--- a/python/lean_pool/exposition/verify.py
+++ b/python/lean_pool/exposition/verify.py
@@ -24,7 +24,8 @@
 from pathlib import Path
 
 import click
-import yaml
+
+from lean_pool.registry import load_document
 
 logger = logging.getLogger(__name__)
 
@@ -50,9 +51,7 @@ class Outcome:
 
 def main_declaration_targets(repo_root: Path, site_dir: Path) -> list[Target]:
     """Every project card ``main_declarations`` entry with a generated shard."""
-    registry = yaml.safe_load(
-        (repo_root / "LeanPool" / "projects.yml").read_text(encoding="utf-8")
-    )
+    registry = load_document(repo_root / "LeanPool" / "projects.yml")
     targets: list[Target] = []
     for entry in registry.get("projects", []):
         entry_module = entry.get("entry_module") or ""
diff --git a/python/lean_pool/indexes.py b/python/lean_pool/indexes.py
index afc679fe60..74b36c2090 100644
--- a/python/lean_pool/indexes.py
+++ b/python/lean_pool/indexes.py
@@ -21,6 +21,28 @@
 # Production module-system packages must never revert to a flat index.
 REQUIRE_PROJECT_ROOTS = True
 
+DISCOVERY_ROOT = MODULE_HEADER + (
+    "-- Lake builds every LeanPool module directly. Import a project's\n"
+    "-- Imports module to use its complete public API.\n"
+)
+
+
+def discovers_modules(root: Path) -> bool:
+    """Recognize the layout whose build enumerates all sources without a root list."""
+    config = root / "lakefile.toml"
+    if not config.exists():
+        return False
+    try:
+        libraries = tomllib.loads(config.read_text()).get("lean_lib", [])
+    except tomllib.TOMLDecodeError:
+        # Lake rejects malformed configurations. Do not interpret them as
+        # permission to omit the existing aggregate coverage check.
+        return False
+    return any(
+        library.get("name") == "LeanPool" and library.get("globs") == ["LeanPool.*"]
+        for library in libraries
+    )
+
 
 def project_modules(root: Path) -> dict[str, list[str]]:
     """Group all source modules by their first component below LeanPool."""
@@ -64,8 +86,11 @@ def render_project_indexes(root: Path) -> dict[Path, str]:
         + "".join(f"public import {module}\n" for module in modules)
         for project, modules in projects.items()
     }
-    result[root / "LeanPool.lean"] = MODULE_HEADER + "".join(
-        f"public import LeanPool.{project}.Imports\n" for project in projects
+    result[root / "LeanPool.lean"] = (
+        DISCOVERY_ROOT
+        if discovers_modules(root) and not (root / "LeanPool/projects.yml").exists()
+        else MODULE_HEADER
+        + "".join(f"public import LeanPool.{project}.Imports\n" for project in projects)
     )
     return result
 
diff --git a/python/lean_pool/notice.py b/python/lean_pool/notice.py
index f0dc636e95..3dfbbc2c21 100644
--- a/python/lean_pool/notice.py
+++ b/python/lean_pool/notice.py
@@ -5,13 +5,13 @@
 maintained by hand, which silently drifted: by the time this generator was
 written, 75 of 141 projects had no entry at all.
 
-Everything the list sections need already lives in ``LeanPool/projects.yml``
+Everything the list sections need already lives in the project registry
 (each card declares ``license`` and ``source.github_repo``), so those are
 derived rather than typed. The prose that cannot be derived -- upstream MIT
 copyright lines, relicensing statements, and reproduced upstream NOTICE text
 -- lives in ``NOTICE.extra.yml``, keyed by project directory.
 
-Deliberately kept out of ``projects.yml``: that file is *content* under
+Deliberately kept out of the project cards: those files are *content* under
 ``.github/workflows/content-pr-guard.yml``, so a PR may not touch it
 alongside infrastructure. Keeping the prose in a separate infra-side file
 lets NOTICE regeneration stay a non-content change.
@@ -32,6 +32,8 @@
 
 import yaml
 
+from lean_pool.registry import load_document
+
 logger = logging.getLogger(__name__)
 
 # Column at which an entry's URL starts, matching the hand-written original.
@@ -51,11 +53,11 @@
 
 Lean Pool is an aggregation of third-party Lean 4 formalizations. Each project
 under LeanPool/ is the work of its original authors, who retain copyright as
-recorded in the per-file headers and in LeanPool/projects.yml. This NOTICE file
+recorded in the per-file headers and in the project registry. This NOTICE file
 records, for every pooled project, the upstream repository it was imported from
 and the license under which it was originally published.
 
-This file is generated by python/lean_pool/notice.py from LeanPool/projects.yml
+This file is generated by python/lean_pool/notice.py from the project registry
 and NOTICE.extra.yml. Do not edit it by hand -- edit those inputs instead."""
 
 APACHE_PREAMBLE = """\
@@ -106,8 +108,8 @@ def _load_yaml(path: Path) -> Any:
 
 
 def load_projects(root: Path) -> list[dict[str, Any]]:
-    """Read the project cards from ``LeanPool/projects.yml``."""
-    data = _load_yaml(root / "LeanPool" / "projects.yml")
+    """Read the project cards from the project registry."""
+    data = load_document(root / "LeanPool" / "projects.yml")
     if isinstance(data, dict):
         data = data.get("projects", [])
     return list(data or [])
diff --git a/python/lean_pool/partial_port_audit.py b/python/lean_pool/partial_port_audit.py
index 81ea0e9b9c..d635ab1a9d 100644
--- a/python/lean_pool/partial_port_audit.py
+++ b/python/lean_pool/partial_port_audit.py
@@ -13,9 +13,8 @@
 from pathlib import Path
 from typing import Any
 
-import yaml
-
 from lean_pool.quality import FORBIDDEN_SOUNDNESS, _strip_lean_comments
+from lean_pool.registry import read_revision
 
 DEFAULT_LOC_TOLERANCE = 0.10
 DEFAULT_MIN_UPSTREAM_LOC = 200
@@ -111,7 +110,7 @@ def changed_paths(repo: Path, base_ref: str, head_ref: str) -> list[str]:
 
 def load_projects(repo: Path, head_ref: str) -> list[dict[str, Any]]:
     """Load ``LeanPool/projects.yml`` from ``head_ref``."""
-    data = yaml.safe_load(git_show(repo, head_ref, PROJECTS_YML)) or {}
+    data = read_revision(repo, head_ref)
     projects = data.get("projects") or []
     return [project for project in projects if isinstance(project, dict)]
 
diff --git a/python/lean_pool/pr_advisory.py b/python/lean_pool/pr_advisory.py
index 0baaa01888..482225e879 100644
--- a/python/lean_pool/pr_advisory.py
+++ b/python/lean_pool/pr_advisory.py
@@ -1,7 +1,7 @@
 """Post project metadata advisory comments on open pull requests.
 
 The advisory is intentionally deterministic and does not execute pull request
-code. It reads ``LeanPool/projects.yml`` from the PR base and head commits via
+code. It reads the project registry from the PR base and head commits via
 the GitHub API, detects added or changed project entries, enriches those
 entries with source-repository metadata, then creates or updates a sticky PR
 conversation comment.
@@ -32,6 +32,8 @@
 
 import yaml
 
+from lean_pool.registry import remote_text
+
 ADVISORY_MARKER = "<!-- lean-pool-project-advisory -->"
 PROJECTS_PATH = "LeanPool/projects.yml"
 TOOLCHAIN_PATH = "lean-toolchain"
@@ -42,7 +44,7 @@
 
 @dataclass(frozen=True)
 class ProjectEntry:
-    """Project metadata read from ``LeanPool/projects.yml``."""
+    """Project metadata read from the project registry."""
 
     slug: str
     title: str
@@ -201,8 +203,8 @@ def advisory_rows_for_pr(
 ) -> list[AdvisoryRow]:
     """Build advisory rows for a pull request."""
     pr_ref = _fetch_pr_ref(repo_full_name, pr_number)
-    base_projects = _fetch_file_text(pr_ref.base_repo, PROJECTS_PATH, pr_ref.base_sha)
-    head_projects = _fetch_file_text(pr_ref.head_repo, PROJECTS_PATH, pr_ref.head_sha)
+    base_projects = remote_text(pr_ref.base_repo, pr_ref.base_sha, _fetch_file_text)
+    head_projects = remote_text(pr_ref.head_repo, pr_ref.head_sha, _fetch_file_text)
     if base_projects is None or head_projects is None:
         return []
 
diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py
index c23ae64e6d..7adf1cfdd9 100644
--- a/python/lean_pool/quality.py
+++ b/python/lean_pool/quality.py
@@ -13,12 +13,18 @@
 
 import yaml
 
-from lean_pool.indexes import project_modules, requires_project_roots, structure_errors
+from lean_pool.indexes import (
+    discovers_modules,
+    project_modules,
+    requires_project_roots,
+    structure_errors,
+)
+from lean_pool.registry import load_document
 from lean_pool.validation_cache import ValidationCache, pool_units
 
 ALLOWED_AXIOMS = {"propext", "Quot.sound", "Classical.choice"}
 CODE_QUALITY_URL = (
-    "https://github.com/Vilin97/lean-pool/blob/main/.github/CODE_QUALITY.md"
+    "https://github.com/LeanPool/lean-pool/blob/main/.github/CODE_QUALITY.md"
 )
 FILE_HEADERS_DOC = f"{CODE_QUALITY_URL}#7-file-headers"
 STATUS_VALUES = {"verified"}
@@ -202,6 +208,8 @@ def _parse_imports(text: str) -> list[str]:
 def _reachable_leanpool_files(root: Path, entry_module: str = "LeanPool") -> set[Path]:
     reachable: set[Path] = set()
     pending = [entry_module]
+    if entry_module == "LeanPool" and discovers_modules(root):
+        pending.extend(f"LeanPool.{name}.Imports" for name in project_modules(root))
     root_module = entry_module.split(".")[0]
 
     while pending:
@@ -602,7 +610,12 @@ def main (args : List String) : IO UInt32 := do
 
 def _check_option_backdoors(root: Path) -> list[_QualityError]:
     """Audit every compiled pool declaration for backdoors."""
-    return _run_option_audit(root, ["LeanPool"])
+    return _run_option_audit(
+        root,
+        [m for unit in pool_units(root) for m in unit]
+        if discovers_modules(root)
+        else ["LeanPool"],
+    )
 
 
 def _run_option_audit(
@@ -679,7 +692,13 @@ def _parse_option_audit_output(
 
 def _check_axioms(root: Path) -> list[_QualityError]:
     """Audit pooled declarations: allowlisted axioms only, never `sorry`."""
-    return _audit_axioms(root, _parse_declarations(root), "LeanPool")
+    return _audit_axioms(
+        root,
+        _parse_declarations(root),
+        [m for unit in pool_units(root) for m in unit]
+        if discovers_modules(root)
+        else "LeanPool",
+    )
 
 
 def _audit_axioms(
@@ -840,14 +859,16 @@ def _load_projects_yaml(
     root: Path,
 ) -> tuple[dict[str, Any] | None, list[_QualityError]]:
     path = root / "LeanPool" / "projects.yml"
-    if not path.exists():
+    if not path.exists() and not (path.parent / "projects").is_dir():
         return None, [_QualityError(path, 1, "missing LeanPool/projects.yml")]
+    if (path.parent / "projects").is_dir():
+        path = path.parent / "projects"
     try:
-        data = yaml.safe_load(path.read_text()) or {}
-    except yaml.YAMLError as error:
+        data = load_document(path)
+    except (yaml.YAMLError, ValueError, OSError) as error:
         return None, [_QualityError(path, 1, f"invalid YAML: {error}")]
     if not isinstance(data, dict):
-        return None, [_QualityError(path, 1, "projects.yml must contain a mapping")]
+        return None, [_QualityError(path, 1, "project registry must contain a mapping")]
     return data, []
 
 
@@ -862,6 +883,8 @@ def _check_projects(
         return errors
 
     path = root / "LeanPool" / "projects.yml"
+    if (path.parent / "projects").is_dir():
+        path = path.parent / "projects"
     projects = data.get("projects", [])
     errors.extend(_check_project_container(path, projects))
     if errors:
@@ -884,7 +907,9 @@ def _check_projects(
         errors.extend(
             _check_project(
                 root,
-                path,
+                (root / "LeanPool/projects" / f"{project['slug']}.yaml")
+                if (root / "LeanPool/projects").is_dir()
+                else path,
                 index,
                 project,
                 validation_cache,
@@ -958,7 +983,11 @@ def _check_project_entry_imports(
         # Each project root directly imports its registered entry and all sources.
         imports = {
             imported
-            for module in imports
+            for module in (
+                {f"LeanPool.{name}.Imports" for name in project_modules(root)}
+                if discovers_modules(root)
+                else imports
+            )
             if module.endswith(".Imports")
             for path in [_module_to_path(root, module)]
             if path.exists()
@@ -971,10 +1000,17 @@ def _check_project_entry_imports(
     }
     return [
         _QualityError(
-            index_path,
+            root / "LeanPool" / module.split(".")[1] / "Imports.lean"
+            if discovers_modules(root) and module.startswith("LeanPool.")
+            else index_path,
             1,
-            f"project entry module {module} is not imported by LeanPool.lean; "
-            "run `lake exe mk_all`",
+            f"project entry module {module} is not imported by "
+            + (
+                "a project Imports module; "
+                if discovers_modules(root)
+                else "LeanPool.lean; "
+            )
+            + "run `lake exe mk_all`",
         )
         for module in sorted(entry_modules - imports)
     ]
@@ -1518,7 +1554,7 @@ def _parse_args(argv: list[str]) -> argparse.Namespace:
     parser.add_argument(
         "--write-project-cards",
         action="store_true",
-        help="Rewrite project-card module docstrings from LeanPool/projects.yml.",
+        help="Rewrite project-card module docstrings from the project registry.",
     )
     return parser.parse_args(argv)
 
diff --git a/python/lean_pool/queue_build.py b/python/lean_pool/queue_build.py
new file mode 100644
index 0000000000..be7c1c57f9
--- /dev/null
+++ b/python/lean_pool/queue_build.py
@@ -0,0 +1,120 @@
+"""Reuse verified constituent PR outputs while retaining the complete queue build."""
+
+from __future__ import annotations
+
+import argparse
+import json
+import logging
+import os
+import re
+import subprocess
+from pathlib import Path
+
+from lean_pool import ci_pr_build, ci_validation_artifacts, rebase_fastpath
+
+LOGGER = logging.getLogger(__name__)
+
+
+def candidate_runs(root: Path, repository: str, base: str, head: str) -> list[dict]:
+    """Find green PR heads named by GitHub's squash-generated queue commits."""
+    messages = rebase_fastpath.git(root, "log", "--format=%s", f"{base}..{head}")
+    numbers = sorted(
+        {int(n) for n in re.findall(r"\(#(\d+)\)$", messages, re.MULTILINE)}
+    )
+    result = []
+    for number in numbers:
+        pull = rebase_fastpath.github_json(f"repos/{repository}/pulls/{number}")
+        if (
+            pull["base"]["repo"]["full_name"] != repository
+            or pull["base"]["ref"] != "main"
+        ):
+            continue
+        previous = pull["head"]["sha"]
+        if not rebase_fastpath.SHA.fullmatch(previous):
+            continue
+        if not rebase_fastpath._exists_at(root, previous, "lakefile.toml"):
+            subprocess.run(["git", "fetch", "origin", previous], cwd=root, check=True)
+        run = ci_validation_artifacts.successful_pr_run(repository, number, previous)
+        if run is not None and ci_pr_build.sources_match(
+            root, previous, pull["base"]["sha"]
+        ):
+            result.append({"run": run, "head": previous, "base": pull["base"]["sha"]})
+    return result
+
+
+def merge_owned_receipts(root: Path, incoming: dict, projects: list[str]) -> None:
+    """Promote only a PR's own units; existing hash validation remains authoritative."""
+    path = root / ".lake/validation-cache/v1/passes.json"
+    try:
+        current = ci_validation_artifacts.receipts(path.read_bytes())
+    except (OSError, ValueError):
+        current = {}
+    for key, value in incoming.items():
+        module = key.partition(":")[2]
+        if any(
+            module == f"LeanPool.{p}" or module.startswith(f"LeanPool.{p}.")
+            for p in projects
+        ):
+            current[key] = value
+    path.parent.mkdir(parents=True, exist_ok=True)
+    temporary = path.with_suffix(".tmp")
+    temporary.write_text(json.dumps({"version": 1, "receipts": current}) + "\n")
+    temporary.replace(path)
+
+
+def restore_merged_group(root: Path, repository: str, head: str) -> bool:
+    """Restore one combined queue archive on main before its cache is published."""
+    run = ci_validation_artifacts.successful_queue_run(repository, head)
+    if run is None:
+        return False
+    rebase_fastpath.restore(root, repository, run, head)
+    return True
+
+
+def main() -> None:
+    """Try queue-specific recovery before ordinary compilation or validation."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--repository", default=os.environ.get("GITHUB_REPOSITORY", ""))
+    parser.add_argument("--base", required=True)
+    parser.add_argument("--head", required=True)
+    parser.add_argument("--receipts", action="store_true")
+    parser.add_argument("--merged", action="store_true")
+    args = parser.parse_args()
+    root = Path.cwd()
+    logging.basicConfig(level=logging.INFO)
+    if args.merged:
+        try:
+            restored = restore_merged_group(root, args.repository, args.head)
+        except ci_pr_build.RECOVERY_ERRORS:
+            LOGGER.exception("Merged queue archive unavailable; use ordinary recovery")
+            restored = False
+        raise SystemExit(0 if restored else 1)
+    try:
+        candidates = candidate_runs(root, args.repository, args.base, args.head)
+    except ci_pr_build.RECOVERY_ERRORS:
+        LOGGER.exception("Queue recovery unavailable; ordinary checks remain")
+        return
+    for candidate in candidates:
+        try:
+            if args.receipts:
+                incoming = ci_validation_artifacts.download_receipts(
+                    args.repository, candidate["run"]
+                )
+                if incoming is not None:
+                    projects = rebase_fastpath._projects(
+                        root, candidate["base"], candidate["head"]
+                    )
+                    merge_owned_receipts(root, incoming, projects)
+            else:
+                rebase_fastpath.restore(
+                    root, args.repository, candidate["run"], candidate["head"]
+                )
+            LOGGER.info("Recovered queued PR outputs from run %s", candidate["run"])
+        except ci_pr_build.RECOVERY_ERRORS:
+            LOGGER.exception(
+                "Candidate unavailable; normal compilation and validation remain"
+            )
+
+
+if __name__ == "__main__":
+    main()
diff --git a/python/lean_pool/queue_guard.py b/python/lean_pool/queue_guard.py
new file mode 100644
index 0000000000..1e294ae1d2
--- /dev/null
+++ b/python/lean_pool/queue_guard.py
@@ -0,0 +1,88 @@
+"""Apply the content separation policy to each PR's commit in a merge group."""
+
+from __future__ import annotations
+
+import argparse
+import re
+import subprocess
+from pathlib import Path
+
+BUMP_METADATA = {
+    "lean-toolchain",
+    "lakefile.toml",
+    "lake-manifest.json",
+    "docbuild/lean-toolchain",
+    "docbuild/lakefile.toml",
+    "docbuild/lake-manifest.json",
+    ".github/workflows/content-pr-guard.yml",
+}
+
+
+def is_content(path: str) -> bool:
+    """Identify proof sources and their per-project metadata."""
+    return bool(re.fullmatch(r"LeanPool/projects/[A-Za-z0-9_-]+\.yaml", path)) or (
+        path.startswith("LeanPool/") and path.endswith(".lean")
+    )
+
+
+def separation_errors(paths: list[str], *, legacy: bool = False) -> list[str]:
+    """Retain the existing version-bump exception without permitting mixed PRs."""
+    if "LeanPool.lean" in paths and not legacy:
+        return ["LeanPool.lean is fixed; content PRs must not edit it"]
+    content = [
+        path
+        for path in paths
+        if is_content(path)
+        or (legacy and path in {"LeanPool.lean", "LeanPool/projects.yml"})
+    ]
+    other = set(paths) - set(content)
+    if content and other - BUMP_METADATA:
+        return sorted(other - BUMP_METADATA)
+    return []
+
+
+def group_changes(root: Path, base: str, head: str) -> list[list[str]]:
+    """Read separate squash commits so unrelated PRs are never graded as one PR."""
+
+    def git(*arguments: str) -> str:
+        return subprocess.check_output(["git", *arguments], cwd=root, text=True)
+
+    git("merge-base", "--is-ancestor", base, head)
+    commits = git("rev-list", "--reverse", f"{base}..{head}").splitlines()
+    if not commits:
+        raise ValueError("merge group contains no commits")
+    result = []
+    for commit in commits:
+        if len(git("rev-list", "--parents", "-n", "1", commit).split()) != 2:
+            raise ValueError("merge queue must use squash commits")
+        result.append(
+            git("diff", "--name-only", "-z", f"{commit}^", commit)
+            .strip("\0")
+            .split("\0")
+        )
+    return result
+
+
+def main() -> None:
+    """Fail the queue gate if any constituent PR violates separation."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--base", required=True)
+    parser.add_argument("--head", required=True)
+    arguments = parser.parse_args()
+    legacy = (
+        subprocess.run(
+            ["git", "cat-file", "-e", f"{arguments.base}:LeanPool/projects.yml"],
+            capture_output=True,
+            check=False,
+        ).returncode
+        == 0
+    )
+    for paths in group_changes(Path.cwd(), arguments.base, arguments.head):
+        errors = separation_errors(paths, legacy=legacy)
+        if errors:
+            raise SystemExit("Content separation failed: " + ", ".join(errors))
+    print("Every queued PR preserves content separation")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/python/lean_pool/queue_notice.py b/python/lean_pool/queue_notice.py
new file mode 100644
index 0000000000..8345a3637d
--- /dev/null
+++ b/python/lean_pool/queue_notice.py
@@ -0,0 +1,152 @@
+"""Validate submitted attribution snapshots before regenerating a combined view."""
+
+from __future__ import annotations
+
+import argparse
+import os
+import re
+import subprocess
+import tempfile
+from pathlib import Path
+
+import yaml
+
+from lean_pool import notice, registry
+from lean_pool.ci_artifacts import github_json
+
+
+def git(root: Path, *arguments: str) -> str:
+    """Read exact queue and constituent objects without changing the checkout."""
+    return subprocess.check_output(["git", *arguments], cwd=root, text=True)
+
+
+def validate_snapshot(root: Path, revision: str, expected_notice: str) -> None:
+    """Reject hand-edited attribution against the submitting PR's own registry."""
+    projects = registry.read_revision(root, revision)["projects"]
+    extra = yaml.safe_load(git(root, "show", f"{revision}:NOTICE.extra.yml")) or {}
+    if notice.unregistered_notes(projects, extra):
+        raise ValueError("Attribution notes refer to unknown projects")
+    if notice.render(projects, extra) != expected_notice:
+        raise ValueError("Submitted NOTICE does not match its own project registry")
+
+
+def write_test_view(root: Path) -> None:
+    """Prepare generated attribution without following a checkout-controlled link."""
+    with tempfile.NamedTemporaryFile(
+        mode="w", dir=root, prefix=".notice-test-", delete=False
+    ) as output:
+        temporary = Path(output.name)
+        try:
+            output.write(notice.build(root))
+        except BaseException:
+            temporary.unlink()
+            raise
+    temporary.replace(root / "NOTICE")
+
+
+def prepare_pull_request(root: Path, base: str, submitted_head: str) -> None:
+    """Validate authored edits separately from stale inherited generated files."""
+    ancestor = git(root, "merge-base", base, submitted_head).strip()
+    changed = git(root, "diff", "--name-only", ancestor, submitted_head).splitlines()
+    if "NOTICE" in changed:
+        validate_snapshot(
+            root, submitted_head, git(root, "show", f"{submitted_head}:NOTICE")
+        )
+    write_test_view(root)
+
+
+def validate_merged_snapshot(
+    root: Path, repository: str, commit: str, submitted: str
+) -> None:
+    """Identify a merged PR by GitHub association, rather than its commit title."""
+    pulls = github_json(f"repos/{repository}/commits/{commit}/pulls?per_page=100")
+    for pull in pulls:
+        if (
+            not pull.get("merged_at")
+            or pull.get("merge_commit_sha") != commit
+            or pull["base"]["repo"]["full_name"] != repository
+            or pull["base"]["ref"] != "main"
+        ):
+            continue
+        previous = pull["head"]["sha"]
+        if not re.fullmatch("[0-9a-f]{40}", previous):
+            raise ValueError("Invalid merged PR head")
+        subprocess.run(["git", "fetch", "origin", previous], cwd=root, check=True)
+        if submitted != git(root, "show", f"{previous}:NOTICE"):
+            raise ValueError("Merged NOTICE does not match the submitted PR")
+        validate_snapshot(root, previous, submitted)
+        return
+    raise ValueError("Merged NOTICE does not match its own project registry")
+
+
+def prepare_main_push(root: Path, repository: str, base: str, head: str) -> None:
+    """Check main snapshots, allowing verified older metadata PR attribution."""
+    commits = git(
+        root, "rev-list", "--first-parent", "--reverse", f"{base}..{head}"
+    ).splitlines()
+    for commit in commits:
+        changed = git(root, "diff", "--name-only", f"{commit}^", commit).splitlines()
+        if "NOTICE" not in changed:
+            continue
+        submitted = git(root, "show", f"{commit}:NOTICE")
+        try:
+            validate_snapshot(root, commit, submitted)
+        except ValueError:
+            # An independent content merge may precede a metadata PR whose
+            # attribution was correctly generated on an older project set.
+            validate_merged_snapshot(root, repository, commit, submitted)
+    write_test_view(root)
+
+
+def prepare(root: Path, repository: str, base: str, head: str) -> None:
+    """Check each edited NOTICE, then include all queued projects in the test view."""
+    commits = git(root, "rev-list", "--reverse", f"{base}..{head}").splitlines()
+    for commit in commits:
+        changed = git(root, "diff", "--name-only", f"{commit}^", commit).splitlines()
+        if "NOTICE" not in changed:
+            continue
+        subject = git(root, "show", "-s", "--format=%s", commit).strip()
+        match = re.search(r"\(#(\d+)\)$", subject)
+        if match is None:
+            raise ValueError("Cannot identify attribution PR in merge queue")
+        pull = github_json(f"repos/{repository}/pulls/{match[1]}")
+        if (
+            pull["base"]["repo"]["full_name"] != repository
+            or pull["base"]["ref"] != "main"
+        ):
+            raise ValueError("Attribution PR belongs to a different base repository")
+        previous = pull["head"]["sha"]
+        if not re.fullmatch("[0-9a-f]{40}", previous):
+            raise ValueError("Invalid constituent head")
+        subprocess.run(["git", "fetch", "origin", previous], cwd=root, check=True)
+        submitted = git(root, "show", f"{commit}:NOTICE")
+        if submitted != git(root, "show", f"{previous}:NOTICE"):
+            raise ValueError("Queue attribution differs from the submitted PR")
+        validate_snapshot(root, previous, submitted)
+    # Content-only PRs already leave generated NOTICE temporarily stale. A
+    # combined queue must retain that policy while validating every edited
+    # snapshot above and testing the full generator on the combined registry.
+    write_test_view(root)
+
+
+def main() -> None:
+    """Prepare attribution for the ordinary full Python suite on merge groups."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--base", required=True)
+    parser.add_argument("--head", required=True)
+    event = parser.add_mutually_exclusive_group()
+    event.add_argument("--pull-request", action="store_true")
+    event.add_argument("--main-push", action="store_true")
+    args = parser.parse_args()
+    if args.pull_request:
+        prepare_pull_request(Path.cwd(), args.base, args.head)
+    elif args.main_push:
+        prepare_main_push(
+            Path.cwd(), os.environ["GITHUB_REPOSITORY"], args.base, args.head
+        )
+    else:
+        prepare(Path.cwd(), os.environ["GITHUB_REPOSITORY"], args.base, args.head)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/python/lean_pool/rebase_fastpath.py b/python/lean_pool/rebase_fastpath.py
index cb1ea9804d..4066cfa39e 100644
--- a/python/lean_pool/rebase_fastpath.py
+++ b/python/lean_pool/rebase_fastpath.py
@@ -24,6 +24,7 @@
 from urllib.parse import urlencode
 
 from lean_pool.indexes import requires_project_roots, structure_errors
+from lean_pool.registry import card_path, read_revision
 
 ARTIFACT = "rebase-project-build"
 ARCHIVE = f"{ARTIFACT}.tar.gz"
@@ -66,8 +67,10 @@ def github_json(endpoint: str) -> Any:
 
 
 def _content_path(path: str) -> bool:
-    return path in {INDEX, REGISTRY} or (
-        path.startswith("LeanPool/") and path.endswith(".lean")
+    return (
+        path in {INDEX, REGISTRY}
+        or card_path(path)
+        or (path.startswith("LeanPool/") and path.endswith(".lean"))
     )
 
 
@@ -91,6 +94,11 @@ def _exists_at(root: Path, revision: str, path: str) -> bool:
 
 def _registry_cards(root: Path, revision: str) -> dict[str, str]:
     """Split the repository's slug-first registry, rejecting unfamiliar layouts."""
+    if not _exists_at(root, revision, REGISTRY):
+        return {
+            card["slug"]: json.dumps(card, sort_keys=True)
+            for card in read_revision(root, revision)["projects"]
+        }
     source = git(root, "show", f"{revision}:{REGISTRY}")
     if not source.startswith("projects:\n"):
         raise ValueError("unrecognized project registry layout")
diff --git a/python/lean_pool/rebase_queue.py b/python/lean_pool/rebase_queue.py
index a693777496..8f4e1ef822 100644
--- a/python/lean_pool/rebase_queue.py
+++ b/python/lean_pool/rebase_queue.py
@@ -9,6 +9,8 @@
 from pathlib import Path
 from typing import Any
 
+from lean_pool.registry import card_path
+
 
 def checks_finished(pull: dict[str, Any]) -> bool:
     """Require observed checks to finish before replacing the checked revision."""
@@ -57,6 +59,7 @@ def content_only(root: Path, base: str, head: str) -> bool:
     paths = [path.decode() for path in changed if path]
     return bool(paths) and all(
         path in {"LeanPool.lean", "LeanPool/projects.yml"}
+        or card_path(path)
         or (path.startswith("LeanPool/") and path.endswith(".lean"))
         for path in paths
     )
diff --git a/python/lean_pool/registry.py b/python/lean_pool/registry.py
new file mode 100644
index 0000000000..8e16699b14
--- /dev/null
+++ b/python/lean_pool/registry.py
@@ -0,0 +1,191 @@
+"""Read per-project cards consistently, including historical monolithic registries."""
+
+from __future__ import annotations
+
+import argparse
+import json
+import re
+import subprocess
+from collections.abc import Callable
+from pathlib import Path
+from typing import Any
+
+import yaml
+
+DIRECTORY = "LeanPool/projects"
+LEGACY = "LeanPool/projects.yml"
+CARD_NAME = re.compile(r"[A-Za-z0-9_-]+\.yaml\Z")
+CARD_QUERY = """
+query($owner:String!,$name:String!,$expression:String!) {
+  repository(owner:$owner,name:$name) {
+    object(expression:$expression) {
+      ... on Tree {entries {name type mode object {
+        ... on Blob {text isTruncated isBinary}
+      }}}
+    }
+  }
+}
+"""
+
+
+def card_path(path: str) -> bool:
+    """Recognize a single card, excluding nested or arbitrary registry files."""
+    parent, _, name = path.rpartition("/")
+    return parent == DIRECTORY and CARD_NAME.fullmatch(name) is not None
+
+
+def combine(cards: dict[str, str]) -> dict[str, Any]:
+    """Validate the file container and preserve all fields for existing validators."""
+    projects = []
+    for name, text in sorted(cards.items()):
+        if not CARD_NAME.fullmatch(name):
+            raise ValueError(f"unexpected registry file: {name}")
+        data = yaml.load(text, Loader=_UniqueLoader)
+        if not isinstance(data, dict):
+            raise ValueError(f"{name}: project card must contain a mapping")
+        if data.get("slug") != name.removesuffix(".yaml"):
+            raise ValueError(f"{name}: filename must match the project slug")
+        projects.append(data)
+    if not projects:
+        raise ValueError("project registry contains no cards")
+    return {"projects": projects}
+
+
+def load_document(path: Path) -> Any:
+    """Read a registry directory or an old file, rejecting ambiguous mixed layouts."""
+    directory = path
+    if not path.is_dir() and path.name == "projects.yml":
+        directory = path.parent / "projects"
+    if directory.is_dir():
+        if directory.is_symlink():
+            raise ValueError("registry directory must not be a symbolic link")
+        if (
+            directory.name == "projects"
+            and (directory.parent / "projects.yml").exists()
+        ):
+            raise ValueError("both registry directory and legacy registry exist")
+        entries = list(directory.iterdir())
+        if any(p.is_symlink() or not p.is_file() for p in entries):
+            raise ValueError("registry must contain ordinary project card files only")
+        return combine({p.name: p.read_text() for p in entries})
+    if not path.is_file():
+        raise FileNotFoundError(path)
+    return yaml.safe_load(path.read_text()) or {}
+
+
+def read_revision(root: Path, revision: str) -> dict[str, Any]:
+    """Read cards from immutable Git objects without checking out a branch."""
+
+    def git(*arguments: str) -> str:
+        return subprocess.check_output(["git", *arguments], cwd=root, text=True)
+
+    entries = git("ls-tree", "-r", revision, "--", DIRECTORY).splitlines()
+    paths = []
+    for entry in entries:
+        metadata, name = entry.split("\t", 1)
+        if metadata.split()[:2] != ["100644", "blob"] or not card_path(name):
+            raise ValueError("unexpected registry path or file type")
+        paths.append(name)
+    if paths:
+        if (
+            subprocess.run(
+                ["git", "cat-file", "-e", f"{revision}:{LEGACY}"],
+                cwd=root,
+                capture_output=True,
+                check=False,
+            ).returncode
+            == 0
+        ):
+            raise ValueError("both registry layouts exist at revision")
+        if not all(card_path(path) for path in paths):
+            raise ValueError("unexpected registry path")
+        return combine(
+            {Path(path).name: git("show", f"{revision}:{path}") for path in paths}
+        )
+    return yaml.safe_load(git("show", f"{revision}:{LEGACY}")) or {}
+
+
+def remote_text(
+    repository: str, revision: str, fetch: Callable[[str, str, str], str | None]
+) -> str | None:
+    """Assemble remote cards for readers that compare complete YAML documents."""
+    legacy = fetch(repository, LEGACY, revision)
+    if legacy is not None:
+        return legacy
+    owner, name = repository.split("/", 1)
+    raw = subprocess.check_output(
+        [
+            "gh",
+            "api",
+            "graphql",
+            "-f",
+            f"query={CARD_QUERY}",
+            "-f",
+            f"owner={owner}",
+            "-f",
+            f"name={name}",
+            "-f",
+            f"expression={revision}:{DIRECTORY}",
+        ],
+        text=True,
+        timeout=60,
+    )
+    return yaml.safe_dump(_remote_cards(json.loads(raw)), sort_keys=False)
+
+
+def _remote_cards(response: dict) -> dict[str, Any]:
+    """Read a complete one-level registry in one request, rejecting partial blobs."""
+    repository = (response.get("data") or {}).get("repository") or {}
+    tree = repository.get("object") or {}
+    entries = tree.get("entries")
+    if response.get("errors") or not isinstance(entries, list):
+        raise ValueError("GitHub registry tree is unavailable")
+    cards = {}
+    for item in entries:
+        name = item["name"]
+        blob = item.get("object") or {}
+        if (
+            item.get("mode") != 0o100644
+            or item.get("type") != "blob"
+            or not CARD_NAME.fullmatch(name)
+            or name in cards
+            or blob.get("isTruncated") is not False
+            or blob.get("isBinary") is not False
+            or not isinstance(blob.get("text"), str)
+        ):
+            raise ValueError(f"invalid or incomplete remote project card: {name}")
+        cards[name] = blob["text"]
+    return combine(cards)
+
+
+class _UniqueLoader(yaml.SafeLoader):
+    """Reject repeated field names instead of silently losing card metadata."""
+
+    def construct_mapping(self, node: Any, deep: bool = False) -> dict:
+        result = {}
+        for key_node, value_node in node.value:
+            key = self.construct_object(key_node, deep=deep)
+            if key in result:
+                raise ValueError(f"duplicate YAML field: {key}")
+            result[key] = self.construct_object(value_node, deep=deep)
+        return result
+
+
+def main() -> None:
+    """Expose the same complete registry to shell importers and inspection tools."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--repo", type=Path, default=Path.cwd())
+    parser.add_argument("--sources", action="store_true")
+    arguments = parser.parse_args()
+    document = load_document(arguments.repo / LEGACY)
+    if arguments.sources:
+        for card in document.get("projects", []):
+            source = card.get("source", {}).get("github_repo")
+            if source:
+                print(source)
+    else:
+        print(yaml.safe_dump(document, sort_keys=False), end="")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py
index fc9a381363..0c1083ef02 100644
--- a/python/lean_pool/review.py
+++ b/python/lean_pool/review.py
@@ -81,9 +81,11 @@
 from typing import Any
 from urllib.parse import quote
 
+import yaml
 from openai import APIStatusError, BadRequestError, OpenAI, RateLimitError
 
 from lean_pool import codex_review, prior_art, review_portions
+from lean_pool.registry import load_document, remote_text
 
 logger = logging.getLogger(__name__)
 
@@ -1770,15 +1772,27 @@ def gather_prior_art(kind: str, head_sha: str, repo_full_name: str) -> str | Non
     if kind != "project":
         return None
     registry = "LeanPool/projects.yml"
-    head_text = fetch_file_at(registry, head_sha, repo_full_name)
-    base_text = (REPO_ROOT / registry).read_text(encoding="utf-8")
+    try:
+        head_text = (
+            remote_text(
+                repo_full_name,
+                head_sha,
+                lambda repo, path, ref: fetch_file_at(path, ref, repo) or None,
+            )
+            or ""
+        )
+    except (ValueError, subprocess.SubprocessError):
+        head_text = ""
+    base_text = yaml.safe_dump(load_document(REPO_ROOT / registry))
     if not head_text.strip():
         # Distinguish "could not read the registry" from "the PR adds
         # nothing": both yield zero claims, but only one of them means
         # the reviewer should treat prior art as unchecked.
         unreadable = f"{registry} could not be read at {head_sha[:8]}"
         print(f"Mathlib prior-art search skipped: {unreadable}", file=sys.stderr)
-        projects = (REPO_ROOT / "LeanPool" / "projects.yml").read_text(encoding="utf-8")
+        projects = yaml.safe_dump(
+            load_document(REPO_ROOT / "LeanPool" / "projects.yml")
+        )
         return prior_art.render([], {}, projects, unreadable)
     claims = prior_art.new_claims(head_text, base_text)
     hits, unavailable = prior_art.search_mathlib(claims)
@@ -1786,8 +1800,8 @@ def gather_prior_art(kind: str, head_sha: str, repo_full_name: str) -> str | Non
         print(f"Mathlib prior-art search skipped: {unavailable}", file=sys.stderr)
     else:
         print(f"Searched Mathlib for {len(claims)} headline(s).", file=sys.stderr)
-    projects_text = (REPO_ROOT / "LeanPool" / "projects.yml").read_text(
-        encoding="utf-8"
+    projects_text = yaml.safe_dump(
+        load_document(REPO_ROOT / "LeanPool" / "projects.yml")
     )
     return prior_art.render(claims, hits, projects_text, unavailable)
 
diff --git a/python/lean_pool/stats.py b/python/lean_pool/stats.py
index 3fb906d5e2..8ed622ff69 100644
--- a/python/lean_pool/stats.py
+++ b/python/lean_pool/stats.py
@@ -24,7 +24,7 @@
 from dataclasses import dataclass
 from pathlib import Path
 
-import yaml
+from lean_pool.registry import load_document
 
 BEGIN_MARKER = "<!-- BEGIN STATS -->"
 END_MARKER = "<!-- END STATS -->"
@@ -59,9 +59,12 @@ def count_projects(projects_yml_path: Path) -> int:
         The length of the top-level ``projects`` list, or ``0`` if the
         file is missing, malformed, or has no ``projects`` key.
     """
-    if not projects_yml_path.is_file():
+    if (
+        not projects_yml_path.is_file()
+        and not (projects_yml_path.parent / "projects").is_dir()
+    ):
         return 0
-    data = yaml.safe_load(projects_yml_path.read_text()) or {}
+    data = load_document(projects_yml_path)
     if not isinstance(data, dict):
         return 0
     projects = data.get("projects") or []
diff --git a/python/lean_pool/validation_cache.py b/python/lean_pool/validation_cache.py
index 6a36428e76..6f838557a1 100644
--- a/python/lean_pool/validation_cache.py
+++ b/python/lean_pool/validation_cache.py
@@ -28,7 +28,12 @@
     ".github/workflows/lean_action_ci.yml",
 )
 LINT_INPUTS = ("scripts/nolints.json", "scripts/ci/lint-project.lean")
-QUALITY_INPUTS = ("scripts/nolints-style.txt", "python/lean_pool/quality.py")
+QUALITY_INPUTS = (
+    "scripts/nolints-style.txt",
+    "python/lean_pool/quality.py",
+    "python/lean_pool/registry.py",
+    "python/lean_pool/indexes.py",
+)
 GLOBAL_INPUTS = SHARED_INPUTS + LINT_INPUTS + QUALITY_INPUTS
 
 
diff --git a/python/merge-queue.md b/python/merge-queue.md
new file mode 100644
index 0000000000..2b197e8236
--- /dev/null
+++ b/python/merge-queue.md
@@ -0,0 +1,44 @@
+# Merge queue and project storage
+
+The organization repository uses GitHub's native merge queue. A ready PR is
+added with the normal Merge button or `gh pr merge --auto --squash`. GitHub tests
+its proposed squash commit together with the latest main and any preceding
+queued PRs. Three proposed groups can build concurrently; up to ten passing PRs
+can merge together. A failed group does not merge. There are no bypass actors.
+
+Every group reports the normal required build, separation, documentation,
+Python, workflow, and applicable minimal-file checks. Optional heavy checks
+report a skipped result when their original trigger paths are absent. Content
+separation is checked for each constituent squash commit, so independent content
+and infrastructure PRs can coexist in a group without becoming a mixed PR.
+The Lean, warning, declaration, style and quality gates still inspect the
+combined tree. Build outputs and validation results are reused only after their
+existing source, inventory, configuration and dependency checks pass.
+
+A project adds its sources, its own complete public `Imports.lean`, and one
+`LeanPool/projects/<slug>.yaml` mapping. It never edits `LeanPool.lean`. Lake's
+`LeanPool.*` discovery builds every source, including files accidentally omitted
+from a project aggregate; the index and quality checks also reject incomplete
+aggregates. Historical tools can still read the previous monolithic registry,
+but mixed old and new layouts are rejected.
+
+Generated README statistics and NOTICE are submitted through one protected
+`codex/generated-metadata` PR. That PR is not rewritten while checks are running.
+For PRs and groups combining metadata and content, Python CI verifies each
+authored NOTICE against its own immutable PR registry before regenerating the
+combined checkout view for the ordinary generator tests. An inherited stale
+generated file therefore cannot block unrelated Python changes; an incorrect
+authored attribution edit still fails before regeneration.
+
+Deployment is deliberately staged: merge the infrastructure while the legacy
+registry remains, then migrate only the content files. Enable the repository's
+`Validated merge queue` ruleset (the checked-in JSON documents the settings),
+set `USE_MERGE_QUEUE=true`, and turn off the classic protection's strict
+up-to-date requirement while retaining its other requirements. The active
+queue replaces repeated author-branch updates with tests of the latest proposed
+merge. The old automatic rebase workflow skips when that variable is true.
+
+Measure throughput from actual `merge_group` runs after main's build cache is
+warm: record queue entry time, group start/end, merged time, failures and
+cancelled/recreated groups. A cold infrastructure migration or a toolchain bump
+is not representative of an unchanged project's steady-state queue wait.
diff --git a/python/tests/aggregator/test_render.py b/python/tests/aggregator/test_render.py
index ce0d415e0c..5975132201 100644
--- a/python/tests/aggregator/test_render.py
+++ b/python/tests/aggregator/test_render.py
@@ -582,6 +582,30 @@ def test_load_pool_repos_missing_file_returns_empty(tmp_path: Path) -> None:
     assert load_pool_repos(tmp_path / "absent.yml") == set()
 
 
+def test_load_pool_repos_honors_custom_files_next_to_cards(tmp_path: Path) -> None:
+    """Existing and missing explicit files retain their own pool membership."""
+    directory = tmp_path / "projects"
+    directory.mkdir()
+    (directory / "other.yaml").write_text(
+        "slug: other\nsource:\n  github_repo: owner/other\n"
+    )
+    path = tmp_path / "alternate.yml"
+    path.write_text(
+        "projects:\n  - slug: selected\n    source:\n"
+        "      github_repo: owner/selected\n"
+    )
+    assert load_pool_repos(path) == {"owner/selected"}
+    assert load_pool_repos(tmp_path / "missing.yml") == set()
+
+
+def test_load_pool_repos_accepts_a_custom_card_directory(tmp_path: Path) -> None:
+    """An explicit archive directory keeps the merged-project markers intact."""
+    path = tmp_path / "archived-cards"
+    path.mkdir()
+    (path / "alpha.yaml").write_text("slug: alpha\nsource:\n  github_repo: Acme/Demo\n")
+    assert load_pool_repos(path) == {"acme/demo"}
+
+
 def test_load_pool_repos_invalid_yaml_returns_empty(tmp_path: Path) -> None:
     """A malformed file logs and returns empty rather than crashing render."""
     path = tmp_path / "projects.yml"
diff --git a/python/tests/test_ci_artifacts.py b/python/tests/test_ci_artifacts.py
index 8b5e77029e..0eccce24d7 100644
--- a/python/tests/test_ci_artifacts.py
+++ b/python/tests/test_ci_artifacts.py
@@ -7,6 +7,7 @@
 import os
 import stat
 import subprocess
+import sys
 import tarfile
 import zipfile
 from pathlib import Path
@@ -16,6 +17,77 @@
 from lean_pool import ci_artifacts
 
 
+def test_wait_command_only_waits_for_exact_head_build(monkeypatch) -> None:
+    """The prerequisite polls the producer without installing or compiling output."""
+    calls = []
+    monkeypatch.setattr(
+        sys,
+        "argv",
+        [
+            "ci_artifacts",
+            "wait",
+            "--repository",
+            "owner/repo",
+            "--head",
+            "abc123",
+            "--event",
+            "pull_request",
+            "--wait-seconds",
+            "18000",
+        ],
+    )
+
+    def matching(repository, head, event):
+        calls.append((repository, head, event))
+        return {"id": 7}
+
+    def waiting(repository, run, seconds):
+        calls.append((repository, run, seconds))
+        return 9
+
+    def unexpected(*args, **kwargs):
+        pytest.fail("Build waiting must not restore or compile output")
+
+    monkeypatch.setattr(ci_artifacts, "matching_run", matching)
+    monkeypatch.setattr(ci_artifacts, "wait_for_artifact", waiting)
+    monkeypatch.setattr(ci_artifacts, "reuse_build", unexpected)
+    monkeypatch.setattr(ci_artifacts, "download_build", unexpected)
+    ci_artifacts.main()
+    assert calls[0] == ("owner/repo", "abc123", "pull_request")
+    assert calls[1][:2] == ("owner/repo", {"id": 7})
+    assert 17999 <= calls[1][2] <= 18000
+
+
+def test_build_wait_handles_late_producer_with_one_deadline(monkeypatch) -> None:
+    """Starting before Lean CI appears must not trigger another cold pool build."""
+    clock = [0]
+    runs = iter([None, {"id": 7}])
+    monkeypatch.setattr(ci_artifacts.time, "monotonic", lambda: clock[0])
+    monkeypatch.setattr(
+        ci_artifacts.time,
+        "sleep",
+        lambda seconds: clock.__setitem__(0, clock[0] + seconds),
+    )
+    monkeypatch.setattr(ci_artifacts, "matching_run", lambda *args: next(runs))
+    calls = []
+
+    def waiting(repository, run, seconds):
+        calls.append((repository, run, seconds))
+        return 9
+
+    monkeypatch.setattr(ci_artifacts, "wait_for_artifact", waiting)
+    assert ci_artifacts.wait_for_build("owner/repo", "abc123", "pull_request", 100) == 9
+    assert calls == [("owner/repo", {"id": 7}, 80)]
+
+
+def test_build_wait_stops_when_producer_never_appears(monkeypatch) -> None:
+    """Unavailable output retains bounded waiting and the regular build fallback."""
+    monkeypatch.setattr(ci_artifacts, "matching_run", lambda *args: None)
+    assert (
+        ci_artifacts.wait_for_build("owner/repo", "abc123", "pull_request", 0) is None
+    )
+
+
 @pytest.fixture
 def repository(tmp_path: Path) -> Path:
     """Create a committed source tree with an ignored synthetic Lake build."""
@@ -362,3 +434,36 @@ def download(command, *, stdout, **kwargs):
         ci_artifacts.download_build(repository, "owner/repo", 7)
     assert output.read_bytes() == b"old"
     assert not list((repository / ".lake").glob("lean-ci-*"))
+
+
+def test_opted_in_minimal_verifier_reuses_exact_pr_build(repository, monkeypatch):
+    """The rare full-pool PR consumer can reuse its matching producer output."""
+    archive = repository / "build.tar.gz"
+    ci_artifacts.pack_build(repository, archive)
+    output = repository / ".lake/build/lib/lean/LeanPool.olean"
+    output.unlink()
+    calls = []
+
+    def matching(repository_name, head, event):
+        calls.append((repository_name, head, event))
+        return {"id": 7, "html_url": "https://github.com/owner/repo/actions/runs/7"}
+
+    monkeypatch.setattr(ci_artifacts, "matching_run", matching)
+    monkeypatch.setattr(ci_artifacts, "wait_for_artifact", lambda *args: 9)
+    monkeypatch.setattr(
+        ci_artifacts,
+        "download_build",
+        lambda root, repository_name, artifact: ci_artifacts.restore_build(
+            root, archive
+        ),
+    )
+    assert ci_artifacts.reuse_build(
+        repository,
+        "owner/repo",
+        "head",
+        "pull_request",
+        0,
+        pull_request_artifact=True,
+    )
+    assert calls == [("owner/repo", "head", "pull_request")]
+    assert output.exists()
diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py
index 68ff4f9926..da19e1114b 100644
--- a/python/tests/test_ci_cache_contract.py
+++ b/python/tests/test_ci_cache_contract.py
@@ -2,6 +2,8 @@
 
 from __future__ import annotations
 
+import os
+import subprocess
 from pathlib import Path
 
 import yaml
@@ -114,3 +116,198 @@ def test_single_and_sharded_builds_use_validation_cache() -> None:
         assert "validation_cache lint" in steps[names.index("Lint")]["run"]
         assert "lint-style LeanPool" in steps[names.index("Text style lint")]["run"]
     assert contracts[0] == contracts[1]
+
+
+def test_merge_queue_reports_all_required_gates_without_path_filtered_workflows() -> (
+    None
+):
+    """A filtered-out workflow must never leave the protected queue waiting forever."""
+    import json
+
+    rules = json.loads((WORKFLOWS.parent / "merge-queue-ruleset.json").read_text())[
+        "rules"
+    ]
+    required = {
+        check["context"]
+        for rule in rules
+        if rule["type"] == "required_status_checks"
+        for check in rule["parameters"]["required_status_checks"]
+    }
+    names = set()
+    for filename in (
+        "lean_action_ci.yml",
+        "content-pr-guard.yml",
+        "docs.yml",
+        "python_ci.yml",
+        "workflow_lint.yml",
+        "exposition-verify.yml",
+    ):
+        workflow = yaml.safe_load((WORKFLOWS / filename).read_text())
+        events = workflow.get("on", workflow.get(True))
+        assert "merge_group" in events
+        if filename != "content-pr-guard.yml":
+            assert "paths" not in events["pull_request"]
+        names.update(job.get("name", key) for key, job in workflow["jobs"].items())
+    assert required <= names
+    queue = next(rule["parameters"] for rule in rules if rule["type"] == "merge_queue")
+    assert queue["grouping_strategy"] == "ALLGREEN"
+    assert queue["merge_method"] == "SQUASH"
+
+
+def test_yaml_aware_recovery_has_a_declared_runtime_in_every_job() -> None:
+    """Early planning and restore steps cannot depend on runner-global PyYAML."""
+    modules = ("rebase_fastpath", "ci_pr_build", "queue_build")
+    for filename in ("lean_action_ci.yml", "docs.yml", "exposition-verify.yml"):
+        workflow = yaml.safe_load((WORKFLOWS / filename).read_text())
+        for job in workflow["jobs"].values():
+            runtime_available = False
+            for step in job["steps"]:
+                if str(step.get("uses", "")).startswith("astral-sh/setup-uv@"):
+                    runtime_available = True
+                command = step.get("run", "")
+                if any(f"-m lean_pool.{module}" in command for module in modules):
+                    assert runtime_available, (filename, step)
+                    assert "uv run --project python --locked python -m" in command
+                    assert not any(
+                        f"python3 -m lean_pool.{module}" in command
+                        for module in modules
+                    )
+
+
+def test_required_scoped_checks_fail_closed_when_classification_fails() -> None:
+    """A broken classifier cannot turn a required validation into a passing skip."""
+    for filename, names in (
+        ("python_ci.yml", ("lint", "test")),
+        ("exposition-verify.yml", ("verify",)),
+    ):
+        workflow = yaml.safe_load((WORKFLOWS / filename).read_text())
+        for name in names:
+            job = workflow["jobs"][name]
+            assert job["if"] == (
+                "always() && (needs.scope.result != 'success' || "
+                "needs.scope.outputs.applicable != 'false')"
+            )
+            guard = job["steps"][0]
+            assert (
+                guard["env"].items()
+                >= {
+                    "SCOPE_RESULT": "${{ needs.scope.result }}",
+                    "APPLICABLE": "${{ needs.scope.outputs.applicable }}",
+                }.items()
+            )
+            for result, applicable, accepted in (
+                ("success", "true", True),
+                ("failure", "true", False),
+                ("failure", "", False),
+                ("cancelled", "false", False),
+                ("success", "", False),
+            ):
+                process = subprocess.run(
+                    ["bash", "-e", "-c", guard["run"]],
+                    env={
+                        **os.environ,
+                        "SCOPE_RESULT": result,
+                        "APPLICABLE": applicable,
+                        "BUILD_READY_RESULT": "success",
+                        "EVENT": "pull_request",
+                    },
+                    capture_output=True,
+                )
+                assert (process.returncode == 0) == accepted
+
+
+def test_minimal_verifier_pr_has_an_explicit_full_build_producer(tmp_path):
+    """Cold minimal verification shares compilation while retaining its real gate."""
+    lean = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"]
+    minimal = yaml.safe_load((WORKFLOWS / "exposition-verify.yml").read_text())["jobs"]
+    assert "minimal_build" in lean["plan"]["outputs"]
+    planning = next(step for step in lean["plan"]["steps"] if step.get("id") == "plan")
+    classifier = minimal["scope"]["steps"][-1]["run"]
+    # Producer scope must include precisely the consumer's heavy trigger paths.
+    pattern = classifier.split("grep -Eq '")[1].split("'")[0]
+    assert pattern in planning["run"]
+    classification = (
+        "minimal_build=false"
+        + planning["run"].split("minimal_build=false", 1)[1].split("cold=false", 1)[0]
+    )
+    changed = tmp_path / "changed-files.txt"
+    output = tmp_path / "output.txt"
+    for path, event, expected in (
+        ("python/lean_pool/ci_artifacts.py", "pull_request", "true"),
+        ("python/lean_pool/exposition/verify.py", "pull_request", "true"),
+        ("scripts/exposition/extract-all.sh", "pull_request", "true"),
+        (".github/workflows/exposition-verify.yml", "pull_request", "true"),
+        ("LeanPool/projects/example.yaml", "pull_request", "false"),
+        ("python/lean_pool/registry.py", "pull_request", "false"),
+        ("python/lean_pool/exposition/verify.py", "merge_group", "false"),
+    ):
+        changed.write_text(path + "\n")
+        output.write_text("")
+        subprocess.run(
+            ["bash", "-e", "-c", classification],
+            env={
+                **os.environ,
+                "changed_files": str(changed),
+                "GITHUB_OUTPUT": str(output),
+                "EVENT_NAME": event,
+            },
+            check=True,
+        )
+        assert output.read_text().strip() == f"minimal_build={expected}"
+    for name in ("build", "finalize"):
+        steps = {step.get("name"): step for step in lean[name]["steps"]}
+        for producer in (
+            "Package build for documentation",
+            "Share build with documentation",
+        ):
+            assert "needs.plan.outputs.minimal_build == 'true'" in steps[producer]["if"]
+            assert "github.event_name == 'pull_request'" in steps[producer]["if"]
+    steps = {step.get("name"): step for step in minimal["verify"]["steps"]}
+    reuse = steps["Reuse matching Lean CI build"]
+    assert "github.event_name != 'pull_request'" not in reuse["if"]
+    assert "--pull-request-artifact" in reuse["run"]
+    assert "--wait-seconds 0" in reuse["run"]
+    assert steps["Build pool"]["run"] == "~/.elan/bin/lake build LeanPool"
+    assert "--baseline 214" in steps["Verify minimal files"]["run"]
+
+
+def test_minimal_build_wait_does_not_consume_verification_window() -> None:
+    """A cold producer cannot use the verifier's six-hour execution allowance."""
+    jobs = yaml.safe_load((WORKFLOWS / "exposition-verify.yml").read_text())["jobs"]
+    assert jobs["verify"]["needs"] == ["scope", "build-ready"]
+    waiting = jobs["build-ready"]
+    assert waiting["needs"] == "scope"
+    assert "needs.scope.outputs.applicable == 'true'" in waiting["if"]
+    assert "github.event_name == 'pull_request'" in waiting["if"]
+    commands = [step.get("run", "") for step in waiting["steps"]]
+    assert any("lean_pool.ci_artifacts wait" in command for command in commands)
+    assert any("--wait-seconds 18000" in command for command in commands)
+    assert not any(
+        "lake build" in command or "extract-all" in command for command in commands
+    )
+    guard = jobs["verify"]["steps"][0]
+    for event, result, accepted in (
+        ("pull_request", "success", True),
+        ("pull_request", "failure", False),
+        ("pull_request", "cancelled", False),
+        ("pull_request", "skipped", False),
+        ("pull_request", "", False),
+        ("merge_group", "skipped", True),
+        ("merge_group", "failure", False),
+        ("schedule", "skipped", True),
+        ("schedule", "failure", False),
+        ("workflow_dispatch", "skipped", True),
+        ("workflow_dispatch", "failure", False),
+    ):
+        process = subprocess.run(
+            ["bash", "-e", "-c", guard["run"]],
+            env={
+                **os.environ,
+                "SCOPE_RESULT": "success",
+                "APPLICABLE": "true",
+                "BUILD_READY_RESULT": result,
+                "EVENT": event,
+            },
+            capture_output=True,
+        )
+        assert (process.returncode == 0) == accepted
diff --git a/python/tests/test_ci_validation_artifacts.py b/python/tests/test_ci_validation_artifacts.py
index 72f8f8cebe..d50c92e705 100644
--- a/python/tests/test_ci_validation_artifacts.py
+++ b/python/tests/test_ci_validation_artifacts.py
@@ -116,6 +116,8 @@ def test_only_associated_merged_main_pull_is_promoted(monkeypatch):
     }
 
     def response(endpoint):
+        if "event=merge_group" in endpoint:
+            return {"workflow_runs": []}
         if endpoint.endswith("/commits/merge/pulls"):
             return [
                 valid | {"merged_at": None},
diff --git a/python/tests/test_indexes.py b/python/tests/test_indexes.py
index 8ad1f654bf..af6a7ccf81 100644
--- a/python/tests/test_indexes.py
+++ b/python/tests/test_indexes.py
@@ -190,3 +190,47 @@ def test_default_generation_only_writes_pool_indexes(tmp_path: Path) -> None:
     assert (tmp_path / "LeanPool.lean").exists()
     assert not (tmp_path / "Challenge.lean").exists()
     assert not (tmp_path / "Solution.lean").exists()
+
+
+def test_lake_directory_build_cannot_omit_unlisted_source(tmp_path: Path) -> None:
+    """A fixed root still builds new modules and rejects an unlisted broken proof."""
+    import os
+    import subprocess
+
+    pin = (Path(__file__).resolve().parents[2] / "lean-toolchain").read_text().strip()
+    lake = (
+        Path.home()
+        / ".elan/toolchains"
+        / pin.replace("/", "--").replace(":", "---")
+        / "bin/lake"
+    )
+    if not lake.is_file():
+        if os.environ.get("LEAN_POOL_REQUIRE_TEST_TOOLCHAIN") == "1":
+            pytest.fail("required pinned Lean toolchain unavailable")
+        pytest.skip("pinned Lean toolchain unavailable")
+    _sources(tmp_path)
+    (tmp_path / "lean-toolchain").write_text(pin + "\n")
+    (tmp_path / "lakefile.toml").write_text(
+        'name = "test"\ndefaultTargets = ["LeanPool"]\nrequiresModuleSystem = true\n'
+        '[[lean_lib]]\nname = "LeanPool"\nglobs = ["LeanPool.*"]\n'
+    )
+    _generate(tmp_path)
+    original = (tmp_path / "LeanPool.lean").read_text()
+    result = subprocess.run(
+        [str(lake), "build"], cwd=tmp_path, capture_output=True, text=True
+    )
+    assert result.returncode == 0, result.stdout + result.stderr
+    assert (tmp_path / ".lake/build/lib/lean/LeanPool/Beta/Nested/Other.olean").exists()
+    (tmp_path / "LeanPool/Independent.lean").write_text(
+        "module\ntheorem broken : False := by trivial\n"
+    )
+    # Do not regenerate any index: Lake must still discover this new broken module.
+    result = subprocess.run(
+        [str(lake), "build"], cwd=tmp_path, capture_output=True, text=True
+    )
+    assert result.returncode != 0
+    assert "LeanPool.Independent" in result.stdout + result.stderr
+    _generate(tmp_path)
+    assert (tmp_path / "LeanPool.lean").read_text() == original
+    assert indexes.structure_errors(tmp_path) == []
+    assert _check_project_indexes(tmp_path) == []
diff --git a/python/tests/test_queue_build.py b/python/tests/test_queue_build.py
new file mode 100644
index 0000000000..5f3d6e04eb
--- /dev/null
+++ b/python/tests/test_queue_build.py
@@ -0,0 +1,112 @@
+"""Queue reuse never replaces checks or overwrites unrelated project passes."""
+
+import json
+
+import pytest
+
+from lean_pool import ci_validation_artifacts, queue_build
+
+
+def test_only_owned_project_receipts_are_promoted(tmp_path):
+    """One PR's old base cannot overwrite another queued project's newer pass."""
+    path = tmp_path / ".lake/validation-cache/v1/passes.json"
+    path.parent.mkdir(parents=True)
+    path.write_text(
+        json.dumps(
+            {
+                "version": 1,
+                "receipts": {"lint:LeanPool.B": "new-B", "quality:LeanPool.A": "old-A"},
+            }
+        )
+    )
+    queue_build.merge_owned_receipts(
+        tmp_path,
+        {
+            "lint:LeanPool.B": "stale-B",
+            "quality:LeanPool.A": "new-A",
+            "lint:LeanPool.ABC": "unrelated",
+            "lint:LeanPool.A.Part": "new-part",
+        },
+        ["A"],
+    )
+    assert json.loads(path.read_text())["receipts"] == {
+        "lint:LeanPool.B": "new-B",
+        "quality:LeanPool.A": "new-A",
+        "lint:LeanPool.A.Part": "new-part",
+    }
+
+
+@pytest.mark.parametrize(
+    "same_sources,green_run,expected",
+    [(False, 9, []), (True, None, []), (True, 9, [9])],
+)
+def test_reuse_requires_current_sources_and_a_green_pr_head(
+    tmp_path, monkeypatch, same_sources, green_run, expected
+):
+    """A changed proof or failed prior CI falls back to the complete ordinary build."""
+    monkeypatch.setattr(
+        queue_build.rebase_fastpath, "git", lambda *args: "Project (#123)\n"
+    )
+    pull = {
+        "head": {"sha": "a" * 40},
+        "base": {"repo": {"full_name": "owner/repo"}, "ref": "main", "sha": "b" * 40},
+    }
+    monkeypatch.setattr(queue_build.rebase_fastpath, "github_json", lambda _: pull)
+    monkeypatch.setattr(queue_build.rebase_fastpath, "_exists_at", lambda *args: True)
+    monkeypatch.setattr(
+        queue_build.ci_pr_build, "sources_match", lambda *args: same_sources
+    )
+    calls = []
+
+    def successful(repository, number, head):
+        calls.append((repository, number, head))
+        return green_run
+
+    monkeypatch.setattr(
+        queue_build.ci_validation_artifacts, "successful_pr_run", successful
+    )
+    assert [
+        entry["run"]
+        for entry in queue_build.candidate_runs(tmp_path, "owner/repo", "base", "head")
+    ] == expected
+    assert calls == [("owner/repo", 123, "a" * 40)]
+
+
+def test_latest_queue_attempt_must_succeed(monkeypatch):
+    """An older success cannot hide a newer failed check on the same queue head."""
+
+    def github(endpoint):
+        if "event=merge_group" in endpoint:
+            return {
+                "workflow_runs": [
+                    {"id": 1, "head_sha": "head", "conclusion": "success"},
+                    {"id": 2, "head_sha": "head", "conclusion": "failure"},
+                ]
+            }
+        if "/commits/" in endpoint:
+            return []
+        raise AssertionError(endpoint)
+
+    monkeypatch.setattr(ci_validation_artifacts, "github_json", github)
+    assert ci_validation_artifacts.source_runs("owner/repo", "push", "head", True) == []
+
+
+@pytest.mark.parametrize("run,expected", [(None, False), (17, True)])
+def test_main_uses_only_a_successful_exact_queue_head(
+    tmp_path, monkeypatch, run, expected
+):
+    """A combined archive warms main once; absent evidence keeps normal recovery."""
+    calls = []
+    monkeypatch.setattr(
+        ci_validation_artifacts, "successful_queue_run", lambda repository, head: run
+    )
+    monkeypatch.setattr(
+        queue_build.rebase_fastpath, "restore", lambda *args: calls.append(args)
+    )
+    assert (
+        queue_build.restore_merged_group(tmp_path, "owner/repo", "validated-head")
+        is expected
+    )
+    assert calls == (
+        [(tmp_path, "owner/repo", 17, "validated-head")] if expected else []
+    )
diff --git a/python/tests/test_queue_guard.py b/python/tests/test_queue_guard.py
new file mode 100644
index 0000000000..66302780f1
--- /dev/null
+++ b/python/tests/test_queue_guard.py
@@ -0,0 +1,61 @@
+"""Verify a queue batch preserves each constituent PR's separation gate."""
+
+import subprocess
+from pathlib import Path
+
+import pytest
+
+from lean_pool.queue_guard import group_changes, separation_errors
+
+
+def test_separate_content_and_infrastructure_prs_can_share_batch(
+    tmp_path: Path,
+) -> None:
+    """Two individually valid PRs stay valid when tested against each other."""
+
+    def git(*args: str) -> str:
+        return subprocess.check_output(["git", *args], cwd=tmp_path, text=True).strip()
+
+    git("init")
+    git("config", "user.email", "test@example.org")
+    git("config", "user.name", "Test")
+    (tmp_path / "README.md").write_text("base")
+    git("add", ".")
+    git("commit", "-m", "base")
+    base = git("rev-parse", "HEAD")
+    (tmp_path / "LeanPool/projects").mkdir(parents=True)
+    (tmp_path / "LeanPool/projects/a.yaml").write_text("slug: a")
+    git("add", ".")
+    git("commit", "-m", "content PR")
+    (tmp_path / "README.md").write_text("documentation")
+    git("add", ".")
+    git("commit", "-m", "infrastructure PR")
+    changes = group_changes(tmp_path, base, "HEAD")
+    assert len(changes) == 2
+    assert all(not separation_errors(paths) for paths in changes)
+    assert separation_errors([path for paths in changes for path in paths])
+
+
+@pytest.mark.parametrize(
+    "paths",
+    [
+        ["LeanPool/A.lean", "python/lean_pool/quality.py"],
+        ["LeanPool.lean"],
+        ["LeanPool/A.lean", "LeanPool/projects/nested/a.yaml"],
+    ],
+)
+def test_invalid_single_pr_cannot_hide_in_batch(paths: list[str]) -> None:
+    """Queue grouping creates no exemption for mixed changes or the shared root."""
+    assert separation_errors(paths)
+
+
+def test_version_bump_exception_is_preserved() -> None:
+    """A proof update alongside pinned version metadata keeps its existing policy."""
+    assert not separation_errors(["LeanPool/A.lean", "lean-toolchain"])
+
+
+def test_lossless_layout_migration_retains_separation() -> None:
+    """The legacy base permits its existing content paths but no mixed tooling."""
+    files = ["LeanPool.lean", "LeanPool/projects.yml", "LeanPool/projects/a.yaml"]
+    assert not separation_errors(files, legacy=True)
+    assert separation_errors(files + ["python/lean_pool/quality.py"], legacy=True)
diff --git a/python/tests/test_queue_notice.py b/python/tests/test_queue_notice.py
new file mode 100644
index 0000000000..cc881aa435
--- /dev/null
+++ b/python/tests/test_queue_notice.py
@@ -0,0 +1,194 @@
+"""Queued content and generated attribution retain separate source checks."""
+
+import subprocess
+
+import pytest
+import yaml
+
+from lean_pool import notice, queue_notice
+
+
+def test_bad_submitted_attribution_is_rejected(tmp_path):
+    """Regeneration cannot conceal an incorrect NOTICE submitted by a PR."""
+    (tmp_path / "LeanPool").mkdir()
+    (tmp_path / "LeanPool/projects.yml").write_text(
+        yaml.safe_dump({"projects": [_card("a")]})
+    )
+    (tmp_path / "NOTICE.extra.yml").write_text("{}\n")
+    _git(tmp_path, "init")
+    _git(tmp_path, "config", "user.name", "Test")
+    _git(tmp_path, "config", "user.email", "test@example.org")
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "base")
+    with pytest.raises(ValueError, match="does not match"):
+        queue_notice.validate_snapshot(tmp_path, "HEAD", "Missing attribution\n")
+
+
+def _card(name):
+    return {
+        "slug": name,
+        "entry_module": f"LeanPool.{name.upper()}",
+        "license": "MIT",
+        "source": {"github_repo": f"example/{name}"},
+    }
+
+
+def _git(root, *arguments):
+    return subprocess.check_output(["git", *arguments], cwd=root, text=True).strip()
+
+
+def test_combined_queue_checks_submitted_snapshot_then_all_new_projects(
+    tmp_path, monkeypatch
+):
+    """A correct metadata PR remains valid when independent content precedes it."""
+    (tmp_path / "LeanPool").mkdir()
+    registry = tmp_path / "LeanPool/projects.yml"
+    registry.write_text(yaml.safe_dump({"projects": [_card("a")]}))
+    extra = tmp_path / "NOTICE.extra.yml"
+    extra.write_text("{}\n")
+    path = tmp_path / "NOTICE"
+    path.write_text(notice.build(tmp_path))
+    _git(tmp_path, "init")
+    _git(tmp_path, "config", "user.name", "Test")
+    _git(tmp_path, "config", "user.email", "test@example.org")
+    _git(tmp_path, "remote", "add", "origin", str(tmp_path))
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "base")
+    base = _git(tmp_path, "rev-parse", "HEAD")
+    extra.write_text("A:\n  note: Additional upstream attribution\n")
+    path.write_text(notice.build(tmp_path))
+    submitted = path.read_text()
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "Refresh attribution")
+    submitted_head = _git(tmp_path, "rev-parse", "HEAD")
+    _git(tmp_path, "checkout", "-b", "queue", base)
+    registry.write_text(yaml.safe_dump({"projects": [_card("a"), _card("b")]}))
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "Add project (#2)")
+    extra.write_text("A:\n  note: Additional upstream attribution\n")
+    path.write_text(submitted)
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "Refresh attribution (#1)")
+    head = _git(tmp_path, "rev-parse", "HEAD")
+    monkeypatch.setattr(
+        queue_notice,
+        "github_json",
+        lambda _: {
+            "head": {"sha": submitted_head},
+            "base": {"repo": {"full_name": "owner/repo"}, "ref": "main"},
+        },
+    )
+    queue_notice.prepare(tmp_path, "owner/repo", base, head)
+    assert path.read_text() == notice.build(tmp_path)
+    assert "https://github.com/example/b" in path.read_text()
+    assert "Additional upstream attribution" in path.read_text()
+
+
+@pytest.mark.parametrize("authored", ["inherited", "valid", "invalid"])
+@pytest.mark.parametrize("event", ["pull_request", "main_push"])
+def test_ordinary_pr_preparation_preserves_the_attribution_gate(
+    tmp_path, authored, event, monkeypatch
+):
+    """An inherited stale NOTICE does not block Python, but a bad edit still fails."""
+    (tmp_path / "LeanPool").mkdir()
+    registry = tmp_path / "LeanPool/projects.yml"
+    registry.write_text(yaml.safe_dump({"projects": [_card("a")]}))
+    extra = tmp_path / "NOTICE.extra.yml"
+    extra.write_text("{}\n")
+    path = tmp_path / "NOTICE"
+    path.write_text(notice.build(tmp_path))
+    _git(tmp_path, "init")
+    _git(tmp_path, "config", "user.name", "Test")
+    _git(tmp_path, "config", "user.email", "test@example.org")
+    _git(tmp_path, "remote", "add", "origin", str(tmp_path))
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "base")
+    base = _git(tmp_path, "rev-parse", "HEAD")
+    (tmp_path / "tool.py").write_text("print('update')\n")
+    if authored == "valid":
+        extra.write_text("A:\n  note: Additional upstream attribution\n")
+        path.write_text(notice.build(tmp_path))
+    elif authored == "invalid":
+        path.write_text("Missing attribution\n")
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "Python or metadata PR")
+    submitted = _git(tmp_path, "rev-parse", "HEAD")
+    _git(tmp_path, "checkout", "-b", "main-view", base)
+    registry.write_text(yaml.safe_dump({"projects": [_card("a"), _card("b")]}))
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "Accept independent project")
+    current_main = _git(tmp_path, "rev-parse", "HEAD")
+    _git(tmp_path, "merge", "--no-edit", submitted)
+    before = path.read_text()
+    assert before != notice.build(tmp_path)
+    monkeypatch.setattr(
+        queue_notice,
+        "github_json",
+        lambda _: [
+            {
+                "merged_at": "now",
+                "merge_commit_sha": _git(tmp_path, "rev-parse", "HEAD"),
+                "head": {"sha": submitted},
+                "base": {"ref": "main", "repo": {"full_name": "owner/repo"}},
+            }
+        ],
+    )
+
+    def prepare():
+        if event == "pull_request":
+            queue_notice.prepare_pull_request(tmp_path, current_main, submitted)
+        else:
+            queue_notice.prepare_main_push(
+                tmp_path,
+                "owner/repo",
+                current_main,
+                _git(tmp_path, "rev-parse", "HEAD"),
+            )
+
+    if authored == "invalid":
+        with pytest.raises(ValueError, match="does not match"):
+            prepare()
+        assert path.read_text() == before
+    else:
+        prepare()
+        assert path.read_text() == notice.build(tmp_path)
+        assert "https://github.com/example/b" in path.read_text()
+        assert _git(tmp_path, "show", "HEAD:NOTICE") + "\n" == before
+
+
+@pytest.mark.parametrize("valid", [True, False])
+def test_main_push_checks_ordinary_commit_without_pr_title(
+    tmp_path, monkeypatch, valid
+):
+    """A direct main commit needs no PR lookup, but must preserve attribution."""
+    (tmp_path / "LeanPool").mkdir()
+    registry = tmp_path / "LeanPool/projects.yml"
+    registry.write_text(yaml.safe_dump({"projects": [_card("a")]}))
+    (tmp_path / "NOTICE.extra.yml").write_text("{}\n")
+    path = tmp_path / "NOTICE"
+    path.write_text(notice.build(tmp_path))
+    _git(tmp_path, "init")
+    _git(tmp_path, "config", "user.name", "Test")
+    _git(tmp_path, "config", "user.email", "test@example.org")
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "base")
+    base = _git(tmp_path, "rev-parse", "HEAD")
+    registry.write_text(yaml.safe_dump({"projects": [_card("a"), _card("b")]}))
+    path.write_text(notice.build(tmp_path) if valid else "Missing attribution\n")
+    _git(tmp_path, "add", ".")
+    _git(tmp_path, "commit", "-m", "Add project and attribution")
+    calls = []
+
+    def associated_pulls(endpoint):
+        calls.append(endpoint)
+        return []
+
+    monkeypatch.setattr(queue_notice, "github_json", associated_pulls)
+    if valid:
+        queue_notice.prepare_main_push(tmp_path, "owner/repo", base, "HEAD")
+        assert not calls
+        assert path.read_text() == notice.build(tmp_path)
+    else:
+        with pytest.raises(ValueError, match="does not match"):
+            queue_notice.prepare_main_push(tmp_path, "owner/repo", base, "HEAD")
+        assert path.read_text() == "Missing attribution\n"
diff --git a/python/tests/test_rebase.py b/python/tests/test_rebase.py
index 074765a92e..d1d76c7563 100644
--- a/python/tests/test_rebase.py
+++ b/python/tests/test_rebase.py
@@ -14,6 +14,7 @@
     resolvable,
     split_cards,
 )
+from lean_pool.registry import load_document
 
 BASE = """projects:
   - slug: alpha
@@ -225,7 +226,10 @@ def test_split_cards_rejects_ambiguous_registries(text: str) -> None:
 def test_split_cards_covers_every_real_project() -> None:
     """Every YAML project, including title-first entries, gets a verbatim block."""
     root = Path(__file__).resolve().parents[2]
-    text = (root / "LeanPool/projects.yml").read_text(encoding="utf-8")
+    text = yaml.safe_dump(
+        load_document(root / "LeanPool/projects.yml"), sort_keys=False, indent=2
+    )
+    text = "projects:\n" + "".join("  " + line + "\n" for line in text.splitlines()[1:])
     header, cards = split_cards(text)
     assert [slug for slug, _ in cards] == [
         card["slug"] for card in yaml.safe_load(text)["projects"]
diff --git a/python/tests/test_registry.py b/python/tests/test_registry.py
new file mode 100644
index 0000000000..ea24de929b
--- /dev/null
+++ b/python/tests/test_registry.py
@@ -0,0 +1,200 @@
+"""Exercise independent project cards, historical reads, and rejected corruption."""
+
+import json
+import subprocess
+from pathlib import Path
+
+import pytest
+import yaml
+
+from lean_pool import registry
+from lean_pool.registry import combine, load_document, read_revision
+
+
+def test_directory_and_legacy_have_identical_cards(tmp_path: Path) -> None:
+    """Migration changes storage only, preserving unknown and nested metadata."""
+    path = tmp_path / "projects.yml"
+    cards = [{"slug": "b", "source": {"url": "https://example.org"}}, {"slug": "a"}]
+    path.write_text(yaml.safe_dump({"projects": cards}))
+    before = load_document(path)
+    path.unlink()
+    directory = tmp_path / "projects"
+    directory.mkdir()
+    for card in cards:
+        (directory / f"{card['slug']}.yaml").write_text(yaml.safe_dump(card))
+    assert load_document(path) == {
+        "projects": sorted(before["projects"], key=lambda c: c["slug"])
+    }
+    assert load_document(directory) == load_document(path)
+
+
+def test_explicit_historical_file_ignores_sibling_cards(tmp_path: Path) -> None:
+    """Selecting a different registry must not silently select canonical cards."""
+    directory = tmp_path / "projects"
+    directory.mkdir()
+    (directory / "other.yaml").write_text("slug: other\n")
+    path = tmp_path / "alternate.yml"
+    path.write_text("projects:\n  - slug: selected\n")
+    assert load_document(path) == {"projects": [{"slug": "selected"}]}
+    with pytest.raises(FileNotFoundError):
+        load_document(tmp_path / "missing.yml")
+
+
+def test_explicit_custom_directory_ignores_unrelated_legacy_file(
+    tmp_path: Path,
+) -> None:
+    """Only the canonical cards and legacy file constitute a mixed layout."""
+    directory = tmp_path / "archived-cards"
+    directory.mkdir()
+    (directory / "selected.yaml").write_text("slug: selected\n")
+    (tmp_path / "projects.yml").write_text("projects:\n  - slug: other\n")
+    assert load_document(directory) == {"projects": [{"slug": "selected"}]}
+
+
+@pytest.mark.parametrize(
+    "cards",
+    [
+        {},
+        {"a.yaml": "[]"},
+        {"a.yaml": "slug: b"},
+        {"a.yaml": "slug: a\nslug: a\n"},
+        {"a.yml": "slug: a"},
+        {"../a.yaml": "slug: a"},
+    ],
+)
+def test_invalid_cards_fail_closed(cards: dict[str, str]) -> None:
+    """Empty registries and malformed identities cannot silently hide projects."""
+    with pytest.raises(ValueError):
+        combine(cards)
+
+
+def test_mixed_layout_and_nested_directory_rejected(tmp_path: Path) -> None:
+    """Ambiguous migrations and ignored nested cards must fail validation."""
+    directory = tmp_path / "projects"
+    directory.mkdir()
+    (directory / "a.yaml").write_text("slug: a\n")
+    legacy = tmp_path / "projects.yml"
+    legacy.write_text("projects: []")
+    with pytest.raises(ValueError, match="both"):
+        load_document(directory)
+    legacy.unlink()
+    (directory / "nested").mkdir()
+    with pytest.raises(ValueError, match="ordinary"):
+        load_document(directory)
+
+
+def test_git_reads_each_layout_without_checkout(tmp_path: Path) -> None:
+    """Old PR comparisons retain their original cards after the local migration."""
+
+    def git(*args: str) -> str:
+        return subprocess.check_output(["git", *args], cwd=tmp_path, text=True).strip()
+
+    git("init")
+    git("config", "user.email", "test@example.org")
+    git("config", "user.name", "Test")
+    pool = tmp_path / "LeanPool"
+    pool.mkdir()
+    legacy = pool / "projects.yml"
+    legacy.write_text("projects:\n  - slug: a\n")
+    git("add", ".")
+    git("commit", "-m", "old registry")
+    before = git("rev-parse", "HEAD")
+    legacy.unlink()
+    (pool / "projects").mkdir()
+    (pool / "projects/a.yaml").write_text("slug: a\n")
+    git("add", ".")
+    git("commit", "-m", "new registry")
+    assert read_revision(tmp_path, before) == read_revision(tmp_path, "HEAD")
+
+
+def test_registry_symlinks_rejected_locally_and_in_git(tmp_path: Path) -> None:
+    """Card contents cannot come from outside the tracked project registry."""
+    directory = tmp_path / "LeanPool/projects"
+    directory.mkdir(parents=True)
+    target = tmp_path / "outside.yaml"
+    target.write_text("slug: a\n")
+    (directory / "a.yaml").symlink_to(target)
+    with pytest.raises(ValueError, match="ordinary"):
+        load_document(directory)
+    for arguments in [
+        ["init"],
+        ["config", "user.email", "test@example.org"],
+        ["config", "user.name", "Test"],
+        ["add", "."],
+        ["commit", "-m", "invalid registry"],
+    ]:
+        subprocess.run(
+            ["git", *arguments], cwd=tmp_path, check=True, capture_output=True
+        )
+    with pytest.raises(ValueError, match="file type"):
+        read_revision(tmp_path, "HEAD")
+    (directory / "a.yaml").unlink()
+    directory.rmdir()
+    directory.symlink_to(tmp_path, target_is_directory=True)
+    with pytest.raises(ValueError, match="symbolic link"):
+        load_document(directory)
+
+
+def test_remote_cards_are_read_in_one_complete_request(monkeypatch) -> None:
+    """Adding hundreds of independent cards does not add hundreds of API calls."""
+    entries = [
+        {
+            "name": f"p{i}.yaml",
+            "type": "blob",
+            "mode": 0o100644,
+            "object": {
+                "text": f"slug: p{i}\n",
+                "isTruncated": False,
+                "isBinary": False,
+            },
+        }
+        for i in range(300)
+    ]
+    calls = []
+
+    def output(arguments, **kwargs):
+        calls.append(arguments)
+        return json.dumps({"data": {"repository": {"object": {"entries": entries}}}})
+
+    monkeypatch.setattr(registry.subprocess, "check_output", output)
+    assert (
+        len(
+            yaml.safe_load(registry.remote_text("owner/repo", "head", lambda *a: None))[
+                "projects"
+            ]
+        )
+        == 300
+    )
+    assert len(calls) == 1
+    assert "expression=head:LeanPool/projects" in calls[0]
+
+
+@pytest.mark.parametrize(
+    "change",
+    [
+        {"mode": 0o120000},
+        {"type": "tree"},
+        {"name": "nested/a.yaml"},
+        {"object": {"text": "slug: a", "isTruncated": True, "isBinary": False}},
+        {"object": {"text": None, "isTruncated": False, "isBinary": True}},
+    ],
+)
+def test_incomplete_remote_cards_are_rejected(change) -> None:
+    """Unavailable or truncated metadata is never treated as a complete registry."""
+    entry = {
+        "name": "a.yaml",
+        "type": "blob",
+        "mode": 0o100644,
+        "object": {"text": "slug: a", "isTruncated": False, "isBinary": False},
+    }
+    entry.update(change)
+    with pytest.raises(ValueError, match="remote project card"):
+        registry._remote_cards(
+            {"data": {"repository": {"object": {"entries": [entry]}}}}
+        )
+
+
+def test_failed_remote_response_is_rejected() -> None:
+    """GraphQL failures cannot turn prior-art lookup into an empty project list."""
+    with pytest.raises(ValueError, match="unavailable"):
+        registry._remote_cards({"data": None, "errors": [{"message": "unavailable"}]})
diff --git a/python/tests/test_validation_cache.py b/python/tests/test_validation_cache.py
index 9756c435bc..2a9a6a5ed6 100644
--- a/python/tests/test_validation_cache.py
+++ b/python/tests/test_validation_cache.py
@@ -103,7 +103,12 @@ def test_checker_edits_invalidate_only_dependent_checks(
     for kind in kinds:
         for modules in pool_units(repository):
             cache.check(kind, modules, lambda: calls.append((kind, modules[0])) or [])
-    if name in {"python/lean_pool/quality.py", "scripts/nolints-style.txt"}:
+    if name in {
+        "python/lean_pool/quality.py",
+        "scripts/nolints-style.txt",
+        "python/lean_pool/registry.py",
+        "python/lean_pool/indexes.py",
+    }:
         fresh_kinds = ("axioms", "backdoors", "declarations", "future-check")
     elif name in {"scripts/ci/lint-project.lean", "scripts/nolints.json"}:
         fresh_kinds = ("lint", "future-check")
diff --git a/scripts/ci/plan-build-shards.py b/scripts/ci/plan-build-shards.py
index 3a4e463bda..53a54564c7 100644
--- a/scripts/ci/plan-build-shards.py
+++ b/scripts/ci/plan-build-shards.py
@@ -54,7 +54,7 @@ def project_weights() -> dict[str, int]:
     """
     weights: dict[str, int] = {}
     for entry in Path("LeanPool").iterdir():
-        if entry.is_dir():
+        if entry.is_dir() and entry.name != "projects":
             count = sum(1 for _ in entry.rglob("*.lean"))
             if Path(f"LeanPool/{entry.name}.lean").exists():
                 count += 1
diff --git a/scripts/import-formalization.sh b/scripts/import-formalization.sh
index cbe5d1c737..c5e0481b33 100755
--- a/scripts/import-formalization.sh
+++ b/scripts/import-formalization.sh
@@ -5,7 +5,7 @@
 #   1. Clone (or reuse) the external repo into a sibling scratch directory.
 #   2. Create a fresh git worktree of lean-pool on a new branch.
 #   3. Hand both paths to a headless agent (Claude or Codex)
-#      with a detailed prompt covering the bump, vendoring, projects.yml
+#      with a detailed prompt covering the bump, vendoring, project cards
 #      entry, file headers, and CI checks documented in
 #      .github/CODE_QUALITY.md.
 #   4. Whatever progress the agent makes, push the branch and open a PR in
@@ -80,14 +80,13 @@ github_repo_of() {
 
 source_repo_registered() {
   local repo="$1"
-  local projects_file="$LEAN_POOL_ROOT/LeanPool/projects.yml"
-  [[ "$repo" == */* && -f "$projects_file" ]] || return 1
-  local normalized_repo
-  normalized_repo="$(printf '%s' "$repo" | tr '[:upper:]' '[:lower:]')"
-  sed -n 's/^[[:space:]]*github_repo:[[:space:]]*//p' "$projects_file" \
-    | tr -d '"' \
-    | tr '[:upper:]' '[:lower:]' \
-    | grep -Fxq "$normalized_repo"
+  [[ "$repo" == */* ]] || return 1
+  command -v uv >/dev/null || die "uv is required to read the project registry."
+  local sources
+  sources="$(PYTHONPATH="$LEAN_POOL_ROOT/python" uv run \
+    --project "$LEAN_POOL_ROOT/python" python -m lean_pool.registry \
+    --repo "$LEAN_POOL_ROOT" --sources)" || die "Cannot read project registry."
+  printf '%s\n' "$sources" | grep -Fxiq "$repo"
 }
 
 # --- Argument parsing --------------------------------------------------------
@@ -166,7 +165,7 @@ mkdir -p "$BUMPS_DIR"
 RAW_SLUG="${SOURCE_URL%.git}"
 RAW_SLUG="${RAW_SLUG##*/}"
 
-# Lowercase slug used for directories, branch, and projects.yml entry.
+# Lowercase slug used for directories, branch, and project card.
 [[ -n "$SLUG" ]] || SLUG="$(echo "$RAW_SLUG" | tr '[:upper:]' '[:lower:]')"
 [[ "$SLUG" =~ ^[a-z0-9][a-z0-9_-]*$ ]] \
   || die "Derived slug '$SLUG' is not a valid identifier; pass --slug explicitly."
@@ -196,7 +195,7 @@ log "Model:         $MODEL  (effort: $EFFORT)"
 
 if SOURCE_GITHUB_REPO="$(github_repo_of "$SOURCE_URL")" \
    && source_repo_registered "$SOURCE_GITHUB_REPO"; then
-  ok "Source repo $SOURCE_GITHUB_REPO is already registered in LeanPool/projects.yml; skipping."
+  ok "Source repo $SOURCE_GITHUB_REPO is already registered in LeanPool/projects/; skipping."
   exit 0
 fi
 
@@ -329,6 +328,19 @@ fi
 # --- Build the agent prompt --------------------------------------------------
 
 LEAN_TOOLCHAIN="$(cat "$LEAN_POOL_ROOT/lean-toolchain")"
+LEGACY_LAYOUT=false
+REGISTRY_LOCATION="LeanPool/projects/${SLUG}.yaml"
+INDEX_INSTRUCTION='Run `lake exe mk_all` to regenerate the project Imports.lean. LeanPool.lean is fixed; do not edit it.'
+REGISTRY_INSTRUCTION="Write one project card mapping in ${REGISTRY_LOCATION} (no outer projects list)."
+CONTENT_SCOPE='Lean source files under `LeanPool/` and your project card under `LeanPool/projects/`. Do not edit `LeanPool.lean`.'
+# Allow an import to finish across the staged infrastructure/layout migration.
+if [[ -f "$WORKTREE/LeanPool/projects.yml" ]]; then
+  LEGACY_LAYOUT=true
+  REGISTRY_LOCATION='LeanPool/projects.yml'
+  INDEX_INSTRUCTION='Run `lake exe mk_all` to regenerate the project Imports.lean and the current legacy LeanPool.lean import list.'
+  REGISTRY_INSTRUCTION='Add your project card to the existing projects list in LeanPool/projects.yml; do not create a projects directory while the legacy registry exists.'
+  CONTENT_SCOPE='Lean source files under `LeanPool/`, the existing legacy `LeanPool/projects.yml`, and the generated `LeanPool.lean`.'
+fi
 
 read -r -d '' PROMPT <<PROMPT_EOF || true
 You are an autonomous Lean engineer importing an external Lean formalization into the lean-pool monorepo. You run unattended — there is no one watching and no one to hand off to. Your goal is a complete, working import: all of the CI checks below passing. A partial result is a failure; be thorough and relentless.
@@ -346,7 +358,7 @@ You are an autonomous Lean engineer importing an external Lean formalization int
 - Dependencies and the Mathlib cache are already fetched; \`.lake/packages\` may be a symlink to a shared, prebuilt store, so \`lake build LeanPool\` should not need to rebuild Mathlib and you should not run \`lake exe cache get\` or \`lake update\`.
 
 # Goal
-Vendor the source repo's Lean content into LeanPool/${SLUG}/, bump it to lean-pool's toolchain, register it in LeanPool/projects.yml, and make the local CI checks pass.
+Vendor the source repo's Lean content into LeanPool/${SLUG}/, bump it to lean-pool's toolchain, register it in ${REGISTRY_LOCATION}, and make the local CI checks pass.
 
 # Step-by-step
 1. Read ${SOURCE_DIR}/README.md (and the source repo's lakefile, lean-toolchain, LICENSE) to figure out: title, authors, main declarations, tags, license. lean-pool is Apache-2.0: an Apache-2.0 upstream is redistributed directly, MIT/BSD and similar permissive upstreams are sublicensed under Apache-2.0, and copyleft (GPL/LGPL/AGPL, CC-BY-SA) is incompatible — if the upstream is copyleft, STOP and write IMPORT_NOTES.md explaining (do NOT commit it; see note below). Unless the upstream is Apache-2.0, record its provenance in IMPORT_NOTES.md under a "NOTICE entry" heading — source repo URL, upstream license, and the upstream copyright notice verbatim if present — so the maintainer can add a matching entry to the root NOTICE file after merge; NOTICE is a non-content file and cannot be committed in the import PR.
@@ -359,8 +371,8 @@ Vendor the source repo's Lean content into LeanPool/${SLUG}/, bump it to lean-po
    - Strip diagnostic commands: \`#check\`, \`#print\`, \`#eval\`, \`#reduce\`, \`#guard_msgs\`, \`#lint\`.
    - Reject any file that depends on \`sorry\`, \`admit\`, a new \`axiom\`/\`constant\`, or uses \`unsafe\`/\`partial\`/\`opaque\`/\`@[extern]\`. First try to fix it (complete the proof; replace the unsafe construct). Only if you genuinely cannot, after real effort, may that one file be excluded as a last resort — and record in \`IMPORT_NOTES.md\` exactly what blocked you and what you tried.
 5. For every directory you create under LeanPool/, add an import-only index .lean file with a module docstring (style matches LeanPool/Basic.lean's header).
-6. Run \`lake exe mk_all\` to regenerate LeanPool.lean.
-7. Add a project entry to LeanPool/projects.yml. Required keys: slug, title, entry_module, authors (list), source ({url|arxiv|doi}), status: verified, main_declarations (list of fully-qualified names), tags (list). Optional: msc.
+6. ${INDEX_INSTRUCTION}
+7. ${REGISTRY_INSTRUCTION} Required keys: slug, title, entry_module, authors (list), source ({url|arxiv|doi}), license, provenance (human, AI, or mix), status: verified, main_declarations (list of fully-qualified names), tags (list). Optional: msc.
 8. Iterate — persistently, as many rounds as it takes — until ALL of these pass cleanly inside ${WORKTREE}:
    - \`lake exe mk_all --check\`
    - \`lake build LeanPool\` — and the build log must contain no warnings (CI greps for \`warning:\`).
@@ -379,7 +391,7 @@ Vendor the source repo's Lean content into LeanPool/${SLUG}/, bump it to lean-po
 - The build must be warning-free (CI fails on any \`warning:\` in the log).
 
 # Stay in your lane — what you may COMMIT
-You may add or modify, AND COMMIT, ONLY: \`LeanPool.lean\` (regenerate via \`lake exe mk_all\`), files under \`LeanPool/\` (including \`LeanPool/projects.yml\`). That's it — the Content-only PR CI gate rejects a PR that touches anything else. You may *write* \`IMPORT_NOTES.md\` locally (the wrapper reads it for the PR body) but you must NOT commit it. Do NOT modify ANYTHING else at all — in particular do NOT touch \`.github/\` (CI workflows, CODE_QUALITY.md), \`python/\` (incl. \`lean_pool/quality.py\`), \`scripts/\` (incl. \`nolints-style.txt\`), \`lakefile.toml\`, \`lean-toolchain\`, \`lake-manifest.json\`, \`AGENTS.md\`, \`CLAUDE.md\`, \`README.md\`, \`CONTRIBUTING.md\`, \`LICENSE\`, \`NOTICE\`, or \`.gitignore\`. Do NOT introduce any waiver/exception/escape-hatch: no \`size-limit-ok\` comment, no entry in \`scripts/nolints-style.txt\`, no \`set_option linter.X false\`, no linter toggle in \`lakefile.toml\`, no editing of \`quality.py\` or a workflow to skip a check. If a check fails, fix the code, not the check. If a proof exceeds 200 lines, split it into lemmas; if a file exceeds 10000 lines, split it into modules. The wrapper script reverts any committed change outside that allowlist (and untracks \`IMPORT_NOTES.md\`) before opening the PR, so out-of-scope edits accomplish nothing.
+You may add or modify, AND COMMIT, ONLY: ${CONTENT_SCOPE} That's it — the Content-only PR CI gate rejects a PR that touches anything else. You may *write* \`IMPORT_NOTES.md\` locally (the wrapper reads it for the PR body) but you must NOT commit it. Do NOT modify ANYTHING else at all — in particular do NOT touch \`.github/\` (CI workflows, CODE_QUALITY.md), \`python/\` (incl. \`lean_pool/quality.py\`), \`scripts/\` (incl. \`nolints-style.txt\`), \`lakefile.toml\`, \`lean-toolchain\`, \`lake-manifest.json\`, \`AGENTS.md\`, \`CLAUDE.md\`, \`README.md\`, \`CONTRIBUTING.md\`, \`LICENSE\`, \`NOTICE\`, or \`.gitignore\`. Do NOT introduce any waiver/exception/escape-hatch: no \`size-limit-ok\` comment, no entry in \`scripts/nolints-style.txt\`, no \`set_option linter.X false\`, no linter toggle in \`lakefile.toml\`, no editing of \`quality.py\` or a workflow to skip a check. If a check fails, fix the code, not the check. If a proof exceeds 200 lines, split it into lemmas; if a file exceeds 10000 lines, split it into modules. The wrapper script reverts any committed change outside that allowlist (and untracks \`IMPORT_NOTES.md\`) before opening the PR, so out-of-scope edits accomplish nothing.
 
 # Do not give up
 A partial import is a failure, not an acceptable stopping point. Bumping pain is expected — work through it: when a Mathlib declaration moved or was renamed, find the current name (grep the Mathlib source under \`.lake/packages/mathlib\`, search for nearby lemmas, check release notes); when a lemma you relied on no longer exists, prove it yourself in your own namespace; when a proof breaks under the new Mathlib, repair it; when \`simp\`/\`omega\`/\`aesop\` no longer closes a goal, find the steps that do. Excluding a file is the absolute last resort, permissible only after you have genuinely exhausted these avenues, and every exclusion must be justified in \`IMPORT_NOTES.md\` (local scratch — not committed) with the specific blocker and what you attempted. Keep iterating — many rounds if that's what it takes — until \`lake build LeanPool\` (warning-free), \`lake exe runLinter LeanPool\`, \`lake exe lint-style LeanPool\`, and the \`quality\` check are all clean. Do not stop early.
@@ -494,7 +506,7 @@ if git ls-files -- "${SCRATCH_FILES[@]}" | grep -q .; then
 fi
 
 # --- Guard: revert anything the agent touched outside the import allowlist ---
-# An import may only add/modify LeanPool.lean and LeanPool/**. If the agent
+# An import may only add/modify project Lean sources and project cards. If the agent
 # edited CI workflows, quality.py, lint allowlists, lakefile/toolchain/manifest,
 # etc. — or *added* any file outside LeanPool/ (a sneak attempt to slip a new
 # script or workflow into the PR) — undo it before the PR goes up. Reverting
@@ -510,7 +522,9 @@ while IFS= read -r -d '' tok; do
   if [[ -z "$status" ]]; then status="$tok"; continue; fi
   p="$tok"; s="$status"; status=""
   case "$p" in
-    LeanPool.lean|LeanPool/*) continue ;;   # allowed
+    LeanPool/*.lean|LeanPool/projects/*.yaml) continue ;;   # allowed
+    LeanPool.lean|LeanPool/projects.yml)
+      if [[ "$LEGACY_LAYOUT" == true ]]; then continue; fi ;;
   esac
   case "$s" in
     A|A?*)        # added by the agent: just remove
@@ -543,7 +557,7 @@ if [[ ${#OUT_OF_SCOPE[@]} -gt 0 ]]; then
   git add -A
   unstage_scratch
   git commit -m "Revert agent edits outside the import allowlist" \
-    -m "Auto-reverted by scripts/import-formalization.sh (an import may only touch LeanPool.lean and LeanPool/): ${OUT_OF_SCOPE[*]}" || true
+    -m "Auto-reverted by scripts/import-formalization.sh (an import may only touch project Lean sources and project cards): ${OUT_OF_SCOPE[*]}" || true
 fi
 
 # The allowlist above intentionally permits LeanPool/** because imports live
diff --git a/scripts/run-import-queue.sh b/scripts/run-import-queue.sh
index 0367db6f5e..15722f1804 100755
--- a/scripts/run-import-queue.sh
+++ b/scripts/run-import-queue.sh
@@ -89,15 +89,15 @@ github_repo_of() {
 }
 
 is_registered_source() {
-  local repo normalized_repo
+  local repo
   repo="$(github_repo_of "$1")" || return 1
   [[ "$repo" == */* ]] || return 1
-  [[ -f "$LEAN_POOL_ROOT/LeanPool/projects.yml" ]] || return 1
-  normalized_repo="$(printf '%s' "$repo" | tr '[:upper:]' '[:lower:]')"
-  sed -n 's/^[[:space:]]*github_repo:[[:space:]]*//p' "$LEAN_POOL_ROOT/LeanPool/projects.yml" \
-    | tr -d '"' \
-    | tr '[:upper:]' '[:lower:]' \
-    | grep -Fxq "$normalized_repo"
+  command -v uv >/dev/null || die "uv is required to read the project registry."
+  local sources
+  sources="$(PYTHONPATH="$LEAN_POOL_ROOT/python" uv run \
+    --project "$LEAN_POOL_ROOT/python" python -m lean_pool.registry \
+    --repo "$LEAN_POOL_ROOT" --sources)" || die "Cannot read project registry."
+  printf '%s\n' "$sources" | grep -Fxiq "$repo"
 }
 
 # --- One import (also the worker invoked by the parallel fan-out) ------------
@@ -113,7 +113,7 @@ if [[ "${1:-}" == "--run-one" ]]; then
   QUEUE_DIR="$BUMPS_DIR/queue-logs"; mkdir -p "$QUEUE_DIR"
   LOGF="$QUEUE_DIR/$SLUG-import.log"
   if is_registered_source "$URL"; then
-    log "SKIP  $SLUG — source already registered in LeanPool/projects.yml."
+    log "SKIP  $SLUG — source already registered in LeanPool/projects/."
     exit 0
   fi
   # Skip if the branch already exists upstream (resume support).