diff --git a/.github/workflows/a280831-fast.yml b/.github/workflows/a280831-fast.yml
new file mode 100644
index 00000000..69e4cdba
--- /dev/null
+++ b/.github/workflows/a280831-fast.yml
@@ -0,0 +1,78 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+
+name: A280831 fast exact audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/a280831-fast.yml'
+      - 'audits/consolidated-tracker-hard.md'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    name: exact parametric-family proofs
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout active research branch
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: research/a280831-parametric-families
+          fetch-depth: 1
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/sha.txt"
+      - name: Install pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Restore cache
+        uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: a280831-fast-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: a280831-fast-${{ runner.os }}-
+      - name: Fetch cache and compile imported theorem
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+          lake build FormalConjectures.Util.ProblemImports
+          mkdir -p .lake/build/lib/lean/FormalConjectures/OEIS
+          lake env lean \
+            -o .lake/build/lib/lean/FormalConjectures/OEIS/280831.olean \
+            FormalConjectures/OEIS/280831.lean
+      - name: Reject placeholders and trust escapes
+        run: |
+          set -euo pipefail
+          target=FormalConjectures/OEIS/A280831Families.lean
+          if grep -nE '\b(sorry|admit|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$target"; then
+            exit 1
+          fi
+      - name: Compile exact family theorems and print axioms
+        run: |
+          set -o pipefail
+          lake env lean FormalConjectures/OEIS/A280831Families.lean \
+            2>&1 | tee "$RUNNER_TEMP/a280831.log"
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          ! grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/a280831.log"
+      - name: Upload transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: a280831-fast-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/sha.txt
+            ${{ runner.temp }}/a280831.log
diff --git a/.github/workflows/consolidated-tracker-hard.yml b/.github/workflows/consolidated-tracker-hard.yml
new file mode 100644
index 00000000..b282dfb9
--- /dev/null
+++ b/.github/workflows/consolidated-tracker-hard.yml
@@ -0,0 +1,209 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+
+name: Consolidated tracker targeted Lean audits
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/consolidated-tracker-hard.yml'
+      - 'audits/consolidated-tracker-hard.md'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  erdos545:
+    name: Erdős 545 exact module
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout exact proof branch
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: research/erdos-545-counterexample
+          fetch-depth: 1
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/sha.txt"
+      - name: Install repository-pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Restore Lean cache
+        uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: erdos545-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: erdos545-${{ runner.os }}-
+      - name: Fetch pinned Mathlib cache
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+      - name: Reject placeholders and trust escapes
+        run: |
+          set -euo pipefail
+          target='FormalConjectures/ErdosProblems/545Counterexample.lean'
+          if grep -nE '\b(sorry|admit|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$target"; then
+            exit 1
+          fi
+      - name: Compile exact Erdős module
+        run: |
+          set -o pipefail
+          lake build FormalConjecturesUtil
+          lake env lean FormalConjectures/ErdosProblems/545Counterexample.lean \
+            2>&1 | tee "$RUNNER_TEMP/erdos545.log"
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          ! grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/erdos545.log"
+      - name: Upload transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos545-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/sha.txt
+            ${{ runner.temp }}/erdos545.log
+
+  sun26:
+    name: Sun 2.6 exact modules
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout exact proof branch
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: statement/sun-2-7-i
+          fetch-depth: 1
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/sha.txt"
+      - name: Install repository-pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Restore Lean cache
+        uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: sun26-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: sun26-${{ runner.os }}-
+      - name: Fetch pinned Mathlib cache
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+      - name: Reject proof placeholders and trust escapes
+        run: |
+          set -euo pipefail
+          targets=(
+            FormalConjectures/SunConjectures/2_6Finite.lean
+            FormalConjectures/SunConjectures/2_6Proof.lean
+          )
+          if grep -nE '\b(sorry|admit|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${targets[@]}"; then
+            exit 1
+          fi
+      - name: Compile finite kernel checks
+        run: |
+          set -o pipefail
+          : > "$RUNNER_TEMP/sun26.log"
+          mkdir -p .lake/build/lib/lean/FormalConjectures/SunConjectures
+          lake env lean \
+            -o .lake/build/lib/lean/FormalConjectures/SunConjectures/2_6Finite.olean \
+            FormalConjectures/SunConjectures/2_6Finite.lean \
+            2>&1 | tee -a "$RUNNER_TEMP/sun26.log"
+      - name: Compile complete analytic proof
+        run: |
+          set -o pipefail
+          lake env lean \
+            -o .lake/build/lib/lean/FormalConjectures/SunConjectures/2_6Proof.olean \
+            FormalConjectures/SunConjectures/2_6Proof.lean \
+            2>&1 | tee -a "$RUNNER_TEMP/sun26.log"
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          ! grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/sun26.log"
+      - name: Upload transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: sun26-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/sha.txt
+            ${{ runner.temp }}/sun26.log
+
+  a280831:
+    name: A280831 parametric families
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout exact research branch
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: research/a280831-parametric-families
+          fetch-depth: 1
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/sha.txt"
+      - name: Install repository-pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Restore Lean cache
+        uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: a280831-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: a280831-${{ runner.os }}-
+      - name: Fetch pinned Mathlib cache
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+      - name: Reject placeholders and trust escapes
+        run: |
+          set -euo pipefail
+          target='FormalConjectures/OEIS/A280831Families.lean'
+          if grep -nE '\b(sorry|admit|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$target"; then
+            exit 1
+          fi
+      - name: Compile exact family module
+        run: |
+          set -o pipefail
+          lake build FormalConjecturesUtil
+          mkdir -p .lake/build/lib/lean/FormalConjectures/OEIS
+          lake env lean \
+            -o .lake/build/lib/lean/FormalConjectures/OEIS/280831.olean \
+            FormalConjectures/OEIS/280831.lean
+          lake env lean \
+            -o .lake/build/lib/lean/FormalConjectures/OEIS/A280831Families.olean \
+            FormalConjectures/OEIS/A280831Families.lean \
+            2>&1 | tee "$RUNNER_TEMP/a280831.log"
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          ! grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/a280831.log"
+      - name: Upload transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: a280831-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/sha.txt
+            ${{ runner.temp }}/a280831.log
diff --git a/.github/workflows/erdos545-fast.yml b/.github/workflows/erdos545-fast.yml
new file mode 100644
index 00000000..f8981132
--- /dev/null
+++ b/.github/workflows/erdos545-fast.yml
@@ -0,0 +1,74 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+
+name: Erdos 545 fast exact audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/erdos545-fast.yml'
+      - 'audits/consolidated-tracker-hard.md'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    name: exact counterexample proof
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout active proof
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: research/erdos-545-counterexample
+          fetch-depth: 1
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/sha.txt"
+      - name: Install pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Restore cache
+        uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: erdos545-fast-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: erdos545-fast-${{ runner.os }}-
+      - name: Fetch cache and build support import
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+          lake build FormalConjectures.Util.ProblemImports
+      - name: Reject placeholders and trust escapes
+        run: |
+          set -euo pipefail
+          target=FormalConjectures/ErdosProblems/545Counterexample.lean
+          if grep -nE '\b(sorry|admit|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$target"; then
+            exit 1
+          fi
+      - name: Compile exact theorem and print axioms
+        run: |
+          set -o pipefail
+          lake env lean FormalConjectures/ErdosProblems/545Counterexample.lean \
+            2>&1 | tee "$RUNNER_TEMP/erdos545.log"
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          ! grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/erdos545.log"
+      - name: Upload transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos545-fast-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/sha.txt
+            ${{ runner.temp }}/erdos545.log
diff --git a/.github/workflows/erdos7-fast.yml b/.github/workflows/erdos7-fast.yml
new file mode 100644
index 00000000..ecca71d4
--- /dev/null
+++ b/.github/workflows/erdos7-fast.yml
@@ -0,0 +1,72 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+
+name: Erdos 7 CRT obstruction exact audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/erdos7-fast.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    name: exact pairwise-coprime obstruction
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout active proof
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: research/erdos7-pairwise-coprime-obstruction
+          fetch-depth: 1
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/sha.txt"
+      - name: Install pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Restore cache
+        uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: erdos7-fast-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: erdos7-fast-${{ runner.os }}-
+      - name: Fetch Mathlib cache
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+      - name: Reject placeholders and trust escapes
+        run: |
+          set -euo pipefail
+          target=FormalConjectures/ErdosProblems/7PairwiseCoprime.lean
+          if grep -nE '^[[:space:]]*(sorry|admit)([[:space:]]|$)|^[[:space:]]*unsafe[[:space:]]+(def|theorem|instance|opaque|abbrev|structure|inductive|class)|^[[:space:]]*axiom[[:space:]]+|Lean\.(trustCompiler|ofReduce|ofReduceBool)|^[[:space:]]*native_decide([[:space:]]|$)' "$target"; then
+            exit 1
+          fi
+      - name: Compile exact theorem and print axioms
+        run: |
+          set -o pipefail
+          lake env lean FormalConjectures/ErdosProblems/7PairwiseCoprime.lean \
+            2>&1 | tee "$RUNNER_TEMP/erdos7.log"
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          ! grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/erdos7.log"
+      - name: Upload transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos7-fast-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/sha.txt
+            ${{ runner.temp }}/erdos7.log
diff --git a/.github/workflows/rna-a4fc-exact.yml b/.github/workflows/rna-a4fc-exact.yml
new file mode 100644
index 00000000..78a91577
--- /dev/null
+++ b/.github/workflows/rna-a4fc-exact.yml
@@ -0,0 +1,98 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+
+name: RNA certificate exact audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/rna-a4fc-exact.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    name: exact algebraic certificate and axiom audit
+    runs-on: ubuntu-latest
+    timeout-minutes: 180
+    steps:
+      - name: Checkout immutable proof
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: a4fc5e6c9f846c424ba20bd3b6587546841cd811
+          fetch-depth: 1
+      - name: Confirm exact source
+        run: |
+          set -euo pipefail
+          test "$(git rev-parse HEAD)" = a4fc5e6c9f846c424ba20bd3b6587546841cd811
+          git rev-parse HEAD | tee "$RUNNER_TEMP/sha.txt"
+          test "$(cat lean-toolchain)" = 'leanprover/lean4:v4.27.0'
+      - name: Install pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Restore cache
+        uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: rna-a4fc-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: rna-a4fc-${{ runner.os }}-
+      - name: Fetch committed Mathlib cache
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+      - name: Reject placeholders and trust escapes
+        run: |
+          set -euo pipefail
+          targets=(RNAQuasiPowers.lean RNAQuasiPowers FormalConjectures/Arxiv/2602.19255/RNAQuasiPowers.lean FormalConjectures/Arxiv/2602.19255/RNAQuasiPowersAxiomAudit.lean)
+          if grep -RInE '^[[:space:]]*(sorry|admit)([[:space:]]|$)|^[[:space:]]*unsafe[[:space:]]+(def|theorem|instance|opaque|abbrev|structure|inductive|class)|^[[:space:]]*axiom[[:space:]]+|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${targets[@]}"; then
+            exit 1
+          fi
+      - name: Build internal certificate library
+        run: |
+          set -o pipefail
+          : > "$RUNNER_TEMP/rna.log"
+          lake --wfail build RNAQuasiPowers \
+            2>&1 | tee -a "$RUNNER_TEMP/rna.log"
+      - name: Build public support import
+        run: |
+          set -o pipefail
+          lake build FormalConjectures.Util.ProblemImports \
+            2>&1 | tee -a "$RUNNER_TEMP/rna.log"
+      - name: Compile and save public theorem layer
+        run: |
+          set -o pipefail
+          mkdir -p .lake/build/lib/lean/FormalConjectures/Arxiv/2602.19255
+          lake env lean -DwarningAsError=true \
+            -o .lake/build/lib/lean/FormalConjectures/Arxiv/2602.19255/RNAQuasiPowers.olean \
+            FormalConjectures/Arxiv/2602.19255/RNAQuasiPowers.lean \
+            2>&1 | tee -a "$RUNNER_TEMP/rna.log"
+      - name: Compile internal and public axiom audits
+        run: |
+          set -o pipefail
+          lake env lean -DwarningAsError=true RNAQuasiPowers/AxiomAudit.lean \
+            2>&1 | tee -a "$RUNNER_TEMP/rna.log"
+          lake env lean -DwarningAsError=true \
+            FormalConjectures/Arxiv/2602.19255/RNAQuasiPowersAxiomAudit.lean \
+            2>&1 | tee -a "$RUNNER_TEMP/rna.log"
+      - name: Enforce final axiom policy
+        run: |
+          set -euo pipefail
+          ! grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/rna.log"
+      - name: Upload transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: rna-a4fc-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/sha.txt
+            ${{ runner.temp }}/rna.log
diff --git a/.github/workflows/sun26-fast.yml b/.github/workflows/sun26-fast.yml
new file mode 100644
index 00000000..4fd63c69
--- /dev/null
+++ b/.github/workflows/sun26-fast.yml
@@ -0,0 +1,84 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+
+name: Sun 2.6 fast exact audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/sun26-fast.yml'
+      - 'audits/consolidated-tracker-hard.md'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    name: finite and analytic proof
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout active Sun proof
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: statement/sun-2-7-i
+          fetch-depth: 1
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/sha.txt"
+      - name: Install pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Restore cache
+        uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: sun26-fast-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: sun26-fast-${{ runner.os }}-
+      - name: Fetch Mathlib cache
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+      - name: Reject placeholders and trust escapes
+        run: |
+          set -euo pipefail
+          targets=(FormalConjectures/SunConjectures/2_6Finite.lean FormalConjectures/SunConjectures/2_6Proof.lean)
+          if grep -nE '(^|[[:space:]])(sorry|admit|unsafe)([[:space:]]|$)|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)|^[[:space:]]*native_decide([[:space:]]|$)' "${targets[@]}"; then
+            exit 1
+          fi
+      - name: Compile finite theorem by kernel reduction
+        run: |
+          set -o pipefail
+          : > "$RUNNER_TEMP/sun26.log"
+          mkdir -p .lake/build/lib/lean/FormalConjectures/SunConjectures
+          lake env lean \
+            -o .lake/build/lib/lean/FormalConjectures/SunConjectures/2_6Finite.olean \
+            FormalConjectures/SunConjectures/2_6Finite.lean \
+            2>&1 | tee -a "$RUNNER_TEMP/sun26.log"
+      - name: Compile analytic theorem
+        run: |
+          set -o pipefail
+          lake env lean \
+            -o .lake/build/lib/lean/FormalConjectures/SunConjectures/2_6Proof.olean \
+            FormalConjectures/SunConjectures/2_6Proof.lean \
+            2>&1 | tee -a "$RUNNER_TEMP/sun26.log"
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          ! grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/sun26.log"
+      - name: Upload transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: sun26-fast-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/sha.txt
+            ${{ runner.temp }}/sun26.log
diff --git a/audits/consolidated-tracker-hard.md b/audits/consolidated-tracker-hard.md
new file mode 100644
index 00000000..a0e8d2df
--- /dev/null
+++ b/audits/consolidated-tracker-hard.md
@@ -0,0 +1,17 @@
+# Consolidated tracker targeted audits
+
+This audit lane compiles three active research modules independently under each source repository's pinned Lean toolchain:
+
+- Erdős Problem 545 literal counterexample proof;
+- Zhi-Wei Sun Conjecture 2.6 finite and analytic proof modules;
+- OEIS A280831 parametric-family lemmas.
+
+Current iterative source heads:
+
+- Erdős 545: `0e3a4ac0fc7ee93cec184bf27bb8f4a79f3dcfca`;
+- Sun 2.6: `70b0ac2147bdcaed3390e4866571b1d2d925f5ac`;
+- A280831 families: `c39efc8f29479a6111a627fb388a846147a40556`.
+
+Each job records the exact checked source commit, rejects placeholders and compiler-trust shortcuts, compiles only the relevant module, inspects the printed axiom transcript, and uploads its log.
+
+This is an iterative verification surface. A final immutable audit will pin exact source SHAs after each branch is repaired and green.