diff --git a/.github/workflows/auto-rebase.yml b/.github/workflows/auto-rebase.yml
index f7aa421748..fe81893a8f 100644
--- a/.github/workflows/auto-rebase.yml
+++ b/.github/workflows/auto-rebase.yml
@@ -27,6 +27,13 @@ on:
       - 'LeanPool/**'
       - 'LeanPool.lean'
   workflow_dispatch:
+  pull_request_target:
+    types: [ready_for_review]
+  workflow_run:
+    workflows: [Lean Action CI, Documentation, Exposition Verify]
+    types: [completed]
+  schedule:
+    - cron: '*/15 * * * *'
 
 concurrency:
   # Serialised: two runs rebasing the same PR would race on its branch.
@@ -45,21 +52,22 @@ jobs:
       pulls: ${{ steps.list.outputs.pulls }}
       any: ${{ steps.list.outputs.any }}
     steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          ref: main
+          persist-credentials: false
+
       - name: Collect open pull requests
         id: list
         env:
           GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           REPO: ${{ github.repository }}
+          TARGET_PR: ${{ github.event.pull_request.number || github.event.workflow_run.pull_requests[0].number || 0 }}
         run: |
           set -euo pipefail
           pulls="$(gh pr list --repo "$REPO" --state open --limit 100 \
-            --json number,headRefName,headRepository,headRepositoryOwner,isCrossRepository,labels \
-            --jq '[.[]
-                  | select([.labels[].name] | index("needs-manual-rebase") | not)
-                  | select(.headRefName | startswith("bump/") | not)
-                  | {number, branch: .headRefName,
-                     repo: "\(.headRepositoryOwner.login)/\(.headRepository.name)",
-                     fork: .isCrossRepository}]')"
+            --json number,headRefName,headRefOid,headRepository,headRepositoryOwner,isCrossRepository,labels,isDraft,baseRefName,statusCheckRollup \
+            | PYTHONPATH=python python3 -m lean_pool.rebase_queue select --number "$TARGET_PR")"
           echo "pulls=$pulls" >> "$GITHUB_OUTPUT"
           if [ "$(echo "$pulls" | python3 -c 'import json,sys; print(len(json.load(sys.stdin)))')" = "0" ]; then
             echo "any=false" >> "$GITHUB_OUTPUT"
@@ -82,17 +90,49 @@ jobs:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
         with:
           fetch-depth: 0
+          ref: main
           token: ${{ secrets.REBASE_TOKEN || secrets.GITHUB_TOKEN }}
 
+      - name: Check this content branch needs updating
+        id: scope
+        env:
+          NUMBER: ${{ matrix.pull.number }}
+          BRANCH: ${{ matrix.pull.branch }}
+          EXPECTED_HEAD: ${{ matrix.pull.head }}
+          HEAD_REPO: ${{ matrix.pull.repo }}
+          TOKEN: ${{ secrets.REBASE_TOKEN || secrets.GITHUB_TOKEN }}
+        run: |
+          set -euo pipefail
+          cp python/lean_pool/rebase_queue.py "$RUNNER_TEMP/rebase-queue.py"
+          git remote add head "https://x-access-token:$TOKEN@github.com/$HEAD_REPO"
+          git fetch head "$BRANCH"
+          git fetch origin main
+          git checkout -B "pr-$NUMBER" "head/$BRANCH"
+          if [ "$(git rev-parse HEAD)" != "$EXPECTED_HEAD" ]; then
+            echo "Author updated the branch; defer until its checks finish."
+            echo "needed=false" >> "$GITHUB_OUTPUT"
+          elif git merge-base --is-ancestor origin/main HEAD; then
+            echo "Already includes current main."
+            echo "needed=false" >> "$GITHUB_OUTPUT"
+          elif python3 "$RUNNER_TEMP/rebase-queue.py" content; then
+            echo "needed=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "Infrastructure PR; preserve its current validation run."
+            echo "needed=false" >> "$GITHUB_OUTPUT"
+          fi
+
       - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+        if: steps.scope.outputs.needed == 'true'
         with:
           enable-cache: true
 
       - name: Install Python tooling
+        if: steps.scope.outputs.needed == 'true'
         run: cd python && uv sync --locked
 
       - name: Check we can push to this branch
         id: capable
+        if: steps.scope.outputs.needed == 'true'
         env:
           FORK: ${{ matrix.pull.fork }}
           HAS_TOKEN: ${{ secrets.REBASE_TOKEN != '' }}
@@ -118,11 +158,6 @@ jobs:
           git config user.name "github-actions[bot]"
           git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
 
-          remote="https://x-access-token:$TOKEN@github.com/$HEAD_REPO"
-          git remote add head "$remote"
-          git fetch head "$BRANCH"
-          git checkout -B "pr-$NUMBER" "head/$BRANCH"
-
           if git merge --no-edit origin/main; then
             echo "Merged cleanly."
             if git diff --quiet "head/$BRANCH" HEAD; then
@@ -179,7 +214,17 @@ jobs:
         env:
           NUMBER: ${{ matrix.pull.number }}
           BRANCH: ${{ matrix.pull.branch }}
-        run: git push head "pr-$NUMBER:$BRANCH"
+          EXPECTED_HEAD: ${{ matrix.pull.head }}
+          REPO: ${{ github.repository }}
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          set -euo pipefail
+          if gh pr view "$NUMBER" --repo "$REPO" --json headRefOid,isDraft,statusCheckRollup \
+            | python3 "$RUNNER_TEMP/rebase-queue.py" can-push --head "$EXPECTED_HEAD"; then
+            git push head "pr-$NUMBER:$BRANCH"
+          else
+            echo "Branch or checks changed; defer this update."
+          fi
 
       - name: Flag PRs that need a human
         if: steps.rebase.outputs.result == 'manual' || steps.capable.outputs.ok == 'false'
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index b18dae1d6c..f61289433f 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -15,6 +15,7 @@ on:
       - '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/docs.yml'
@@ -38,6 +39,7 @@ on:
       - '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'
@@ -70,6 +72,7 @@ jobs:
     runs-on: ubuntu-latest
     name: Documentation preflight
     outputs:
+      build_revision: ${{ steps.build-identity.outputs.revision }}
       readme_only: ${{ steps.scope.outputs.readme_only }}
       rebase_only: ${{ steps.rebase.outputs.rebase_only }}
     steps:
@@ -78,6 +81,13 @@ jobs:
         with:
           fetch-depth: 0
 
+      - name: Identify compiled Lean sources
+        id: build-identity
+        run: |
+          set -euo pipefail
+          revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)
+          echo "revision=$revision" >> "$GITHUB_OUTPUT"
+
       - name: Detect README-only change
         id: scope
         env:
@@ -194,6 +204,9 @@ jobs:
        (github.event_name == 'workflow_dispatch' && inputs.preview))
     runs-on: ubuntu-latest
     name: Build exposition site
+    permissions:
+      contents: read
+      actions: write
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
@@ -208,10 +221,11 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Restore pool build
+        id: pool-build
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.preflight.outputs.build_revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -234,6 +248,7 @@ jobs:
           fi
 
       - name: Reuse matching Lean CI build
+        if: steps.pool-build.outputs.cache-hit != 'true'
         env:
           GH_TOKEN: ${{ github.token }}
           BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
@@ -271,6 +286,17 @@ jobs:
           path: .lake/exposition-cache/v1
           key: ${{ steps.extraction-cache.outputs.cache-primary-key }}
 
+      - name: Prune old copies of project extraction cache
+        if: steps.extraction-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          CACHE_KEY: ${{ steps.extraction-cache.outputs.cache-primary-key }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
+          --repository "$REPOSITORY" --key "$CACHE_KEY"
+
       - name: Upload extraction timings and logs
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
@@ -318,6 +344,9 @@ jobs:
        (github.event_name == 'workflow_dispatch' && inputs.preview))
     runs-on: ubuntu-latest
     name: Build Mathlib documentation data
+    permissions:
+      contents: read
+      actions: write
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
@@ -401,6 +430,17 @@ jobs:
             .lake/packages/MD4Lean
           key: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}
 
+      - name: Prune old copies of mathlib documentation checkpoint
+        if: steps.mathlib-doc-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          CACHE_KEY: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
+          --repository "$REPOSITORY" --key "$CACHE_KEY"
+
   build:
     needs:
       - preflight
@@ -411,6 +451,9 @@ jobs:
        (github.event_name == 'workflow_dispatch' && inputs.preview))
     runs-on: ubuntu-latest
     name: Build doc-gen4 site
+    permissions:
+      contents: read
+      actions: write
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
@@ -425,10 +468,11 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Restore pool build
+        id: pool-build
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.preflight.outputs.build_revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -446,7 +490,7 @@ jobs:
             .lake/packages/UnicodeBasic
             .lake/packages/BibtexQuery
             .lake/packages/MD4Lean
-          key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ github.sha }}
+          key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }}
           restore-keys: |
             DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-
 
@@ -483,6 +527,7 @@ jobs:
           fi
 
       - name: Reuse matching Lean CI build
+        if: steps.pool-build.outputs.cache-hit != 'true'
         env:
           GH_TOKEN: ${{ github.token }}
           BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
@@ -526,7 +571,18 @@ jobs:
             .lake/packages/UnicodeBasic
             .lake/packages/BibtexQuery
             .lake/packages/MD4Lean
-          key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ github.sha }}
+          key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }}
+
+      - name: Prune old copies of pool documentation checkpoint
+        if: steps.pool-doc-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          CACHE_KEY: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
+          --repository "$REPOSITORY" --key "$CACHE_KEY"
 
       - name: Build documentation
         run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs
diff --git a/.github/workflows/exposition-verify.yml b/.github/workflows/exposition-verify.yml
index 71c92b483c..420356b851 100644
--- a/.github/workflows/exposition-verify.yml
+++ b/.github/workflows/exposition-verify.yml
@@ -35,6 +35,10 @@ jobs:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
 
+      - name: Identify compiled Lean sources
+        id: build-identity
+        run: echo "revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)" >> "$GITHUB_OUTPUT"
+
       # Match Lean Action CI's cache lookup exactly. This workflow only needs
       # compiled Lean artifacts; restoring doc-gen output here used to make a
       # broad fallback pull an incompatible cache after every toolchain bump.
@@ -48,10 +52,11 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Restore pool build
+        id: pool-build
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ steps.build-identity.outputs.revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -74,6 +79,7 @@ jobs:
           fi
 
       - name: Reuse matching Lean CI build
+        if: steps.pool-build.outputs.cache-hit != 'true' && github.event_name != 'pull_request'
         env:
           GH_TOKEN: ${{ github.token }}
           BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index d05a622b0d..13995e7a4b 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -36,6 +36,8 @@ on:
       - '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_validation_artifacts.py'
       - 'python/lean_pool/rebase_fastpath.py'
       - 'python/pyproject.toml'
       - 'python/uv.lock'
@@ -63,6 +65,8 @@ on:
       - '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_validation_artifacts.py'
       - 'python/lean_pool/rebase_fastpath.py'
       - 'python/pyproject.toml'
       - 'python/uv.lock'
@@ -79,10 +83,10 @@ on:
         type: boolean
         default: false
 
-# Cancel superseded runs on the same branch / PR.
+# Let main finish and seed caches; cancel superseded PR runs.
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: true
+  cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}
 
 permissions:
   contents: read
@@ -95,6 +99,8 @@ jobs:
     runs-on: ubuntu-latest
     name: Plan build
     outputs:
+      build_revision: ${{ steps.build-identity.outputs.revision }}
+      base_build_revision: ${{ steps.build-identity.outputs.base_revision }}
       mode: ${{ steps.plan.outputs.mode }}
       matrix: ${{ steps.plan.outputs.matrix }}
       reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }}
@@ -105,15 +111,25 @@ jobs:
         with:
           fetch-depth: 0
 
-      # Only checks whether a warm build cache exists; a cold cache means a
-      # whole-pool build, which is exactly when sharding pays off most.
+      - name: Identify compiled Lean sources
+        id: build-identity
+        env:
+          BASE_REF: ${{ github.event.pull_request.base.sha || github.sha }}
+        run: |
+          set -euo pipefail
+          revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)
+          echo "revision=$revision" >> "$GITHUB_OUTPUT"
+          base_revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision --ref "$BASE_REF")
+          echo "base_revision=$base_revision" >> "$GITHUB_OUTPUT"
+
+      # A cold build cache is when whole-pool sharding pays off most.
       - name: Check for a warm build cache
         id: lake-cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           lookup-only: true
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ steps.build-identity.outputs.revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -186,6 +202,9 @@ jobs:
     if: needs.plan.outputs.mode == 'single'
     runs-on: ubuntu-latest
     name: Build pool
+    permissions:
+      contents: read
+      actions: write
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
@@ -207,7 +226,7 @@ jobs:
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -239,7 +258,21 @@ jobs:
             exit 1
           fi
 
+      - name: Reuse compiled projects from merged PRs
+        if: github.event_name == 'push' && steps.cache.outputs.cache-hit != 'true'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          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 \
+              --repository "$REPOSITORY" --head "$BEFORE_SHA" --base "$GITHUB_SHA"
+          fi
+
       - name: Build project
+        id: compilation
         run: |
           set -euo pipefail
           ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
@@ -259,7 +292,7 @@ jobs:
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
           name: lean-pool-build
-          path: lean-pool-build.tar.gz
+          path: lean-pool-build.tar.zst
           if-no-files-found: error
           compression-level: 0
           retention-days: 1
@@ -274,6 +307,16 @@ jobs:
           restore-keys: |
             LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
+      - name: Recover saved validation when caches were evicted
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BUILD_EVENT: ${{ github.event_name }}
+          BUILD_HEAD: ${{ github.sha }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_validation_artifacts
+          --event "$BUILD_EVENT" --head "$BUILD_HEAD"
+
       - name: Install validation dependencies
         run: cd python && uv sync --locked
 
@@ -292,6 +335,17 @@ jobs:
           cd python
           uv run python -m lean_pool.validation_cache quality --repo ..
 
+      - name: Retain successful validation independently of build caches
+        continue-on-error: true
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: lean-validation-receipts
+          path: .lake/validation-cache/v1/passes.json
+          include-hidden-files: true
+          if-no-files-found: error
+          compression-level: 1
+          retention-days: 14
+
       - name: Package PR project build for later rebases
         if: github.event_name == 'pull_request'
         continue-on-error: true
@@ -318,6 +372,17 @@ jobs:
           path: .lake/validation-cache/v1
           key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
 
+      - name: Prune old copies of project validation
+        if: success() && github.ref == 'refs/heads/main'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          CACHE_KEY: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
+          --repository "$REPOSITORY" --key "$CACHE_KEY"
+
       - name: Save Lean dependencies
         if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'
         uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
@@ -327,12 +392,34 @@ jobs:
             .lake/packages
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
+      - name: Prune old copies of lean dependencies
+        if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          CACHE_KEY: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
+          --repository "$REPOSITORY" --key "$CACHE_KEY"
+
       - name: Save pool build
-        if: always() && github.ref == 'refs/heads/main'
+        if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
         uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
+
+      - name: Prune old copies of pool build
+        if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          CACHE_KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
+          --repository "$REPOSITORY" --key "$CACHE_KEY"
 
   shard:
     needs: plan
@@ -362,10 +449,11 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Restore pool build
+        id: cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -440,6 +528,9 @@ jobs:
       needs.plan.outputs.mode == 'sharded'
     runs-on: ubuntu-latest
     name: Assemble and lint
+    permissions:
+      contents: read
+      actions: write
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
@@ -456,10 +547,11 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Restore pool build
+        id: cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -511,6 +603,7 @@ jobs:
       # builds the root module and anything a shard missed or failed to
       # deliver, so the assembled pool is complete regardless.
       - name: Build project
+        id: compilation
         run: |
           set -euo pipefail
           ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
@@ -530,7 +623,7 @@ jobs:
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
           name: lean-pool-build
-          path: lean-pool-build.tar.gz
+          path: lean-pool-build.tar.zst
           if-no-files-found: error
           compression-level: 0
           retention-days: 1
@@ -545,6 +638,16 @@ jobs:
           restore-keys: |
             LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
+      - name: Recover saved validation when caches were evicted
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BUILD_EVENT: ${{ github.event_name }}
+          BUILD_HEAD: ${{ github.sha }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_validation_artifacts
+          --event "$BUILD_EVENT" --head "$BUILD_HEAD"
+
       - name: Install validation dependencies
         run: cd python && uv sync --locked
 
@@ -563,6 +666,17 @@ jobs:
           cd python
           uv run python -m lean_pool.validation_cache quality --repo ..
 
+      - name: Retain successful validation independently of build caches
+        continue-on-error: true
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: lean-validation-receipts
+          path: .lake/validation-cache/v1/passes.json
+          include-hidden-files: true
+          if-no-files-found: error
+          compression-level: 1
+          retention-days: 14
+
       - name: Package PR project build for later rebases
         if: github.event_name == 'pull_request'
         continue-on-error: true
@@ -589,6 +703,17 @@ jobs:
           path: .lake/validation-cache/v1
           key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
 
+      - name: Prune old copies of project validation
+        if: success() && github.ref == 'refs/heads/main'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          CACHE_KEY: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
+          --repository "$REPOSITORY" --key "$CACHE_KEY"
+
       - name: Save Lean dependencies
         if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'
         uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
@@ -598,15 +723,37 @@ jobs:
             .lake/packages
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
+      - name: Prune old copies of lean dependencies
+        if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          CACHE_KEY: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
+          --repository "$REPOSITORY" --key "$CACHE_KEY"
+
       - name: Save pool build
-        if: always() && github.ref == 'refs/heads/main'
+        if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
         uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
 
   # Reuse the prior green project's compiled modules and current main's cache.
   # A missing artifact falls back to the full validation sequence in this job.
+      - name: Prune old copies of pool build
+        if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          CACHE_KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
+          --repository "$REPOSITORY" --key "$CACHE_KEY"
+
   rebase:
     needs: plan
     if: needs.plan.outputs.mode == 'rebase'
@@ -631,7 +778,7 @@ jobs:
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.event.pull_request.base.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.base_build_revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -696,8 +843,7 @@ jobs:
         if: steps.project-build.outcome == 'success'
         run: cd python && uv run python -m lean_pool.quality --repo .. --static-only
 
-      - name: Restore validation cache for full fallback
-        if: steps.project-build.outcome != 'success'
+      - name: Restore validation cache for the combined checkout
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/validation-cache/v1
@@ -705,6 +851,16 @@ jobs:
           restore-keys: |
             LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
+      - name: Carry saved checks through the verified rebase
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          PREVIOUS_RUN: ${{ needs.plan.outputs.reuse_run_id }}
+          BUILD_HEAD: ${{ github.sha }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_validation_artifacts
+          --event pull_request --head "$BUILD_HEAD" --previous-run "$PREVIOUS_RUN"
+
       - name: Full validation when the prior artifact is unavailable
         if: steps.project-build.outcome != 'success'
         run: |
@@ -713,6 +869,17 @@ jobs:
           ~/.elan/bin/lake exe lint-style LeanPool
           (cd python && uv run python -m lean_pool.validation_cache quality --repo ..)
 
+      - name: Retain successful validation independently of build caches
+        continue-on-error: true
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: lean-validation-receipts
+          path: .lake/validation-cache/v1/passes.json
+          include-hidden-files: true
+          if-no-files-found: warn
+          compression-level: 1
+          retention-days: 14
+
       - name: Package PR project build for later rebases
         continue-on-error: true
         env:
diff --git a/.github/workflows/proof-profile.yml b/.github/workflows/proof-profile.yml
index 33cbcba1c8..6613b23f4d 100644
--- a/.github/workflows/proof-profile.yml
+++ b/.github/workflows/proof-profile.yml
@@ -1,7 +1,8 @@
 name: Proof Profile
 
-# Profile once when a PR is opened, and again on demand when the PR author (or
-# anyone with write access) comments `/profile`. No `synchronize` trigger — the
+# Profile once when a ready PR is opened or a draft becomes ready, and again
+# on demand when the PR author or anyone with write access comments `/profile`.
+# No `synchronize` trigger — the
 # profile is advisory, so re-run it by hand after a push if you want a fresh
 # one. That on-demand path is what lets an external contributor re-profile
 # their own PR after pushing. workflow_dispatch takes an explicit PR number.
@@ -47,7 +48,7 @@ name: Proof Profile
 
 on:
   pull_request:
-    types: [opened]
+    types: [opened, ready_for_review]
   issue_comment:
     types: [created]
   workflow_dispatch:
@@ -88,7 +89,7 @@ jobs:
   plan:
     runs-on: ubuntu-latest
     name: Plan profile
-    # Run on a fresh PR or a workflow_dispatch unconditionally; for issue
+    # Run automatically on ready PRs; workflow_dispatch also supports drafts. For issue
     # comments, only when the body starts with `/profile` AND the commenter is
     # either the PR author or someone with write access. The measurement jobs
     # check out and *run* the PR's Lean code, so the workflow stays
@@ -100,7 +101,7 @@ jobs:
     # arbitrary commenter from triggering a run on someone else's fork PR.
     if: >-
       github.event_name == 'workflow_dispatch' ||
-      github.event_name == 'pull_request' ||
+      (github.event_name == 'pull_request' && !github.event.pull_request.draft) ||
       (github.event_name == 'issue_comment' &&
        github.event.issue.pull_request != null &&
        startsWith(github.event.comment.body, '/profile') &&
diff --git a/python/lean_pool/ci_artifacts.py b/python/lean_pool/ci_artifacts.py
index 900113dd96..e164a64463 100644
--- a/python/lean_pool/ci_artifacts.py
+++ b/python/lean_pool/ci_artifacts.py
@@ -9,6 +9,7 @@
 from __future__ import annotations
 
 import argparse
+import gzip
 import hashlib
 import io
 import json
@@ -20,12 +21,14 @@
 import tempfile
 import time
 import zipfile
+from contextlib import contextmanager
 from pathlib import Path, PurePosixPath
 from urllib.parse import urlencode
 
 LOGGER = logging.getLogger(__name__)
 ARTIFACT_NAME = "lean-pool-build"
-ARCHIVE_NAME = "lean-pool-build.tar.gz"
+ARCHIVE_NAME = "lean-pool-build.tar.zst"
+LEGACY_ARCHIVE_NAME = "lean-pool-build.tar.gz"
 MANIFEST_NAME = "build-manifest.json"
 
 
@@ -49,47 +52,96 @@ def build_identity(root: Path) -> dict:
     }
 
 
+@contextmanager
+def _compressed_stream(path: Path, *, writing: bool = False):
+    """Stream compression and verify completion before accepting an archive."""
+    if path.suffix == ".gz":
+        with gzip.open(path, "wb" if writing else "rb", compresslevel=1) as stream:
+            yield stream
+            if not writing:
+                while stream.read(1024 * 1024):
+                    pass
+        return
+    command = (
+        ["zstd", "--quiet", "-1", "-T2"]
+        if writing
+        else ["zstd", "--quiet", "--decompress", "--stdout", str(path)]
+    )
+    with path.open("wb") if writing else open(os.devnull, "wb") as output:
+        process = subprocess.Popen(
+            command,
+            stdin=subprocess.PIPE if writing else subprocess.DEVNULL,
+            stdout=output if writing else subprocess.PIPE,
+        )
+        stream = process.stdin if writing else process.stdout
+        try:
+            yield stream
+            if not writing:
+                while stream.read(1024 * 1024):
+                    pass
+            stream.close()
+            if process.wait() != 0:
+                raise subprocess.CalledProcessError(process.returncode, command)
+        finally:
+            stream.close()
+            if process.poll() is None:
+                process.terminate()
+            process.wait()
+
+
 def pack_build(root: Path, destination: Path) -> None:
-    """Package the completed root build; toolchains and dependencies stay in caches."""
+    """Package all completed build files using fast, bounded-memory compression."""
     subprocess.run(["git", "diff", "--exit-code", "HEAD", "--"], cwd=root, check=True)
     payload = json.dumps(build_identity(root)).encode()
     manifest = tarfile.TarInfo(MANIFEST_NAME)
     manifest.size = len(payload)
-    with tarfile.open(
-        destination, "w:gz", compresslevel=1, dereference=True
-    ) as archive:
-        archive.addfile(manifest, io.BytesIO(payload))
-        archive.add(root / ".lake/build", arcname=".lake/build")
+    with _compressed_stream(destination, writing=True) as stream:
+        with tarfile.open(fileobj=stream, mode="w|", dereference=True) as archive:
+            archive.addfile(manifest, io.BytesIO(payload))
+            archive.add(root / ".lake/build", arcname=".lake/build")
+
+
+def _extract_build(root: Path, archive: tarfile.TarFile, temporary: Path) -> bool:
+    """Check the manifest first, then extract only ordinary build files."""
+    manifest = archive.next()
+    if manifest is None or manifest.name != MANIFEST_NAME or not manifest.isfile():
+        raise ValueError("Missing build archive manifest")
+    if json.load(archive.extractfile(manifest)) != build_identity(root):
+        LOGGER.info("CI build has different sources or configuration; rebuilding")
+        return False
+    has_files = False
+    for member in archive:
+        if member is manifest:
+            continue
+        path = PurePosixPath(member.name)
+        if (
+            path.parts[:2] != (".lake", "build")
+            or ".." in path.parts
+            or not (member.isfile() or member.isdir())
+        ):
+            raise ValueError(f"Unexpected build archive member: {member.name}")
+        has_files |= member.isfile()
+        archive.extract(member, temporary, filter="data")
+    if not has_files:
+        raise ValueError("Empty Lean build artifact")
+    return True
 
 
 def restore_build(root: Path, archive_path: Path) -> bool:
-    """Validate identity and archive paths before replacing the root build."""
-    with tarfile.open(archive_path, "r:gz") as archive:
-        manifest = archive.extractfile(MANIFEST_NAME)
-        if manifest is None or json.load(manifest) != build_identity(root):
-            LOGGER.info(
-                "CI build has a different source tree or configuration; rebuilding"
-            )
-            return False
-        members = [
-            member for member in archive.getmembers() if member.name != MANIFEST_NAME
-        ]
-        for member in members:
-            path = PurePosixPath(member.name)
-            if (
-                path.parts[:2] != (".lake", "build")
-                or ".." in path.parts
-                or not (member.isfile() or member.isdir())
-            ):
-                raise ValueError(f"Unexpected build archive member: {member.name}")
-        if not any(member.isfile() for member in members):
-            raise ValueError("Empty Lean build artifact")
-        with tempfile.TemporaryDirectory(prefix="lean-ci-build-") as temporary:
-            archive.extractall(temporary, members=members, filter="data")
-            destination = root / ".lake/build"
-            if destination.exists():
-                shutil.rmtree(destination)
-            shutil.copytree(Path(temporary) / ".lake/build", destination)
+    """Validate and unpack once, then move the finished build into place."""
+    (root / ".lake").mkdir(exist_ok=True)
+    with tempfile.TemporaryDirectory(
+        prefix="lean-ci-build-", dir=root / ".lake"
+    ) as name:
+        temporary = Path(name)
+        with _compressed_stream(archive_path) as stream:
+            with tarfile.open(fileobj=stream, mode="r|") as archive:
+                if not _extract_build(root, archive, temporary):
+                    return False
+        destination = root / ".lake/build"
+        if destination.exists():
+            shutil.rmtree(destination)
+        (temporary / ".lake/build").rename(destination)
     LOGGER.info("Restored Lean CI build for the current source tree")
     return True
 
@@ -139,16 +191,24 @@ def download_build(root: Path, repository: str, artifact: int) -> bool:
                 timeout=600,
             )
         with zipfile.ZipFile(zipped) as archive:
-            if archive.namelist() != [ARCHIVE_NAME]:
+            names = archive.namelist()
+            if names not in ([ARCHIVE_NAME], [LEGACY_ARCHIVE_NAME]):
                 raise ValueError("Unexpected files in Lean CI artifact")
-            with archive.open(ARCHIVE_NAME) as source:
-                with (directory / ARCHIVE_NAME).open("wb") as destination:
+            name = names[0]
+            with archive.open(name) as source:
+                with (directory / name).open("wb") as destination:
                     shutil.copyfileobj(source, destination)
-        return restore_build(root, directory / ARCHIVE_NAME)
+        return restore_build(root, directory / name)
 
 
 def reuse_build(root: Path, repository: str, head: str, event: str, wait: int) -> 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":
+        LOGGER.info(
+            "PRs do not publish full build artifacts; using the regular Lake build"
+        )
+        return False
     try:
         run = matching_run(repository, head, event)
         if run is None:
@@ -168,6 +228,7 @@ def reuse_build(root: Path, repository: str, head: str, event: str, wait: int) -
         ValueError,
         KeyError,
         tarfile.TarError,
+        EOFError,
         zipfile.BadZipFile,
     ):
         LOGGER.exception("Could not reuse CI output; using the regular Lake build")
diff --git a/python/lean_pool/ci_cache.py b/python/lean_pool/ci_cache.py
new file mode 100644
index 0000000000..8d79e09dec
--- /dev/null
+++ b/python/lean_pool/ci_cache.py
@@ -0,0 +1,132 @@
+"""Identify reusable Lean builds and bound saved main-branch cache copies."""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import json
+import logging
+import subprocess
+from pathlib import Path
+from typing import Any
+
+LOGGER = logging.getLogger(__name__)
+CACHE_PREFIXES = (
+    "LeanPoolBuild-v1-",
+    "LeanDependencies-v1-",
+    "LeanValidation-v1-",
+    "DocsInfo-v3-",
+    "DocsInfoMathlib-v3-",
+    "Exposition-v1-",
+)
+
+
+def build_revision(root: Path, reference: str = "HEAD") -> str:
+    """Identify tracked Lean sources and build scripts independently of commit IDs."""
+    sources = subprocess.check_output(
+        [
+            "git",
+            "ls-tree",
+            "-r",
+            "-z",
+            reference,
+            "--",
+            "LeanPool",
+            "LeanPool.lean",
+            "scripts/ProjectIndexes.lean",
+        ],
+        cwd=root,
+    )
+    sources = b"\0".join(
+        entry
+        for entry in sources.split(b"\0")
+        if entry.rsplit(b"\t", 1)[-1].endswith(b".lean")
+    )
+    if not sources:
+        raise ValueError("no Lean build sources found")
+    return hashlib.sha256(sources).hexdigest()
+
+
+def cache_family(key: str) -> str:
+    """Limit retention to one known cache kind on one runner operating system."""
+    for prefix in CACHE_PREFIXES:
+        if key.startswith(prefix):
+            operating_system, separator, identity = key[len(prefix) :].partition("-")
+            if operating_system and separator and identity:
+                return prefix + operating_system + "-"
+    raise ValueError(f"unsupported cache key: {key}")
+
+
+def obsolete_caches(caches: list[dict[str, Any]], key: str) -> list[int]:
+    """Prune old copies only after the replacement is visible on main."""
+    family = cache_family(key)
+    replacements = [
+        cache
+        for cache in caches
+        if cache.get("ref") == "refs/heads/main" and cache.get("key") == key
+    ]
+    if not replacements:
+        return []
+    created = replacements[0].get("created_at", "")
+    return [
+        cache["id"]
+        for cache in caches
+        if cache.get("ref") == "refs/heads/main"
+        and isinstance(cache.get("key"), str)
+        and cache["key"].startswith(family)
+        and cache["key"] != key
+        and (not created or cache.get("created_at", "") < created)
+    ]
+
+
+def prune_cache(repository: str, key: str) -> None:
+    """Retain the replacement and remove older copies after a successful upload."""
+    cache_family(key)
+    pages = json.loads(
+        subprocess.check_output(
+            [
+                "gh",
+                "api",
+                "--paginate",
+                "--slurp",
+                f"repos/{repository}/actions/caches?per_page=100",
+            ],
+            text=True,
+            timeout=60,
+        )
+    )
+    caches = [cache for page in pages for cache in page["actions_caches"]]
+    for identifier in obsolete_caches(caches, key):
+        subprocess.run(
+            [
+                "gh",
+                "api",
+                "--method",
+                "DELETE",
+                f"repos/{repository}/actions/caches/{identifier}",
+            ],
+            check=True,
+            timeout=60,
+        )
+        LOGGER.info("Removed obsolete main cache %s", identifier)
+
+
+def main() -> None:
+    """Print a build identity or prune main caches after replacement."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    commands = parser.add_subparsers(dest="command", required=True)
+    revision = commands.add_parser("revision")
+    revision.add_argument("--ref", default="HEAD")
+    prune = commands.add_parser("prune")
+    prune.add_argument("--repository", required=True)
+    prune.add_argument("--key", required=True)
+    arguments = parser.parse_args()
+    logging.basicConfig(level=logging.INFO, format="cache: %(message)s")
+    if arguments.command == "revision":
+        print(build_revision(Path.cwd(), arguments.ref))
+    else:
+        prune_cache(arguments.repository, arguments.key)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/python/lean_pool/ci_validation_artifacts.py b/python/lean_pool/ci_validation_artifacts.py
new file mode 100644
index 0000000000..16d75c544e
--- /dev/null
+++ b/python/lean_pool/ci_validation_artifacts.py
@@ -0,0 +1,174 @@
+"""Recover successful validation receipts independently of large build caches."""
+
+from __future__ import annotations
+
+import argparse
+import json
+import logging
+import os
+import subprocess
+import tempfile
+import zipfile
+from pathlib import Path
+from urllib.parse import urlencode
+
+from lean_pool.ci_artifacts import github_json
+
+LOGGER = logging.getLogger(__name__)
+ARTIFACT = "lean-validation-receipts"
+MAXIMUM_BYTES = 32 * 1024 * 1024
+
+
+def receipts(data: bytes) -> dict:
+    """Read receipt metadata; the validation checker still verifies every hash."""
+    document = json.loads(data)
+    if document.get("version") != 1 or not isinstance(document.get("receipts"), dict):
+        raise ValueError("invalid validation receipt artifact")
+    return document["receipts"]
+
+
+def successful_pr_run(repository: str, number: int, head: str) -> int | None:
+    """Reuse only the latest successful Lean CI attempt for the merged PR head."""
+    query = urlencode({"event": "pull_request", "head_sha": head, "per_page": 100})
+    runs = github_json(
+        f"repos/{repository}/actions/workflows/lean_action_ci.yml/runs?{query}"
+    )["workflow_runs"]
+    matches = [
+        run
+        for run in runs
+        if run.get("head_sha") == head
+        and (
+            not run.get("pull_requests")
+            or any(pull.get("number") == number for pull in run["pull_requests"])
+        )
+    ]
+    latest = max(matches, key=lambda run: run["id"], default=None)
+    return latest["id"] if latest and latest.get("conclusion") == "success" else None
+
+
+def source_runs(
+    repository: str, event: str, head: str, has_cache: bool
+) -> list[tuple[int, bool]]:
+    """Promote merged PR passes on main; otherwise recover main's published passes."""
+    result = []
+    if event == "push":
+        for pull in github_json(f"repos/{repository}/commits/{head}/pulls"):
+            if (
+                pull.get("merged_at")
+                and pull.get("merge_commit_sha") == head
+                and pull.get("base", {}).get("ref") == "main"
+            ):
+                run = successful_pr_run(repository, pull["number"], pull["head"]["sha"])
+                if run is not None:
+                    result.append((run, True))
+    if not has_cache:
+        query = urlencode(
+            {"event": "push", "branch": "main", "status": "success", "per_page": 5}
+        )
+        runs = github_json(
+            f"repos/{repository}/actions/workflows/lean_action_ci.yml/runs?{query}"
+        )["workflow_runs"]
+        result.extend(
+            (run["id"], False)
+            for run in sorted(runs, key=lambda run: run["id"], reverse=True)
+            if run.get("conclusion") == "success" and run.get("head_branch") == "main"
+        )
+    return result
+
+
+def download_receipts(repository: str, run: int) -> dict | None:
+    """Read one bounded JSON member; never extract artifact paths into the checkout."""
+    artifacts = github_json(
+        f"repos/{repository}/actions/runs/{run}/artifacts?per_page=100"
+    )["artifacts"]
+    matches = [
+        item for item in artifacts if item["name"] == ARTIFACT and not item["expired"]
+    ]
+    if not matches:
+        return None
+    identifier = max(matches, key=lambda item: item["id"])["id"]
+    with tempfile.TemporaryDirectory(prefix="lean-validation-") as name:
+        archive = Path(name) / "receipts.zip"
+        with archive.open("wb") as output:
+            subprocess.run(
+                ["gh", "api", f"repos/{repository}/actions/artifacts/{identifier}/zip"],
+                stdout=output,
+                check=True,
+                timeout=60,
+            )
+        with zipfile.ZipFile(archive) as wrapper:
+            if wrapper.namelist() != ["passes.json"]:
+                raise ValueError("unexpected validation artifact members")
+            if wrapper.getinfo("passes.json").file_size > MAXIMUM_BYTES:
+                raise ValueError("validation artifact too large")
+            return receipts(wrapper.read("passes.json"))
+
+
+def restore_receipts(
+    root: Path, repository: str, event: str, head: str, *, previous_run: int = 0
+) -> bool:
+    """Missing artifacts leave normal validation intact; reuse never marks a pass."""
+    destination = root / ".lake/validation-cache/v1/passes.json"
+    try:
+        current = receipts(destination.read_bytes())
+    except (OSError, ValueError, AttributeError):
+        current = {}
+    candidates = (
+        [(previous_run, True)]
+        if previous_run
+        else source_runs(repository, event, head, bool(current))
+    )
+    for run, prefer in candidates:
+        try:
+            recovered = download_receipts(repository, run)
+            if recovered is None:
+                continue
+            combined = (current | recovered) if prefer else (recovered | current)
+            destination.parent.mkdir(parents=True, exist_ok=True)
+            temporary = destination.with_suffix(".tmp")
+            temporary.write_text(
+                json.dumps({"version": 1, "receipts": combined}) + "\n"
+            )
+            temporary.replace(destination)
+            LOGGER.info(
+                "Recovered %d saved check results from run %s", len(recovered), run
+            )
+            return True
+        except (
+            OSError,
+            ValueError,
+            AttributeError,
+            subprocess.SubprocessError,
+            zipfile.BadZipFile,
+        ):
+            LOGGER.exception(
+                "Could not read receipts from %s; regular checks remain", run
+            )
+    return False
+
+
+def main() -> None:
+    """Restore optional successful receipts before the standard validation steps."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument(
+        "--repository", default=os.environ.get("GITHUB_REPOSITORY"), required=False
+    )
+    parser.add_argument("--event", required=True)
+    parser.add_argument("--head", required=True)
+    parser.add_argument("--previous-run", type=int, default=0)
+    arguments = parser.parse_args()
+    logging.basicConfig(level=logging.INFO, format="validation-artifacts: %(message)s")
+    try:
+        restore_receipts(
+            Path.cwd(),
+            arguments.repository,
+            arguments.event,
+            arguments.head,
+            previous_run=arguments.previous_run,
+        )
+    except (OSError, ValueError, AttributeError, KeyError, subprocess.SubprocessError):
+        LOGGER.exception("Saved check results unavailable; running normal validation")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py
index cb06a211f0..343c569cbd 100644
--- a/python/lean_pool/quality.py
+++ b/python/lean_pool/quality.py
@@ -79,6 +79,22 @@
 FORBIDDEN_SOUNDNESS = re.compile(
     r"\b(?:axiom|constant|unsafe|partial|opaque)\b|@\[\s*extern\b"
 )
+FORBIDDEN_TEXT_RULES = (
+    (re.compile(r"\bset_option\b"), "set_option is forbidden"),
+    (re.compile(r"\bnolint\b"), "nolint waiver is forbidden"),
+    (FORBIDDEN_OPTION_APIS, "programmatic option manipulation is forbidden"),
+    (FORBIDDEN_OPTION_NAMES, "gated option name in code is forbidden"),
+    (
+        re.compile(r"^\s*(?:public\s+)?import\s+Mathlib\s*$"),
+        "broad import Mathlib is forbidden",
+    ),
+    (re.compile(r"\b(?:admit|sorry)\b"), None),
+    (FORBIDDEN_SOUNDNESS, "unchecked declaration is forbidden"),
+    (FORBIDDEN_DIAGNOSTICS, "diagnostic command is forbidden"),
+)
+FORBIDDEN_TEXT_CANDIDATES = re.compile(
+    "|".join(pattern.pattern for pattern, _ in FORBIDDEN_TEXT_RULES)
+)
 # Strict four-line header. Anchored at the start of the file, no extra lines
 # allowed inside the block: this forbids ad-hoc Source/MSC/Tags/Status fields
 # (those belong in projects.yml per CODE_QUALITY.md §7) and enforces the
@@ -91,6 +107,9 @@
     r"-/\n"
 )
 POOL_CODE_LINE_LIMIT = 10000
+LEAN_TEXT_TOKENS = re.compile(r'--|/-|"')
+LEAN_BLOCK_TOKENS = re.compile(r"/-|-/")
+LEAN_STRING_TOKENS = re.compile(r'\\[\s\S]|"')
 
 
 @dataclass(frozen=True)
@@ -116,66 +135,39 @@ class _Declaration:
 def _strip_lean_comments(text: str) -> str:
     result: list[str] = []
     index = 0
-    block_depth = 0
-    in_line_comment = False
-    in_string = False
-    escaped = False
-
-    while index < len(text):
-        char = text[index]
-        pair = text[index : index + 2]
-
-        if in_line_comment:
-            if char == "\n":
-                in_line_comment = False
-                result.append("\n")
-            else:
-                result.append(" ")
-            index += 1
-            continue
+    while match := LEAN_TEXT_TOKENS.search(text, index):
+        start = match.start()
+        result.append(text[index:start])
+        if match[0] == "--":
+            end = text.find("\n", match.end())
+            end = len(text) if end == -1 else end
+        elif match[0] == "/-":
+            end = _block_comment_end(text, match.end())
+        else:
+            end = _string_end(text, match.end())
+        # Preserve every character offset and newline for localized errors.
+        result.append(
+            "\n".join(" " * len(line) for line in text[start:end].split("\n"))
+        )
+        index = end
+    result.append(text[index:])
+    return "".join(result)
 
-        if block_depth > 0:
-            if pair == "/-":
-                block_depth += 1
-                result.append("  ")
-                index += 2
-            elif pair == "-/":
-                block_depth -= 1
-                result.append("  ")
-                index += 2
-            else:
-                result.append("\n" if char == "\n" else " ")
-                index += 1
-            continue
 
-        if in_string:
-            result.append("\n" if char == "\n" else " ")
-            if escaped:
-                escaped = False
-            elif char == "\\":
-                escaped = True
-            elif char == '"':
-                in_string = False
-            index += 1
-            continue
+def _block_comment_end(text: str, start: int) -> int:
+    depth = 1
+    for match in LEAN_BLOCK_TOKENS.finditer(text, start):
+        depth += 1 if match[0] == "/-" else -1
+        if depth == 0:
+            return match.end()
+    return len(text)
 
-        if pair == "--":
-            in_line_comment = True
-            result.append("  ")
-            index += 2
-        elif pair == "/-":
-            block_depth = 1
-            result.append("  ")
-            index += 2
-        elif char == '"':
-            in_string = True
-            result.append(" ")
-            index += 1
-        else:
-            result.append(char)
-            index += 1
 
-    return "".join(result)
+def _string_end(text: str, start: int) -> int:
+    for match in LEAN_STRING_TOKENS.finditer(text, start):
+        if match[0] == '"':
+            return match.end()
+    return len(text)
 
 
 def _line_number(text: str, offset: int) -> int:
@@ -277,41 +269,14 @@ def _forbidden_text_errors(path: Path) -> list[_QualityError]:
     errors: list[_QualityError] = []
     stripped = _strip_lean_comments(path.read_text())
     for line_number, line in enumerate(stripped.splitlines(), start=1):
-        if re.search(r"\bset_option\b", line):
-            errors.append(_QualityError(path, line_number, "set_option is forbidden"))
-        if re.search(r"\bnolint\b", line):
-            errors.append(
-                _QualityError(path, line_number, "nolint waiver is forbidden")
-            )
-        if FORBIDDEN_OPTION_APIS.search(line):
-            errors.append(
-                _QualityError(
-                    path,
-                    line_number,
-                    "programmatic option manipulation is forbidden",
-                )
-            )
-        if FORBIDDEN_OPTION_NAMES.search(line):
-            errors.append(
-                _QualityError(
-                    path,
-                    line_number,
-                    "gated option name in code is forbidden",
-                )
-            )
-        if re.match(r"^\s*(?:public\s+)?import\s+Mathlib\s*$", line):
-            errors.append(
-                _QualityError(path, line_number, "broad import Mathlib is forbidden")
-            )
-        errors.extend(_sorry_errors(path, line_number, line))
-        if FORBIDDEN_SOUNDNESS.search(line):
-            errors.append(
-                _QualityError(path, line_number, "unchecked declaration is forbidden")
-            )
-        if FORBIDDEN_DIAGNOSTICS.search(line):
-            errors.append(
-                _QualityError(path, line_number, "diagnostic command is forbidden")
-            )
+        if not FORBIDDEN_TEXT_CANDIDATES.search(line):
+            continue
+        for pattern, message in FORBIDDEN_TEXT_RULES:
+            if pattern.search(line):
+                if message is None:
+                    errors.extend(_sorry_errors(path, line_number, line))
+                else:
+                    errors.append(_QualityError(path, line_number, message))
     return errors
 
 
diff --git a/python/lean_pool/rebase_queue.py b/python/lean_pool/rebase_queue.py
new file mode 100644
index 0000000000..a693777496
--- /dev/null
+++ b/python/lean_pool/rebase_queue.py
@@ -0,0 +1,91 @@
+"""Refresh ready content PRs without interrupting their existing checks."""
+
+from __future__ import annotations
+
+import argparse
+import json
+import subprocess
+import sys
+from pathlib import Path
+from typing import Any
+
+
+def checks_finished(pull: dict[str, Any]) -> bool:
+    """Require observed checks to finish before replacing the checked revision."""
+    checks = pull.get("statusCheckRollup")
+    return bool(checks) and all(
+        check.get("status") == "COMPLETED"
+        or check.get("state") in {"SUCCESS", "FAILURE", "ERROR"}
+        for check in checks
+    )
+
+
+def select_pulls(pulls: list[dict[str, Any]], number: int = 0) -> list[dict[str, Any]]:
+    """Defer drafts and active CI; retain only PRs targeting the maintained main."""
+    result = []
+    for pull in pulls:
+        if (
+            (number and pull["number"] != number)
+            or pull.get("isDraft", True)
+            or pull.get("baseRefName") != "main"
+            or pull["headRefName"].startswith("bump/")
+            or any(label["name"] == "needs-manual-rebase" for label in pull["labels"])
+            or not checks_finished(pull)
+        ):
+            continue
+        result.append(
+            {
+                "number": pull["number"],
+                "branch": pull["headRefName"],
+                "head": pull["headRefOid"],
+                "repo": (
+                    f"{pull['headRepositoryOwner']['login']}/"
+                    f"{pull['headRepository']['name']}"
+                ),
+                "fork": pull["isCrossRepository"],
+            }
+        )
+    return result
+
+
+def content_only(root: Path, base: str, head: str) -> bool:
+    """Keep infrastructure branches stable while independent content merges."""
+    changed = subprocess.check_output(
+        ["git", "diff", "--name-only", "--no-renames", "-z", f"{base}...{head}"],
+        cwd=root,
+    ).split(b"\0")
+    paths = [path.decode() for path in changed if path]
+    return bool(paths) and all(
+        path in {"LeanPool.lean", "LeanPool/projects.yml"}
+        or (path.startswith("LeanPool/") and path.endswith(".lean"))
+        for path in paths
+    )
+
+
+def can_push(pull: dict[str, Any], expected_head: str) -> bool:
+    """Recheck races with an author's push or a newly started check."""
+    return (
+        pull.get("headRefOid") == expected_head
+        and not pull.get("isDraft", True)
+        and checks_finished(pull)
+    )
+
+
+def main() -> int:
+    """Select pending updates or check scope and state before publishing one."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("command", choices=("select", "content", "can-push"))
+    parser.add_argument("--number", type=int, default=0)
+    parser.add_argument("--base", default="origin/main")
+    parser.add_argument("--head", default="HEAD")
+    arguments = parser.parse_args()
+    if arguments.command == "select":
+        print(json.dumps(select_pulls(json.load(sys.stdin), arguments.number)))
+        return 0
+    if arguments.command == "content":
+        return 0 if content_only(Path.cwd(), arguments.base, arguments.head) else 1
+    return 0 if can_push(json.load(sys.stdin), arguments.head) else 1
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/python/lean_pool/validation_cache.py b/python/lean_pool/validation_cache.py
index 57392d1c82..6a36428e76 100644
--- a/python/lean_pool/validation_cache.py
+++ b/python/lean_pool/validation_cache.py
@@ -17,20 +17,28 @@
 from typing import Any
 
 LOGGER = logging.getLogger(__name__)
-GLOBAL_INPUTS = (
+SHARED_INPUTS = (
     "lean-toolchain",
     "lake-manifest.json",
     "lakefile.toml",
     "lakefile.lean",
-    "scripts/nolints.json",
-    "scripts/nolints-style.txt",
-    "scripts/ci/lint-project.lean",
-    "python/lean_pool/quality.py",
     "python/lean_pool/validation_cache.py",
     "python/pyproject.toml",
     "python/uv.lock",
     ".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")
+GLOBAL_INPUTS = SHARED_INPUTS + LINT_INPUTS + QUALITY_INPUTS
+
+
+def checker_inputs(kind: str | None) -> tuple[str, ...]:
+    """Track each check's implementation; unknown checks retain every input."""
+    if kind == "lint":
+        return SHARED_INPUTS + LINT_INPUTS
+    if kind in {"axioms", "backdoors", "declarations"}:
+        return SHARED_INPUTS + QUALITY_INPUTS
+    return GLOBAL_INPUTS
 
 
 def pool_units(root: Path) -> list[list[str]]:
@@ -45,25 +53,51 @@ def pool_units(root: Path) -> list[list[str]]:
     return [sorted(modules) for _, modules in sorted(units.items())]
 
 
-def source_inventory(root: Path, modules: list[str]) -> set[Path]:
+def _module_sources(
+    root: Path,
+    module: str,
+    imported_sources: dict[str, Path | None],
+    *,
+    discovered_sources: set[Path] | None = None,
+) -> set[Path]:
+    setup = root / (".lake/build/ir/" + module.replace(".", "/") + ".setup.json")
+    inventory = json.loads(setup.read_text())
+    if inventory["name"] != module or not isinstance(inventory["importArts"], dict):
+        raise ValueError("invalid compiler inventory")
+    paths = {root / (module.replace(".", "/") + ".lean")}
+    for imported in inventory["importArts"]:
+        if imported not in imported_sources:
+            path = root / (imported.replace(".", "/") + ".lean")
+            imported_sources[imported] = path if path.is_file() else None
+        path = imported_sources[imported]
+        if path is not None:
+            paths.add(path)
+            # Keep discoveries even if a later import makes this inventory fail.
+            if discovered_sources is not None:
+                discovered_sources.add(path)
+        elif imported.split(".")[0] == "LeanPool":
+            raise ValueError(f"missing imported source: {imported}")
+    return paths
+
+
+def source_inventory(
+    root: Path,
+    modules: list[str],
+    *,
+    inventories: dict[str, set[Path]] | None = None,
+    imported_sources: dict[str, Path | None] | None = None,
+) -> set[Path]:
     """Use every module's compiler inventory; fall back to all local Lean sources."""
     paths = {root / (module.replace(".", "/") + ".lean") for module in modules}
+    inventories = {} if inventories is None else inventories
+    imported_sources = {} if imported_sources is None else imported_sources
     try:
         for module in modules:
-            setup = root / (
-                ".lake/build/ir/" + module.replace(".", "/") + ".setup.json"
-            )
-            inventory = json.loads(setup.read_text())
-            if inventory["name"] != module or not isinstance(
-                inventory["importArts"], dict
-            ):
-                raise ValueError("invalid compiler inventory")
-            for imported in inventory["importArts"]:
-                path = root / (imported.replace(".", "/") + ".lean")
-                if path.is_file():
-                    paths.add(path)
-                elif imported.split(".")[0] == "LeanPool":
-                    raise ValueError(f"missing imported source: {imported}")
+            if module not in inventories:
+                inventories[module] = _module_sources(
+                    root, module, imported_sources, discovered_sources=paths
+                )
+            paths.update(inventories[module])
     except (OSError, ValueError, KeyError, TypeError):
         LOGGER.warning(
             "%s: missing import inventory; hashing all local sources", modules[0]
@@ -84,6 +118,13 @@ def __init__(self, root: Path, directory: Path, *, refresh: bool = False) -> Non
         self.directory = directory
         self.refresh = refresh
         self.digests: dict[Path, str] = {}
+        # Compilation finishes before validation; reuse inventories and path
+        # lookups only within this immutable checkout, never across CI runs.
+        self.inventories: dict[str, set[Path]] = {}
+        self.imported_sources: dict[str, Path | None] = {}
+        self.fingerprint_inputs: dict[
+            tuple[tuple[str, ...], tuple[str, ...]], dict[str, str]
+        ] = {}
         self.receipts: dict[str, dict[str, Any]] = {}
         self.used: dict[str, dict[str, Any]] = {}
         self.hits = 0
@@ -95,10 +136,33 @@ def __init__(self, root: Path, directory: Path, *, refresh: bool = False) -> Non
         except (OSError, ValueError, KeyError, TypeError):
             pass
 
-    def fingerprint(self, modules: list[str], metadata: Any = None) -> str:
+    def fingerprint(
+        self, modules: list[str], metadata: Any = None, *, kind: str | None = None
+    ) -> str:
         """Hash all checked inputs, retaining missing optional files in the key."""
-        paths = source_inventory(self.root, modules)
-        paths.update(self.root / name for name in GLOBAL_INPUTS)
+        global_inputs = checker_inputs(kind)
+        key = (tuple(modules), global_inputs)
+        if key not in self.fingerprint_inputs:
+            self.fingerprint_inputs[key] = self._fingerprint_inputs(
+                modules, global_inputs
+            )
+        payload = {
+            "inputs": self.fingerprint_inputs[key],
+            "modules": modules,
+            "metadata": metadata,
+        }
+        return hashlib.sha256(json.dumps(payload, sort_keys=True).encode()).hexdigest()
+
+    def _fingerprint_inputs(
+        self, modules: list[str], global_inputs: tuple[str, ...]
+    ) -> dict[str, str]:
+        paths = source_inventory(
+            self.root,
+            modules,
+            inventories=self.inventories,
+            imported_sources=self.imported_sources,
+        )
+        paths.update(self.root / name for name in global_inputs)
         inputs = {}
         for path in sorted(paths):
             if path not in self.digests:
@@ -108,8 +172,7 @@ def fingerprint(self, modules: list[str], metadata: Any = None) -> str:
                     else "missing"
                 )
             inputs[path.relative_to(self.root).as_posix()] = self.digests[path]
-        payload = {"inputs": inputs, "modules": modules, "metadata": metadata}
-        return hashlib.sha256(json.dumps(payload, sort_keys=True).encode()).hexdigest()
+        return inputs
 
     def check[T](
         self,
@@ -119,7 +182,7 @@ def check[T](
         metadata: Any = None,
     ) -> list[T]:
         """Run on a miss and retain only passes; failures never create receipts."""
-        digest = self.fingerprint(modules, metadata)
+        digest = self.fingerprint(modules, metadata, kind=kind)
         key = f"{kind}:{modules[0]}"
         expected = {"fingerprint": digest, "modules": modules, "passed": True}
         if not self.refresh and self.receipts.get(key) == expected:
@@ -169,8 +232,6 @@ def validate() -> list[str]:
 
 def main() -> int:
     """Run the cached declaration linter or repository quality checker."""
-    from lean_pool.quality import run_checks
-
     parser = argparse.ArgumentParser(description=__doc__)
     parser.add_argument("check", choices=("lint", "quality"))
     parser.add_argument("--repo", type=Path, default=Path.cwd())
@@ -190,6 +251,8 @@ def main() -> int:
         } | cache.used
         errors = []
     else:
+        from lean_pool.quality import run_checks
+
         errors = run_checks(root, validation_cache=cache)
         cache.used |= {
             key: receipt
diff --git a/python/tests/test_ci_artifacts.py b/python/tests/test_ci_artifacts.py
index 30a739d807..b6b463b7bf 100644
--- a/python/tests/test_ci_artifacts.py
+++ b/python/tests/test_ci_artifacts.py
@@ -6,6 +6,7 @@
 import json
 import subprocess
 import tarfile
+import zipfile
 from pathlib import Path
 
 import pytest
@@ -126,6 +127,23 @@ def test_missing_run_falls_back(repository: Path, monkeypatch) -> None:
     assert not ci_artifacts.reuse_build(repository, "owner/repo", "head", "push", 0)
 
 
+def test_pull_request_does_not_wait_for_unpublished_build(
+    repository: Path, monkeypatch
+):
+    """PR producers omit full build artifacts, so consumers use Lake immediately."""
+
+    def unexpected_query(*args):
+        pytest.fail("PR build reuse must not query or wait for an unpublished artifact")
+
+    monkeypatch.setattr(ci_artifacts, "github_json", unexpected_query)
+    output = repository / ".lake/build/lib/lean/LeanPool.olean"
+    before = output.read_bytes()
+    assert not ci_artifacts.reuse_build(
+        repository, "owner/repo", "head", "pull_request", 7200
+    )
+    assert output.read_bytes() == before
+
+
 def test_api_error_falls_back(repository: Path, monkeypatch) -> None:
     """Artifact API errors are an optimization miss rather than a docs failure."""
 
@@ -171,3 +189,87 @@ def response(endpoint):
 
     monkeypatch.setattr(ci_artifacts, "github_json", response)
     assert ci_artifacts.wait_for_artifact("owner/repo", {"id": 1}, 0) == 8
+
+
+@pytest.mark.parametrize("extension", ["gz", "zst"])
+def test_streamed_build_replaces_directory_without_copying(
+    repository: Path, monkeypatch, extension: str
+) -> None:
+    """Both compression formats restore all files without a second directory copy."""
+    archive = repository / f"build.tar.{extension}"
+    output = repository / ".lake/build/lib/lean/LeanPool.olean"
+    ci_artifacts.pack_build(repository, archive)
+    output.write_bytes(b"old")
+    monkeypatch.setattr(
+        ci_artifacts.shutil,
+        "copytree",
+        lambda *args, **kwargs: pytest.fail("unexpected second build copy"),
+    )
+    assert ci_artifacts.restore_build(repository, archive)
+    assert output.read_bytes() == b"compiled"
+
+
+@pytest.mark.parametrize("extension", ["gz", "zst"])
+def test_truncated_compression_preserves_current_build(
+    repository: Path, extension: str
+) -> None:
+    """Reject incomplete compressed files before installing the staged build."""
+    archive = repository / f"build.tar.{extension}"
+    ci_artifacts.pack_build(repository, archive)
+    archive.write_bytes(archive.read_bytes()[:-8])
+    output = repository / ".lake/build/lib/lean/LeanPool.olean"
+    output.write_bytes(b"original build")
+    with pytest.raises((subprocess.SubprocessError, tarfile.TarError, EOFError)):
+        ci_artifacts.restore_build(repository, archive)
+    assert output.read_bytes() == b"original build"
+    assert not list((repository / ".lake").glob("lean-ci-build-*"))
+
+
+def test_invalid_member_after_valid_output_preserves_current_build(repository: Path):
+    """A later invalid path cannot install an otherwise valid partial build."""
+    destination = repository / "build.tar.gz"
+    with tarfile.open(destination, "w:gz") as archive:
+        for name, payload in (
+            (
+                ci_artifacts.MANIFEST_NAME,
+                json.dumps(ci_artifacts.build_identity(repository)).encode(),
+            ),
+            (".lake/build/lib/lean/LeanPool.olean", b"replacement"),
+            ("../escape", b"invalid"),
+        ):
+            member = tarfile.TarInfo(name)
+            member.size = len(payload)
+            archive.addfile(member, io.BytesIO(payload))
+    with pytest.raises(ValueError, match="Unexpected build archive member"):
+        ci_artifacts.restore_build(repository, destination)
+    assert (
+        repository / ".lake/build/lib/lean/LeanPool.olean"
+    ).read_bytes() == b"compiled"
+
+
+@pytest.mark.parametrize(
+    "name", [ci_artifacts.ARCHIVE_NAME, ci_artifacts.LEGACY_ARCHIVE_NAME]
+)
+def test_download_accepts_current_and_previous_compression(
+    repository: Path, monkeypatch, name: str
+) -> None:
+    """Documentation can consume builds produced on either side of the rollout."""
+    archive = repository / name
+    ci_artifacts.pack_build(repository, archive)
+    zipped = io.BytesIO()
+    with zipfile.ZipFile(zipped, "w") as bundle:
+        bundle.write(archive, arcname=name)
+    output = repository / ".lake/build/lib/lean/LeanPool.olean"
+    output.write_bytes(b"old")
+
+    original_run = subprocess.run
+
+    def download(command, *, stdout, **kwargs):
+        if command[0] != "gh":
+            return original_run(command, stdout=stdout, **kwargs)
+        assert command == ["gh", "api", "repos/owner/repo/actions/artifacts/7/zip"]
+        stdout.write(zipped.getvalue())
+
+    monkeypatch.setattr(subprocess, "run", download)
+    assert ci_artifacts.download_build(repository, "owner/repo", 7)
+    assert output.read_bytes() == b"compiled"
diff --git a/python/tests/test_ci_cache.py b/python/tests/test_ci_cache.py
new file mode 100644
index 0000000000..5aad24ab84
--- /dev/null
+++ b/python/tests/test_ci_cache.py
@@ -0,0 +1,184 @@
+"""Check source-based build reuse and narrowly scoped cache replacement."""
+
+from __future__ import annotations
+
+import json
+import subprocess
+from pathlib import Path
+
+import pytest
+
+from lean_pool.ci_cache import build_revision, obsolete_caches, prune_cache
+
+
+def _commit(root: Path) -> None:
+    subprocess.run(["git", "add", "."], cwd=root, check=True)
+    subprocess.run(
+        [
+            "git",
+            "-c",
+            "user.name=Test",
+            "-c",
+            "user.email=test@example.com",
+            "commit",
+            "-qm",
+            "change",
+        ],
+        cwd=root,
+        check=True,
+    )
+
+
+@pytest.fixture
+def repository(tmp_path: Path) -> Path:
+    """Commit Lean sources alongside unrelated Python and documentation files."""
+    subprocess.run(["git", "init", "-q"], cwd=tmp_path, check=True)
+    for name in ("LeanPool.lean", "LeanPool/A.lean", "scripts/ProjectIndexes.lean"):
+        path = tmp_path / name
+        path.parent.mkdir(parents=True, exist_ok=True)
+        path.write_text("module\n")
+    (tmp_path / "README.md").write_text("Documentation\n")
+    _commit(tmp_path)
+    return tmp_path
+
+
+def test_unrelated_commit_reuses_build_identity(repository: Path) -> None:
+    """A different commit with the same Lean sources needs no new build upload."""
+    before = build_revision(repository)
+    (repository / "README.md").write_text("New documentation\n")
+    _commit(repository)
+    assert build_revision(repository) == before
+    assert build_revision(repository, "HEAD^") == before
+
+
+@pytest.mark.parametrize(
+    "name",
+    [
+        "scripts/exposition/Extract.lean",
+        "scripts/ci/lint-project.lean",
+        "scripts/profile.py",
+        "LeanPool/projects.yml",
+        "LeanPool/A/LICENSE",
+    ],
+)
+def test_unrelated_file_reuses_compiled_build(repository: Path, name: str) -> None:
+    """Scripts, project cards, and licenses do not change the pool's compilation."""
+    before = build_revision(repository)
+    path = repository / name
+    path.parent.mkdir(parents=True, exist_ok=True)
+    path.write_text("changed script\n")
+    _commit(repository)
+    assert build_revision(repository) == before
+
+
+@pytest.mark.parametrize(
+    "name", ["LeanPool.lean", "LeanPool/A.lean", "scripts/ProjectIndexes.lean"]
+)
+def test_source_change_gets_new_build_identity(repository: Path, name: str) -> None:
+    """Pool sources and the index generator each invalidate compiled reuse."""
+    before = build_revision(repository)
+    (repository / name).write_text("module\n-- change\n")
+    _commit(repository)
+    assert build_revision(repository) != before
+    assert build_revision(repository, "HEAD^") == before
+
+
+def test_source_addition_and_deletion_change_identity(repository: Path) -> None:
+    """Changes to the module inventory count, not just edits to existing files."""
+    before = build_revision(repository)
+    (repository / "LeanPool/B.lean").write_text("module\n")
+    _commit(repository)
+    assert build_revision(repository) != before
+    (repository / "LeanPool/B.lean").unlink()
+    _commit(repository)
+    assert build_revision(repository) == before
+
+
+def test_retention_preserves_other_cache_kinds_platforms_and_prs() -> None:
+    """Pruning one build family cannot discard validation or dependency results."""
+    keys = [
+        ("LeanPoolBuild-v1-Linux-old", "refs/heads/main"),
+        ("LeanPoolBuild-v1-Linux-current", "refs/heads/main"),
+        ("LeanPoolBuild-v1-Windows-old", "refs/heads/main"),
+        ("LeanPoolBuild-v1-Linux-old", "refs/pull/1/merge"),
+        ("LeanValidation-v1-Linux-old", "refs/heads/main"),
+        ("LeanDependencies-v1-Linux-old", "refs/heads/main"),
+    ]
+    caches = [
+        {"id": index, "key": key, "ref": reference}
+        for index, (key, reference) in enumerate(keys)
+    ]
+    assert obsolete_caches(caches, "LeanPoolBuild-v1-Linux-current") == [0]
+
+
+def test_prune_reads_all_pages_and_only_deletes_obsolete_main_entries(
+    monkeypatch,
+) -> None:
+    """A confirmed replacement frees space without deleting unrelated caches."""
+    pages = [
+        {
+            "actions_caches": [
+                {"id": 7, "key": "LeanPoolBuild-v1-Linux-old", "ref": "refs/heads/main"}
+            ]
+        },
+        {
+            "actions_caches": [
+                {
+                    "id": 9,
+                    "key": "LeanPoolBuild-v1-Linux-new",
+                    "ref": "refs/heads/main",
+                },
+                {
+                    "id": 8,
+                    "key": "LeanValidation-v1-Linux-new",
+                    "ref": "refs/heads/main",
+                },
+            ]
+        },
+    ]
+
+    calls = []
+    monkeypatch.setattr(
+        subprocess, "check_output", lambda *args, **kwargs: json.dumps(pages)
+    )
+    monkeypatch.setattr(
+        subprocess, "run", lambda command, **kwargs: calls.append(command)
+    )
+    prune_cache("owner/repo", "LeanPoolBuild-v1-Linux-new")
+    assert calls == [
+        ["gh", "api", "--method", "DELETE", "repos/owner/repo/actions/caches/7"]
+    ]
+
+
+def test_failed_or_missing_replacement_preserves_previous_copy() -> None:
+    """An upload failure, or a replacement visible only to a PR, cannot erase main."""
+    caches = [
+        {"id": 1, "key": "LeanPoolBuild-v1-Linux-old", "ref": "refs/heads/main"},
+        {"id": 2, "key": "LeanPoolBuild-v1-Linux-new", "ref": "refs/pull/1/merge"},
+    ]
+    assert obsolete_caches(caches, "LeanPoolBuild-v1-Linux-new") == []
+
+
+def test_older_run_cannot_delete_a_newer_run_cache() -> None:
+    """Overlapping jobs may prune predecessors but never a newer replacement."""
+    caches = [
+        {
+            "id": index,
+            "key": f"LeanPoolBuild-v1-Linux-{index}",
+            "ref": "refs/heads/main",
+            "created_at": f"2026-10-06T07:0{index}:00Z",
+        }
+        for index in range(3)
+    ]
+    assert obsolete_caches(caches, "LeanPoolBuild-v1-Linux-1") == [0]
+
+
+def test_unknown_cache_family_is_rejected_before_api_calls(monkeypatch) -> None:
+    """An accidental broad cache key must not delete unrelated saved data."""
+    monkeypatch.setattr(
+        subprocess,
+        "check_output",
+        lambda *args, **kwargs: pytest.fail("unexpected API call"),
+    )
+    with pytest.raises(ValueError, match="unsupported cache key"):
+        prune_cache("owner/repo", "unknown")
diff --git a/python/tests/test_ci_validation_artifacts.py b/python/tests/test_ci_validation_artifacts.py
new file mode 100644
index 0000000000..72f8f8cebe
--- /dev/null
+++ b/python/tests/test_ci_validation_artifacts.py
@@ -0,0 +1,208 @@
+"""Recover saved checks without trusting them for changed sources or failed runs."""
+
+from __future__ import annotations
+
+import io
+import json
+import subprocess
+import sys
+import zipfile
+from pathlib import Path
+
+import pytest
+
+from lean_pool import ci_validation_artifacts as artifacts
+from lean_pool.validation_cache import ValidationCache
+
+
+def _archive(monkeypatch, members: dict[str, bytes]) -> None:
+    payload = io.BytesIO()
+    with zipfile.ZipFile(payload, "w") as wrapper:
+        for name, contents in members.items():
+            wrapper.writestr(name, contents)
+    monkeypatch.setattr(
+        artifacts,
+        "github_json",
+        lambda _: {
+            "artifacts": [{"id": 8, "name": artifacts.ARTIFACT, "expired": False}]
+        },
+    )
+
+    def download(command, *, stdout, **kwargs):
+        assert command[-1].endswith("/artifacts/8/zip")
+        stdout.write(payload.getvalue())
+
+    monkeypatch.setattr(artifacts.subprocess, "run", download)
+
+
+def test_recovered_passes_still_recheck_changed_sources(tmp_path: Path, monkeypatch):
+    """Transporting a real pass receipt cannot bypass its original dependency checks."""
+    source = tmp_path / "LeanPool/A.lean"
+    source.parent.mkdir()
+    source.write_text("def a := 1\n")
+    inventory = tmp_path / ".lake/build/ir/LeanPool/A.setup.json"
+    inventory.parent.mkdir(parents=True)
+    inventory.write_text(json.dumps({"name": "LeanPool.A", "importArts": {}}))
+    directory = tmp_path / ".lake/validation-cache/v1"
+    cache = ValidationCache(tmp_path, directory)
+    assert cache.check("lint", ["LeanPool.A"], lambda: []) == []
+    cache.save()
+    saved = (directory / "passes.json").read_bytes()
+    (directory / "passes.json").unlink()
+    _archive(monkeypatch, {"passes.json": saved})
+    monkeypatch.setattr(artifacts, "source_runs", lambda *args: [(1, False)])
+    assert artifacts.restore_receipts(tmp_path, "owner/repo", "pull_request", "head")
+    cache = ValidationCache(tmp_path, directory)
+    assert cache.check("lint", ["LeanPool.A"], lambda: ["unexpected recheck"]) == []
+    source.write_text("def a := 2\n")
+    cache = ValidationCache(tmp_path, directory)
+    assert cache.check("lint", ["LeanPool.A"], lambda: ["must recheck"]) == [
+        "must recheck"
+    ]
+
+
+@pytest.mark.parametrize("prefer, expected", [(True, "new"), (False, "old")])
+def test_promoted_pr_passes_replace_old_main_results(
+    tmp_path, monkeypatch, prefer, expected
+):
+    """Main uses a merged PR's newer results; fallback preserves existing PR results."""
+    destination = tmp_path / ".lake/validation-cache/v1/passes.json"
+    destination.parent.mkdir(parents=True)
+    destination.write_text(json.dumps({"version": 1, "receipts": {"check": "old"}}))
+    _archive(
+        monkeypatch,
+        {
+            "passes.json": json.dumps(
+                {"version": 1, "receipts": {"check": "new"}}
+            ).encode()
+        },
+    )
+    monkeypatch.setattr(artifacts, "source_runs", lambda *args: [(1, prefer)])
+    assert artifacts.restore_receipts(tmp_path, "owner/repo", "push", "head")
+    assert json.loads(destination.read_text())["receipts"]["check"] == expected
+
+
+def test_warm_pr_does_not_query_artifact_api(monkeypatch):
+    """Normal cached PRs need no extra metadata requests or downloads."""
+    monkeypatch.setattr(
+        artifacts, "github_json", lambda _: pytest.fail("unexpected API request")
+    )
+    assert artifacts.source_runs("owner/repo", "pull_request", "head", True) == []
+
+
+def test_verified_rebase_carries_prior_results_without_run_search(
+    tmp_path, monkeypatch
+):
+    """The existing rebase eligibility check supplies its exact successful run."""
+    _archive(monkeypatch, {"passes.json": b'{"version": 1, "receipts": {"prior": {}}}'})
+    monkeypatch.setattr(
+        artifacts, "source_runs", lambda *args: pytest.fail("unexpected run search")
+    )
+    assert artifacts.restore_receipts(
+        tmp_path, "owner/repo", "pull_request", "head", previous_run=42
+    )
+    saved = tmp_path / ".lake/validation-cache/v1/passes.json"
+    assert json.loads(saved.read_text())["receipts"] == {"prior": {}}
+
+
+def test_only_associated_merged_main_pull_is_promoted(monkeypatch):
+    """An open PR, different merge commit, or migration branch is not a source."""
+    valid = {
+        "number": 42,
+        "merged_at": "now",
+        "merge_commit_sha": "merge",
+        "base": {"ref": "main"},
+        "head": {"sha": "head"},
+    }
+
+    def response(endpoint):
+        if endpoint.endswith("/commits/merge/pulls"):
+            return [
+                valid | {"merged_at": None},
+                valid | {"merge_commit_sha": "other"},
+                valid | {"base": {"ref": "bump/v4"}},
+                valid,
+            ]
+        assert "head_sha=head" in endpoint
+        return {
+            "workflow_runs": [
+                {
+                    "id": 8,
+                    "head_sha": "head",
+                    "pull_requests": [],
+                    "conclusion": "success",
+                }
+            ]
+        }
+
+    monkeypatch.setattr(artifacts, "github_json", response)
+    assert artifacts.source_runs("owner/repo", "push", "merge", True) == [(8, True)]
+
+
+def test_failed_latest_attempt_blocks_older_pass_promotion(monkeypatch):
+    """A rerun failure cannot be hidden by an older successful attempt."""
+    runs = [
+        {"id": 8, "head_sha": "head", "conclusion": "success"},
+        {"id": 9, "head_sha": "head", "conclusion": "failure"},
+    ]
+    monkeypatch.setattr(artifacts, "github_json", lambda _: {"workflow_runs": runs})
+    assert artifacts.successful_pr_run("owner/repo", 42, "head") is None
+
+
+def test_missing_cache_uses_only_successful_main_runs(monkeypatch):
+    """Sibling PR artifacts are never selected as default-branch results."""
+    runs = [
+        {"id": 7, "head_branch": "main", "conclusion": "success"},
+        {"id": 8, "head_branch": "main", "conclusion": "success"},
+        {"id": 9, "head_branch": "feature", "conclusion": "success"},
+        {"id": 10, "head_branch": "main", "conclusion": "failure"},
+    ]
+    monkeypatch.setattr(artifacts, "github_json", lambda _: {"workflow_runs": runs})
+    assert artifacts.source_runs("owner/repo", "pull_request", "head", False) == [
+        (8, False),
+        (7, False),
+    ]
+
+
+@pytest.mark.parametrize(
+    "members",
+    [
+        {"../passes.json": b"{}"},
+        {"passes.json": b"broken"},
+        {"passes.json": b'{"version": 2, "receipts": {}}'},
+        {"passes.json": b'{"version": 1, "receipts": []}'},
+    ],
+)
+def test_bad_download_preserves_existing_receipts(tmp_path, monkeypatch, members):
+    """Rejected artifacts do not discard existing passes or alter build files."""
+    destination = tmp_path / ".lake/validation-cache/v1/passes.json"
+    destination.parent.mkdir(parents=True)
+    existing = b'{"version": 1, "receipts": {"old": {}}}'
+    destination.write_bytes(existing)
+    _archive(monkeypatch, members)
+    monkeypatch.setattr(artifacts, "source_runs", lambda *args: [(1, True)])
+    assert not artifacts.restore_receipts(tmp_path, "owner/repo", "push", "head")
+    assert destination.read_bytes() == existing
+
+
+def test_oversized_receipts_are_rejected(monkeypatch):
+    """Unexpectedly large content never becomes a validation input file."""
+    _archive(monkeypatch, {"passes.json": b'{"version": 1, "receipts": {}}'})
+    monkeypatch.setattr(artifacts, "MAXIMUM_BYTES", 1)
+    with pytest.raises(ValueError, match="too large"):
+        artifacts.download_receipts("owner/repo", 1)
+
+
+def test_api_limit_keeps_standard_validation_path(monkeypatch):
+    """A transient API problem is a reuse miss rather than a new gate failure."""
+    monkeypatch.setattr(
+        sys,
+        "argv",
+        ["receipts", "--repository", "owner/repo", "--event", "push", "--head", "head"],
+    )
+
+    def unavailable(*args):
+        raise subprocess.CalledProcessError(1, "gh")
+
+    monkeypatch.setattr(artifacts, "source_runs", unavailable)
+    artifacts.main()
diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py
index 95bdce124e..2952565a56 100644
--- a/python/tests/test_quality.py
+++ b/python/tests/test_quality.py
@@ -92,6 +92,27 @@ def test_strip_lean_comments_preserves_code_not_comments() -> None:
     assert "def safe := 1" in stripped
 
 
+@pytest.mark.parametrize(
+    ("text", "expected"),
+    [
+        ("α /- outer /- sorry -/ end -/ β", "α " + " " * 27 + " β"),
+        ('"a\\"sorry" def safe := 1', " " * 10 + " def safe := 1"),
+        ('"a\\\\"sorry', " " * 5 + "sorry"),
+        ('"α\nβ"\ndef safe := 1', "  \n  \ndef safe := 1"),
+        ("-- sorry\r\ndef safe := 1", " " * 9 + "\ndef safe := 1"),
+        ("/- α\n/- nested -/", " " * 4 + "\n" + " " * 12),
+        ('"unfinished\\', " " * 12),
+        ("def safe := 1 -- sorry", "def safe := 1 " + " " * 8),
+    ],
+)
+def test_strip_comments_preserves_offsets_with_nested_and_escaped_tokens(
+    text: str, expected: str
+) -> None:
+    """Nested comments, escapes, and unfinished tokens retain diagnostic locations."""
+    assert _strip_lean_comments(text) == expected
+    assert len(expected) == len(text)
+
+
 def test_minimal_repo_passes_static_quality_checks(tmp_path: Path) -> None:
     """A compliant minimal repo passes without invoking Lean."""
     _write_minimal_repo(tmp_path)
diff --git a/python/tests/test_rebase_queue.py b/python/tests/test_rebase_queue.py
new file mode 100644
index 0000000000..598ef844be
--- /dev/null
+++ b/python/tests/test_rebase_queue.py
@@ -0,0 +1,102 @@
+"""Keep branch updates from cancelling active CI or changing infrastructure PRs."""
+
+from __future__ import annotations
+
+import subprocess
+from pathlib import Path
+
+import pytest
+
+from lean_pool.rebase_queue import can_push, content_only, select_pulls
+
+
+@pytest.fixture
+def pull() -> dict:
+    """A ready content PR whose existing checks have completed."""
+    return {
+        "number": 42,
+        "isDraft": False,
+        "baseRefName": "main",
+        "headRefName": "feature/project",
+        "headRefOid": "a" * 40,
+        "headRepositoryOwner": {"login": "owner"},
+        "headRepository": {"name": "repo"},
+        "isCrossRepository": False,
+        "labels": [],
+        "statusCheckRollup": [{"status": "COMPLETED", "conclusion": "SUCCESS"}],
+    }
+
+
+@pytest.mark.parametrize(
+    "changes",
+    [
+        {"isDraft": True},
+        {"baseRefName": "bump/v4"},
+        {"headRefName": "bump/v4"},
+        {"labels": [{"name": "needs-manual-rebase"}]},
+        {"statusCheckRollup": []},
+        {"statusCheckRollup": None},
+        {"statusCheckRollup": [{"status": "QUEUED"}]},
+        {"statusCheckRollup": [{"status": "IN_PROGRESS"}]},
+        {"statusCheckRollup": [{"state": "PENDING"}]},
+        {"statusCheckRollup": [{}]},
+    ],
+)
+def test_busy_or_ineligible_pulls_are_deferred(pull: dict, changes: dict) -> None:
+    """An update must not interrupt CI, a draft, or a manual/migration branch."""
+    assert select_pulls([pull | changes]) == []
+
+
+def test_ready_pull_is_selected_and_completion_targets_one_pull(pull: dict) -> None:
+    """CI completion wakes only the finished PR, preserving other branches."""
+    other = pull | {"number": 43}
+    assert [item["number"] for item in select_pulls([pull, other], 42)] == [42]
+    assert [item["number"] for item in select_pulls([pull, other])] == [42, 43]
+    assert select_pulls([pull])[0]["head"] == "a" * 40
+
+
+def test_completed_failure_can_receive_main_fixes(pull: dict) -> None:
+    """Failed CI stays a merge blocker but may benefit from a newer main."""
+    pull["statusCheckRollup"] = [{"state": "FAILURE"}]
+    assert len(select_pulls([pull])) == 1
+
+
+def test_author_or_check_races_prevent_publication(pull: dict) -> None:
+    """Recheck both the remote revision and active checks before pushing."""
+    assert can_push(pull, "a" * 40)
+    assert not can_push(pull, "b" * 40)
+    assert not can_push(pull | {"isDraft": True}, "a" * 40)
+    pull["statusCheckRollup"].append({"status": "IN_PROGRESS"})
+    assert not can_push(pull, "a" * 40)
+
+
+@pytest.mark.parametrize("path", ["LeanPool/A.lean", "README.md", "python/tool.py"])
+def test_only_content_branches_are_automatically_updated(tmp_path: Path, path: str):
+    """Infrastructure PRs stay stable when unrelated projects merge."""
+    subprocess.run(["git", "init", "-q", "-b", "main"], cwd=tmp_path, check=True)
+    (tmp_path / "LeanPool.lean").write_text("import LeanPool.A\n")
+    _commit(tmp_path)
+    subprocess.run(["git", "checkout", "-qb", "feature"], cwd=tmp_path, check=True)
+    target = tmp_path / path
+    target.parent.mkdir(parents=True, exist_ok=True)
+    target.write_text("change\n")
+    _commit(tmp_path)
+    assert content_only(tmp_path, "main", "HEAD") == path.startswith("LeanPool/")
+
+
+def _commit(root: Path) -> None:
+    subprocess.run(["git", "add", "."], cwd=root, check=True)
+    subprocess.run(
+        [
+            "git",
+            "-c",
+            "user.name=Test",
+            "-c",
+            "user.email=test@example.com",
+            "commit",
+            "-qm",
+            "change",
+        ],
+        cwd=root,
+        check=True,
+    )
diff --git a/python/tests/test_validation_cache.py b/python/tests/test_validation_cache.py
index 8443354c1d..9756c435bc 100644
--- a/python/tests/test_validation_cache.py
+++ b/python/tests/test_validation_cache.py
@@ -9,7 +9,13 @@
 import pytest
 
 from lean_pool.quality import _cached_pool_audits
-from lean_pool.validation_cache import GLOBAL_INPUTS, ValidationCache, pool_units
+from lean_pool.validation_cache import (
+    GLOBAL_INPUTS,
+    ValidationCache,
+    _module_sources,
+    pool_units,
+    source_inventory,
+)
 
 
 def _inventory(root: Path, module: str, imports: tuple[str, ...] = ()) -> None:
@@ -80,13 +86,62 @@ def test_transitive_import_of_nested_module_invalidates_consumer(
 
 
 @pytest.mark.parametrize("name", GLOBAL_INPUTS)
-def test_checker_and_dependency_changes_invalidate_all(
+def test_checker_edits_invalidate_only_dependent_checks(
     repository: Path, name: str
 ) -> None:
-    """Toolchain, dependencies, lint options, and checker implementations are inputs."""
-    _run(repository)
+    """Unrelated tooling edits preserve passes; shared inputs invalidate all kinds."""
+    kinds = ("lint", "axioms", "backdoors", "declarations", "future-check")
+    directory = repository / ".lake/validation-cache/v1"
+    cache = ValidationCache(repository, directory)
+    for kind in kinds:
+        for modules in pool_units(repository):
+            cache.check(kind, modules, lambda: [])
+    cache.save()
     (repository / name).write_text("changed\n")
-    assert len(_run(repository)[1]) == 3
+    cache = ValidationCache(repository, directory)
+    calls: list[tuple[str, str]] = []
+    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"}:
+        fresh_kinds = ("axioms", "backdoors", "declarations", "future-check")
+    elif name in {"scripts/ci/lint-project.lean", "scripts/nolints.json"}:
+        fresh_kinds = ("lint", "future-check")
+    else:
+        fresh_kinds = kinds
+    assert calls == [
+        (kind, modules[0]) for kind in fresh_kinds for modules in pool_units(repository)
+    ]
+    assert len(calls) >= 3
+
+
+@pytest.mark.parametrize("kind", ("lint", "axioms", "backdoors", "declarations"))
+def test_source_changes_invalidate_every_check_kind(
+    repository: Path, kind: str
+) -> None:
+    """Scoping checker inputs must preserve all imported-source dependencies."""
+    directory = repository / ".lake/validation-cache/v1"
+    cache = ValidationCache(repository, directory)
+    for modules in pool_units(repository):
+        cache.check(kind, modules, lambda: [])
+    cache.save()
+    (repository / "LeanPool/A/Detail.lean").write_text("-- changed\n")
+    cache = ValidationCache(repository, directory)
+    calls: list[str] = []
+    for modules in pool_units(repository):
+        cache.check(kind, modules, lambda: calls.append(modules[0]) or [])
+    assert calls == ["LeanPool.A", "LeanPool"]
+
+
+def test_quality_check_kinds_reuse_source_comparisons(repository: Path) -> None:
+    """Quality checks sharing dependencies calculate their input list once."""
+    cache = ValidationCache(repository, repository / ".lake/validation-cache/v1")
+    with patch.object(
+        cache, "_fingerprint_inputs", wraps=cache._fingerprint_inputs
+    ) as inputs:
+        for kind in ("axioms", "backdoors", "declarations"):
+            cache.check(kind, ["LeanPool.A"], lambda: [])
+        assert inputs.call_count == 1
 
 
 @pytest.mark.parametrize("contents", [None, "{", "{}", '{"name": "wrong"}'])
@@ -156,3 +211,79 @@ def test_quality_audits_cover_every_owned_module(repository: Path) -> None:
         cache = ValidationCache(repository, cache.directory)
         assert _cached_pool_audits(repository, cache) == []
         assert axioms.call_count == backdoors.call_count == 3
+
+
+def test_overlapping_checks_reuse_inventories_without_changing_fingerprints(
+    repository: Path,
+) -> None:
+    """Shared imports are resolved once, while metadata still changes the key."""
+    _inventory(repository, "LeanPool.A", ("LeanPool.A.Detail", "Mathlib.Shared"))
+    _inventory(repository, "LeanPool.A.Detail", ("Mathlib.Shared",))
+    cache = ValidationCache(repository, repository / ".lake/validation-cache/v1")
+    groups = [["LeanPool.A"], ["LeanPool.A", "LeanPool.A.Detail"]]
+    checks = [
+        (modules, metadata)
+        for modules in groups
+        for metadata in (None, {"main_declarations": ["a"]})
+    ]
+    expected = [
+        ValidationCache(repository, cache.directory).fingerprint(modules, metadata)
+        for modules, metadata in checks
+    ]
+    with patch(
+        "lean_pool.validation_cache._module_sources",
+        wraps=_module_sources,
+    ) as inventories:
+        assert [
+            cache.fingerprint(modules, metadata) for modules, metadata in checks
+        ] == expected
+        assert inventories.call_count == 2
+    assert expected[0] != expected[1]
+    assert cache.imported_sources["Mathlib.Shared"] is None
+    assert (
+        source_inventory(repository, groups[1])
+        == cache.inventories["LeanPool.A"] | cache.inventories["LeanPool.A.Detail"]
+    )
+
+
+def test_local_import_outside_pool_invalidates_cached_checks(repository: Path) -> None:
+    """Memoized import lookups still cover local modules outside LeanPool."""
+    source = repository / "Support.lean"
+    source.write_text("def support := 1\n")
+    _inventory(repository, "LeanPool.A.Detail", ("Support",))
+    _run(repository)
+    source.write_text("def support := 2\n")
+    assert _run(repository)[1] == ["LeanPool.A"]
+
+
+def test_missing_pool_import_falls_back_after_memoized_lookup(repository: Path) -> None:
+    """A cached missing path cannot hide a missing imported pool source."""
+    _inventory(repository, "LeanPool.A", ("LeanPool.Missing",))
+    _inventory(repository, "LeanPool.A.Detail", ("LeanPool.Missing",))
+    _run(repository)
+    (repository / "LeanPool/B.lean").write_text("-- unrelated edit\n")
+    assert len(_run(repository)[1]) == 3
+
+
+@pytest.mark.parametrize("kind", ("lint", "axioms", "backdoors", "declarations"))
+def test_inventory_fallback_preserves_discovered_external_dependencies(
+    repository: Path, kind: str
+) -> None:
+    """An inventory error cannot hide a local dependency discovered before it."""
+    source = repository / "Aux/Support.lean"
+    source.parent.mkdir()
+    source.write_text("def support := 1\n")
+    _inventory(repository, "LeanPool.A.Detail", ("Aux.Support", "LeanPool.Missing"))
+    directory = repository / ".lake/validation-cache/v1"
+    modules = ["LeanPool.A", "LeanPool.A.Detail"]
+    cache = ValidationCache(repository, directory)
+    assert cache.check(kind, modules, lambda: []) == []
+    cache.save()
+    cache = ValidationCache(repository, directory)
+    assert cache.check(kind, modules, lambda: ["unexpected recheck"]) == []
+    cache.save()
+    source.write_text("def support := 2\n")
+    cache = ValidationCache(repository, directory)
+    assert cache.check(kind, modules, lambda: ["changed dependency"]) == [
+        "changed dependency"
+    ]