From 9f15cfd83b00b864d36cfe17685e6dd42333ce55 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:04:50 -0700
Subject: [PATCH 01/20] ci: add targeted tracker proof audits

---
 .../workflows/consolidated-tracker-hard.yml   | 196 ++++++++++++++++++
 1 file changed, 196 insertions(+)
 create mode 100644 .github/workflows/consolidated-tracker-hard.yml

diff --git a/.github/workflows/consolidated-tracker-hard.yml b/.github/workflows/consolidated-tracker-hard.yml
new file mode 100644
index 00000000..3b62a1c9
--- /dev/null
+++ b/.github/workflows/consolidated-tracker-hard.yml
@@ -0,0 +1,196 @@
+# 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 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"
+          lake env lean 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 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 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-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/sha.txt
+            ${{ runner.temp }}/a280831.log

From cbe9201b936001c833ed0a8f4023c8617423b1c9 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:05:00 -0700
Subject: [PATCH 02/20] docs: trigger consolidated tracker audits

---
 audits/consolidated-tracker-hard.md | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 audits/consolidated-tracker-hard.md

diff --git a/audits/consolidated-tracker-hard.md b/audits/consolidated-tracker-hard.md
new file mode 100644
index 00000000..797a3603
--- /dev/null
+++ b/audits/consolidated-tracker-hard.md
@@ -0,0 +1,11 @@
+# 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.
+
+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.

From b5ee7224244c6a68ae7e799179b5b60c76a315bc Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:09:23 -0700
Subject: [PATCH 03/20] fix: build project-local imports before targeted Lean
 audits

---
 .../workflows/consolidated-tracker-hard.yml   | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/consolidated-tracker-hard.yml b/.github/workflows/consolidated-tracker-hard.yml
index 3b62a1c9..b282dfb9 100644
--- a/.github/workflows/consolidated-tracker-hard.yml
+++ b/.github/workflows/consolidated-tracker-hard.yml
@@ -57,6 +57,7 @@ jobs:
       - 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
@@ -118,12 +119,17 @@ jobs:
         run: |
           set -o pipefail
           : > "$RUNNER_TEMP/sun26.log"
-          lake env lean FormalConjectures/SunConjectures/2_6Finite.lean \
+          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 FormalConjectures/SunConjectures/2_6Proof.lean \
+          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: |
@@ -180,7 +186,14 @@ jobs:
       - name: Compile exact family module
         run: |
           set -o pipefail
-          lake env lean FormalConjectures/OEIS/A280831Families.lean \
+          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: |

From ccba899a5546a092c19182be16e523e151f3e5be Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:10:48 -0700
Subject: [PATCH 04/20] ci: add corrected fast Sun 2.6 audit

---
 .github/workflows/sun26-fast.yml | 84 ++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 .github/workflows/sun26-fast.yml

diff --git a/.github/workflows/sun26-fast.yml b/.github/workflows/sun26-fast.yml
new file mode 100644
index 00000000..2e34b6f3
--- /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'
+  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 and build native_decide
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+          lake build Mathlib.Tactic.NativeDecide
+      - name: Reject 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 theorem
+        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

From 179b708d4d59043da69be059b6be3ff9353dcbed Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:12:16 -0700
Subject: [PATCH 05/20] ci: add immutable RNA certificate audit

---
 .github/workflows/rna-a4fc-exact.yml | 96 ++++++++++++++++++++++++++++
 1 file changed, 96 insertions(+)
 create mode 100644 .github/workflows/rna-a4fc-exact.yml

diff --git a/.github/workflows/rna-a4fc-exact.yml b/.github/workflows/rna-a4fc-exact.yml
new file mode 100644
index 00000000..5c1776c7
--- /dev/null
+++ b/.github/workflows/rna-a4fc-exact.yml
@@ -0,0 +1,96 @@
+# 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 '\b(sorry|admit|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|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 public theorem layer
+        run: |
+          set -o pipefail
+          lake env lean -DwarningAsError=true \
+            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

From e6e6d36986bf5d19b678fea29624667a83e32bee Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:17:11 -0700
Subject: [PATCH 06/20] ci: retest corrected Sun threshold proof

---
 .github/workflows/sun26-fast.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/sun26-fast.yml b/.github/workflows/sun26-fast.yml
index 2e34b6f3..84c42eb8 100644
--- a/.github/workflows/sun26-fast.yml
+++ b/.github/workflows/sun26-fast.yml
@@ -8,6 +8,7 @@ on:
     branches: [main]
     paths:
       - '.github/workflows/sun26-fast.yml'
+      - 'audits/consolidated-tracker-hard.md'
   workflow_dispatch:
 
 permissions:

From 17dbae57113710f51940ccef068f838dd90b008e Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:18:30 -0700
Subject: [PATCH 07/20] ci: retest repaired Sun and A280831 sources

---
 audits/consolidated-tracker-hard.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/audits/consolidated-tracker-hard.md b/audits/consolidated-tracker-hard.md
index 797a3603..4195b03f 100644
--- a/audits/consolidated-tracker-hard.md
+++ b/audits/consolidated-tracker-hard.md
@@ -6,6 +6,12 @@ This audit lane compiles three active research modules independently under each
 - Zhi-Wei Sun Conjecture 2.6 finite and analytic proof modules;
 - OEIS A280831 parametric-family lemmas.
 
+Current iterative source heads:
+
+- Erdős 545: `e48690cec64e5b2a719f344b2ffd2bf012a0b487`;
+- Sun 2.6: `fc3595a02b559ee08fae89f5f0eeeabfeeda5b83`;
+- A280831 families: `58797393438be078942dc8c7bc2d456d01779fee`.
+
 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.

From e54fd2a2491f3cc63fa5bf0e136a1d7ca08da338 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:22:18 -0700
Subject: [PATCH 08/20] =?UTF-8?q?ci:=20add=20corrected=20fast=20Erd=C5=91s?=
 =?UTF-8?q?=20545=20audit?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/erdos545-fast.yml | 74 +++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 .github/workflows/erdos545-fast.yml

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

From 1e713b1e994ff1f74ac2d70d95f8d41933c94dcd Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:22:40 -0700
Subject: [PATCH 09/20] ci: add corrected fast A280831 audit

---
 .github/workflows/a280831-fast.yml | 74 ++++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 .github/workflows/a280831-fast.yml

diff --git a/.github/workflows/a280831-fast.yml b/.github/workflows/a280831-fast.yml
new file mode 100644
index 00000000..ab7c3253
--- /dev/null
+++ b/.github/workflows/a280831-fast.yml
@@ -0,0 +1,74 @@
+# 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 build imported theorem
+        run: |
+          set -euo pipefail
+          lake exe cache unpack || true
+          lake exe cache get
+          lake build FormalConjectures.OEIS.280831
+      - 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

From cbcbc4186ff8c447fbbb8542425ade8ec439c7bd Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:23:48 -0700
Subject: [PATCH 10/20] fix: compile A280831 imported module by path

---
 .github/workflows/a280831-fast.yml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/a280831-fast.yml b/.github/workflows/a280831-fast.yml
index ab7c3253..69e4cdba 100644
--- a/.github/workflows/a280831-fast.yml
+++ b/.github/workflows/a280831-fast.yml
@@ -42,12 +42,16 @@ jobs:
             .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 build imported theorem
+      - name: Fetch cache and compile imported theorem
         run: |
           set -euo pipefail
           lake exe cache unpack || true
           lake exe cache get
-          lake build FormalConjectures.OEIS.280831
+          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

From 0ef5f1be220b3aa83b66d460fa4409bda5931ab9 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:29:03 -0700
Subject: [PATCH 11/20] fix: distinguish Lean placeholders from sorry-free
 prose

---
 .github/workflows/rna-a4fc-exact.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/rna-a4fc-exact.yml b/.github/workflows/rna-a4fc-exact.yml
index 5c1776c7..f95c18ad 100644
--- a/.github/workflows/rna-a4fc-exact.yml
+++ b/.github/workflows/rna-a4fc-exact.yml
@@ -54,7 +54,7 @@ jobs:
         run: |
           set -euo pipefail
           targets=(RNAQuasiPowers.lean RNAQuasiPowers FormalConjectures/Arxiv/2602.19255/RNAQuasiPowers.lean FormalConjectures/Arxiv/2602.19255/RNAQuasiPowersAxiomAudit.lean)
-          if grep -RInE '\b(sorry|admit|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${targets[@]}"; then
+          if grep -RInE '(^|[[:space:]])(sorry|admit|unsafe)([[:space:]]|$)|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${targets[@]}"; then
             exit 1
           fi
       - name: Build internal certificate library

From 0c4e619f82be75868e83bf64ce67e0dca031d5ca Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:30:11 -0700
Subject: [PATCH 12/20] ci: audit kernel-reduced Sun finite proof

---
 .github/workflows/sun26-fast.yml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/sun26-fast.yml b/.github/workflows/sun26-fast.yml
index 84c42eb8..5c2776c5 100644
--- a/.github/workflows/sun26-fast.yml
+++ b/.github/workflows/sun26-fast.yml
@@ -42,20 +42,19 @@ jobs:
             .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 and build native_decide
+      - name: Fetch Mathlib cache
         run: |
           set -euo pipefail
           lake exe cache unpack || true
           lake exe cache get
-          lake build Mathlib.Tactic.NativeDecide
       - name: Reject 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
+          if grep -nE '(^|[[:space:]])(sorry|admit|unsafe)([[:space:]]|$)|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)|native_decide' "${targets[@]}"; then
             exit 1
           fi
-      - name: Compile finite theorem
+      - name: Compile finite theorem by kernel reduction
         run: |
           set -o pipefail
           : > "$RUNNER_TEMP/sun26.log"

From 233bf495177a2cdb5e1b5f04c862f6d97d81749f Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:32:56 -0700
Subject: [PATCH 13/20] ci: retest repaired tracker proof heads

---
 audits/consolidated-tracker-hard.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/audits/consolidated-tracker-hard.md b/audits/consolidated-tracker-hard.md
index 4195b03f..ff11c0c5 100644
--- a/audits/consolidated-tracker-hard.md
+++ b/audits/consolidated-tracker-hard.md
@@ -8,9 +8,9 @@ This audit lane compiles three active research modules independently under each
 
 Current iterative source heads:
 
-- Erdős 545: `e48690cec64e5b2a719f344b2ffd2bf012a0b487`;
-- Sun 2.6: `fc3595a02b559ee08fae89f5f0eeeabfeeda5b83`;
-- A280831 families: `58797393438be078942dc8c7bc2d456d01779fee`.
+- Erdős 545: `d1521d52329c1ce891642d50be1bdb654ad43433`;
+- Sun 2.6: `4541e7704610f4e16bb1ef4d637a5867ac2c78db`;
+- 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.
 

From 2ac82a75e91d93b703b1321086b26b687ab62bd8 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:37:57 -0700
Subject: [PATCH 14/20] fix: scan only actual native_decide tactic lines

---
 .github/workflows/sun26-fast.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/sun26-fast.yml b/.github/workflows/sun26-fast.yml
index 5c2776c5..4fd63c69 100644
--- a/.github/workflows/sun26-fast.yml
+++ b/.github/workflows/sun26-fast.yml
@@ -51,7 +51,7 @@ jobs:
         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)|native_decide' "${targets[@]}"; then
+          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

From c51747a1a1072051b1f499b40eda4268d90e4ad9 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:40:14 -0700
Subject: [PATCH 15/20] fix: detect only actual Lean trust declarations

---
 .github/workflows/rna-a4fc-exact.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/rna-a4fc-exact.yml b/.github/workflows/rna-a4fc-exact.yml
index f95c18ad..e61ae2ab 100644
--- a/.github/workflows/rna-a4fc-exact.yml
+++ b/.github/workflows/rna-a4fc-exact.yml
@@ -54,7 +54,7 @@ jobs:
         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|unsafe)([[:space:]]|$)|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${targets[@]}"; then
+          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

From 188a92386096ff7b8ad91d26a30673580476bed1 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:41:06 -0700
Subject: [PATCH 16/20] =?UTF-8?q?ci:=20audit=20clean=20one-file=20Erd?=
 =?UTF-8?q?=C5=91s=20545=20head?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 audits/consolidated-tracker-hard.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/audits/consolidated-tracker-hard.md b/audits/consolidated-tracker-hard.md
index ff11c0c5..75d86e6b 100644
--- a/audits/consolidated-tracker-hard.md
+++ b/audits/consolidated-tracker-hard.md
@@ -8,7 +8,7 @@ This audit lane compiles three active research modules independently under each
 
 Current iterative source heads:
 
-- Erdős 545: `d1521d52329c1ce891642d50be1bdb654ad43433`;
+- Erdős 545: `0e3a4ac0fc7ee93cec184bf27bb8f4a79f3dcfca`;
 - Sun 2.6: `4541e7704610f4e16bb1ef4d637a5867ac2c78db`;
 - A280831 families: `c39efc8f29479a6111a627fb388a846147a40556`.
 

From a143c7da6ff589fb3d2d9b1c38f8c1ba376f0ea4 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:47:30 -0700
Subject: [PATCH 17/20] ci: test block-decomposed Sun kernel proof

---
 audits/consolidated-tracker-hard.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/audits/consolidated-tracker-hard.md b/audits/consolidated-tracker-hard.md
index 75d86e6b..cb454838 100644
--- a/audits/consolidated-tracker-hard.md
+++ b/audits/consolidated-tracker-hard.md
@@ -9,7 +9,7 @@ This audit lane compiles three active research modules independently under each
 Current iterative source heads:
 
 - Erdős 545: `0e3a4ac0fc7ee93cec184bf27bb8f4a79f3dcfca`;
-- Sun 2.6: `4541e7704610f4e16bb1ef4d637a5867ac2c78db`;
+- Sun 2.6: `65ab4714f5fb032c9d58430c71c0f5a5e85870ce`;
 - 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.

From f03f5f2531964da4a4a128d34fdea98ca3900104 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:48:36 -0700
Subject: [PATCH 18/20] fix: save RNA public module before axiom audits

---
 .github/workflows/rna-a4fc-exact.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/rna-a4fc-exact.yml b/.github/workflows/rna-a4fc-exact.yml
index e61ae2ab..78a91577 100644
--- a/.github/workflows/rna-a4fc-exact.yml
+++ b/.github/workflows/rna-a4fc-exact.yml
@@ -68,10 +68,12 @@ jobs:
           set -o pipefail
           lake build FormalConjectures.Util.ProblemImports \
             2>&1 | tee -a "$RUNNER_TEMP/rna.log"
-      - name: Compile public theorem layer
+      - 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

From 707df94d1cff1ab4626346698948cf4f76af3989 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:53:03 -0700
Subject: [PATCH 19/20] ci: retest reducible Sun block certificate

---
 audits/consolidated-tracker-hard.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/audits/consolidated-tracker-hard.md b/audits/consolidated-tracker-hard.md
index cb454838..a0e8d2df 100644
--- a/audits/consolidated-tracker-hard.md
+++ b/audits/consolidated-tracker-hard.md
@@ -9,7 +9,7 @@ This audit lane compiles three active research modules independently under each
 Current iterative source heads:
 
 - Erdős 545: `0e3a4ac0fc7ee93cec184bf27bb8f4a79f3dcfca`;
-- Sun 2.6: `65ab4714f5fb032c9d58430c71c0f5a5e85870ce`;
+- 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.

From 2de01b8218a22a2cd7db8b7d82fd3f4004970eef Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sat, 25 Jul 2026 21:58:20 -0700
Subject: [PATCH 20/20] =?UTF-8?q?ci:=20add=20exact=20Erd=C5=91s=207=20CRT?=
 =?UTF-8?q?=20obstruction=20audit?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/erdos7-fast.yml | 72 +++++++++++++++++++++++++++++++
 1 file changed, 72 insertions(+)
 create mode 100644 .github/workflows/erdos7-fast.yml

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