From 02e74ac4b8595a2ec2f1c3c7f8b0858aee9a1585 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 22:48:56 -0700
Subject: [PATCH 01/43] Audit migrated checkerboard all-n proof

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 95 +++++++++++++++++++
 1 file changed, 95 insertions(+)
 create mode 100644 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
new file mode 100644
index 00000000..12250e1c
--- /dev/null
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -0,0 +1,95 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+
+name: Checkerboard all-n ProofPlaygrond audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/checkerboard-alln-proofplaygrond-audit.yml'
+      - 'audits/checkerboard-alln-proofplaygrond.md'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  audit:
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout exact migrated proof
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/ProofPlaygrond
+          ref: 8fc0535a3677bebdfbb16a699e2897da9958ec90
+          fetch-depth: 1
+
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/resolved-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 build cache
+        uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: checkerboard-alln-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: checkerboard-alln-${{ runner.os }}-
+
+      - name: Restore pinned Mathlib cache
+        run: |
+          set -euo pipefail
+          "$HOME/.elan/bin/lake" exe cache unpack || true
+          "$HOME/.elan/bin/lake" exe cache get
+
+      - name: Reject proof holes and trust shortcuts
+        run: |
+          set -euo pipefail
+          files=(Checkerboard/*.lean)
+          if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then
+            echo 'Forbidden placeholder or trust shortcut found in checkerboard proof chain.' >&2
+            exit 1
+          fi
+
+      - name: Compile exact all-n theorem
+        run: |
+          set -o pipefail
+          "$HOME/.elan/bin/lake" env lean Checkerboard/AllNTheorem.lean \
+            2>&1 | tee "$RUNNER_TEMP/checkerboard-alln.log"
+
+      - name: Run terminal axiom audit
+        run: |
+          set -o pipefail
+          cat > CheckerboardAllNAxiomAudit.lean <<'EOF'
+          import Checkerboard.AllNTheorem
+          #print axioms Checkerboard.checkerboard_upper_all_n
+          EOF
+          "$HOME/.elan/bin/lake" env lean CheckerboardAllNAxiomAudit.lean \
+            2>&1 | tee -a "$RUNNER_TEMP/checkerboard-alln.log"
+
+      - name: Enforce final axiom policy
+        run: |
+          set -euo pipefail
+          if grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-alln.log"; then
+            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
+            exit 1
+          fi
+
+      - name: Upload transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: checkerboard-alln-proofplaygrond-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/resolved-sha.txt
+            ${{ runner.temp }}/checkerboard-alln.log
+          if-no-files-found: warn

From 36ee309cea3818e5ef8bb34eff3f93455863610e Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 22:52:40 -0700
Subject: [PATCH 02/43] Reuse cached Lean environment for checkerboard audit

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 31 ++++++++++++++++---
 1 file changed, 26 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 12250e1c..705f1eb6 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -36,20 +36,41 @@ jobs:
             | sh -s -- -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
-      - name: Restore Lean build cache
-        uses: actions/cache@v4
+      - name: Restore reusable Lean build cache
+        id: lean-cache
+        uses: actions/cache/restore@v4
         with:
           path: |
             .lake/packages
             .lake/build
           key: checkerboard-alln-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
-          restore-keys: checkerboard-alln-${{ runner.os }}-
+          restore-keys: |
+            checkerboard-alln-${{ runner.os }}-
+            a263135-${{ runner.os }}-
+            litt-${{ runner.os }}-
+            wow59-${{ runner.os }}-
 
-      - name: Restore pinned Mathlib cache
+      - name: Restore pinned Mathlib cache when needed
+        if: steps.lean-cache.outputs.cache-matched-key == ''
         run: |
           set -euo pipefail
           "$HOME/.elan/bin/lake" exe cache unpack || true
-          "$HOME/.elan/bin/lake" exe cache get
+          for attempt in 1 2 3; do
+            if "$HOME/.elan/bin/lake" exe cache get; then
+              exit 0
+            fi
+            sleep 10
+          done
+          exit 1
+
+      - name: Save reusable Lean build cache
+        if: steps.lean-cache.outputs.cache-matched-key == ''
+        uses: actions/cache/save@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: checkerboard-alln-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
 
       - name: Reject proof holes and trust shortcuts
         run: |

From b157910ea46e8642332b23c4e39e2701044ce60a Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 22:55:05 -0700
Subject: [PATCH 03/43] Compile checkerboard from restored cache

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 20 +------------------
 1 file changed, 1 insertion(+), 19 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 705f1eb6..77a1c401 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -37,7 +37,6 @@ jobs:
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
       - name: Restore reusable Lean build cache
-        id: lean-cache
         uses: actions/cache/restore@v4
         with:
           path: |
@@ -50,27 +49,10 @@ jobs:
             litt-${{ runner.os }}-
             wow59-${{ runner.os }}-
 
-      - name: Restore pinned Mathlib cache when needed
-        if: steps.lean-cache.outputs.cache-matched-key == ''
+      - name: Unpack any restored Mathlib cache
         run: |
           set -euo pipefail
           "$HOME/.elan/bin/lake" exe cache unpack || true
-          for attempt in 1 2 3; do
-            if "$HOME/.elan/bin/lake" exe cache get; then
-              exit 0
-            fi
-            sleep 10
-          done
-          exit 1
-
-      - name: Save reusable Lean build cache
-        if: steps.lean-cache.outputs.cache-matched-key == ''
-        uses: actions/cache/save@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-          key: checkerboard-alln-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
 
       - name: Reject proof holes and trust shortcuts
         run: |

From fa7462142fa9c24e8e028d8408f0c5c8cf9c9ee5 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 22:57:37 -0700
Subject: [PATCH 04/43] Audit checkerboard with its pinned Lean 4.32 project

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 37 +++++++++++++------
 1 file changed, 26 insertions(+), 11 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 77a1c401..31750511 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -19,11 +19,11 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout exact migrated proof
+      - name: Checkout exact migrated proof project
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 8fc0535a3677bebdfbb16a699e2897da9958ec90
+          ref: 85f69c802c08b145dbf2946055d34ec902ac6697
           fetch-depth: 1
 
       - name: Record exact commit
@@ -36,23 +36,38 @@ jobs:
             | sh -s -- -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
-      - name: Restore reusable Lean build cache
+      - name: Restore checkerboard Lean cache
         uses: actions/cache/restore@v4
         with:
           path: |
             .lake/packages
             .lake/build
-          key: checkerboard-alln-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
-          restore-keys: |
-            checkerboard-alln-${{ runner.os }}-
-            a263135-${{ runner.os }}-
-            litt-${{ runner.os }}-
-            wow59-${{ runner.os }}-
+          key: checkerboard-432-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.lean') }}
+          restore-keys: checkerboard-432-${{ runner.os }}-
 
-      - name: Unpack any restored Mathlib cache
+      - name: Resolve pinned Mathlib
         run: |
           set -euo pipefail
-          "$HOME/.elan/bin/lake" exe cache unpack || true
+          "$HOME/.elan/bin/lake" update
+
+      - name: Fetch Mathlib olean cache
+        run: |
+          set -euo pipefail
+          for attempt in 1 2 3; do
+            if "$HOME/.elan/bin/lake" exe cache get; then
+              exit 0
+            fi
+            sleep 10
+          done
+          exit 1
+
+      - name: Save checkerboard Lean cache
+        uses: actions/cache/save@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: checkerboard-432-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.lean') }}
 
       - name: Reject proof holes and trust shortcuts
         run: |

From 6818d044691caf4ac1c6bdc83396ad2499a1399a Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 23:01:27 -0700
Subject: [PATCH 05/43] Audit minimal checkerboard library root

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 31750511..b312ebf1 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -23,7 +23,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 85f69c802c08b145dbf2946055d34ec902ac6697
+          ref: be4caf8714f89d84d8f56662c01eea5eb6f05c70
           fetch-depth: 1
 
       - name: Record exact commit

From 9ef4f2f5e3ef4716a6db27df85f2216ee6d73952 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 23:05:19 -0700
Subject: [PATCH 06/43] Audit conventional checkerboard root module

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index b312ebf1..85cd4eff 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -23,7 +23,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: be4caf8714f89d84d8f56662c01eea5eb6f05c70
+          ref: d1c24f00796c59c695eb0ceb1ade131f0e463b5d
           fetch-depth: 1
 
       - name: Record exact commit

From 0e3fe64da9775b1ea6f544a715b9b0191b7a1bf6 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 23:08:38 -0700
Subject: [PATCH 07/43] Build checkerboard library before axiom audit

---
 .../workflows/checkerboard-alln-proofplaygrond-audit.yml    | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 85cd4eff..cabcdc45 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -72,16 +72,16 @@ jobs:
       - name: Reject proof holes and trust shortcuts
         run: |
           set -euo pipefail
-          files=(Checkerboard/*.lean)
+          files=(Checkerboard.lean Checkerboard/*.lean)
           if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then
             echo 'Forbidden placeholder or trust shortcut found in checkerboard proof chain.' >&2
             exit 1
           fi
 
-      - name: Compile exact all-n theorem
+      - name: Build exact all-n library
         run: |
           set -o pipefail
-          "$HOME/.elan/bin/lake" env lean Checkerboard/AllNTheorem.lean \
+          "$HOME/.elan/bin/lake" build Checkerboard \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-alln.log"
 
       - name: Run terminal axiom audit

From 7d0efb9945b3d685866773bc7d88d9ca2a8b5cdf Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 23:33:58 -0700
Subject: [PATCH 08/43] Audit repaired checkerboard support modules

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index cabcdc45..67196712 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -23,7 +23,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: d1c24f00796c59c695eb0ceb1ade131f0e463b5d
+          ref: 2ac1cabede0f3c0b6d4324d41912c86e131e96c6
           fetch-depth: 1
 
       - name: Record exact commit

From 0f9d3d653c98efb7e3b5f813a824887f3f76fdb6 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 23:42:59 -0700
Subject: [PATCH 09/43] Audit final checkerboard support repairs

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 67196712..02c11a3f 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -23,7 +23,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 2ac1cabede0f3c0b6d4324d41912c86e131e96c6
+          ref: c6f5ef34bbe926cdb4b60c1da890a0f8f14eea39
           fetch-depth: 1
 
       - name: Record exact commit

From 03ee3bb3eec80512f6e1b786d5b0885ccb1bafd0 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Wed, 22 Jul 2026 23:51:23 -0700
Subject: [PATCH 10/43] Audit checkerboard filter and cast repairs

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 02c11a3f..e5d03871 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -23,7 +23,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: c6f5ef34bbe926cdb4b60c1da890a0f8f14eea39
+          ref: d59a5abcbdca0a41f874b5a8b568e32ea8a29dfe
           fetch-depth: 1
 
       - name: Record exact commit

From d14704ec80748ee6ccd3517215889e603190c3ea Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 00:00:05 -0700
Subject: [PATCH 11/43] Audit final checkerboard support goals

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index e5d03871..8b27dc88 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -23,7 +23,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: d59a5abcbdca0a41f874b5a8b568e32ea8a29dfe
+          ref: 0a9bbc29df42110e9a4cc72e0591a60d6df554c6
           fetch-depth: 1
 
       - name: Record exact commit

From a70032be81d268d1d573bec2a0da856cbd429141 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 00:07:17 -0700
Subject: [PATCH 12/43] Audit checkerboard support-complete source

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 8b27dc88..d87af5d5 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -23,7 +23,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 0a9bbc29df42110e9a4cc72e0591a60d6df554c6
+          ref: 03d2e3dca3740d8557ddccf0938b576ad56da2da
           fetch-depth: 1
 
       - name: Record exact commit

From 361735088ca23a67d237252eb44a6d2090e3b367 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 00:14:51 -0700
Subject: [PATCH 13/43] Audit checkerboard weighted-certificate repairs

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index d87af5d5..b29bc416 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -23,7 +23,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 03d2e3dca3740d8557ddccf0938b576ad56da2da
+          ref: 8b74711053b5fe6069ca2e9c42e52c2b1c168146
           fetch-depth: 1
 
       - name: Record exact commit

From 940189f196d3fcdcb8d37b4ab280608ba61ccaea Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 00:27:39 -0700
Subject: [PATCH 14/43] Audit checkerboard cast-difference repair

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index b29bc416..f22f312d 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -23,7 +23,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 8b74711053b5fe6069ca2e9c42e52c2b1c168146
+          ref: b6b2e5541702a09f89a0176bae2dc0c7899a01c4
           fetch-depth: 1
 
       - name: Record exact commit

From f76ccf3264332c5f7dda84b8b6d7bbfe6abeb1a8 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 00:39:18 -0700
Subject: [PATCH 15/43] Audit current checkerboard repair tip

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index f22f312d..294a9348 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -19,11 +19,11 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout exact migrated proof project
+      - name: Checkout current checkerboard proof project
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: b6b2e5541702a09f89a0176bae2dc0c7899a01c4
+          ref: migrate/checkerboard-alln-27a80067
           fetch-depth: 1
 
       - name: Record exact commit

From 90e99ca1f6fd1ccbf5894ee81181120153a504c0 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 00:54:55 -0700
Subject: [PATCH 16/43] Synchronize checkerboard weighted-certificate audit

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 294a9348..b8e1c3f3 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,5 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
+# Synchronization gate for source commit 5b1a99ff750a6160c7e284dee3c62f85e2262dfa.
 
 name: Checkerboard all-n ProofPlaygrond audit
 

From 700e62e1dd0a493c46de61d28e1060a48c662927 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 01:31:34 -0700
Subject: [PATCH 17/43] Pin checkerboard audit to n6 and cast repairs

---
 .../workflows/checkerboard-alln-proofplaygrond-audit.yml    | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index b8e1c3f3..ef4bbfb5 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Synchronization gate for source commit 5b1a99ff750a6160c7e284dee3c62f85e2262dfa.
+# Exact audit gate for source commit b790c9d75033659e272fc64bac23b185c07fabc2.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -20,11 +20,11 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout current checkerboard proof project
+      - name: Checkout exact migrated proof project
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: migrate/checkerboard-alln-27a80067
+          ref: b790c9d75033659e272fc64bac23b185c07fabc2
           fetch-depth: 1
 
       - name: Record exact commit

From 545de4d7f6f8ff8d43b746d54b849c5e13dea185 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 01:46:21 -0700
Subject: [PATCH 18/43] Test compact checkerboard n6 SAT certificate

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 53 +++++--------------
 1 file changed, 12 insertions(+), 41 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index ef4bbfb5..d08422e9 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Exact audit gate for source commit b790c9d75033659e272fc64bac23b185c07fabc2.
+# Focused audit for compact n6 SAT source commit aa165e404a0319c272c2eb6cf76efa29e144b06c.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: b790c9d75033659e272fc64bac23b185c07fabc2
+          ref: aa165e404a0319c272c2eb6cf76efa29e144b06c
           fetch-depth: 1
 
       - name: Record exact commit
@@ -62,53 +62,24 @@ jobs:
           done
           exit 1
 
-      - name: Save checkerboard Lean cache
-        uses: actions/cache/save@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-          key: checkerboard-432-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.lean') }}
-
-      - name: Reject proof holes and trust shortcuts
-        run: |
-          set -euo pipefail
-          files=(Checkerboard.lean Checkerboard/*.lean)
-          if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then
-            echo 'Forbidden placeholder or trust shortcut found in checkerboard proof chain.' >&2
-            exit 1
-          fi
-
-      - name: Build exact all-n library
+      - name: Test compact n6 SAT certificate
+        id: sat
+        continue-on-error: true
         run: |
           set -o pipefail
-          "$HOME/.elan/bin/lake" build Checkerboard \
+          "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-alln.log"
 
-      - name: Run terminal axiom audit
-        run: |
-          set -o pipefail
-          cat > CheckerboardAllNAxiomAudit.lean <<'EOF'
-          import Checkerboard.AllNTheorem
-          #print axioms Checkerboard.checkerboard_upper_all_n
-          EOF
-          "$HOME/.elan/bin/lake" env lean CheckerboardAllNAxiomAudit.lean \
-            2>&1 | tee -a "$RUNNER_TEMP/checkerboard-alln.log"
-
-      - name: Enforce final axiom policy
-        run: |
-          set -euo pipefail
-          if grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-alln.log"; then
-            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
-            exit 1
-          fi
-
-      - name: Upload transcript
+      - name: Upload focused transcript
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: checkerboard-alln-proofplaygrond-${{ github.run_id }}
+          name: checkerboard-n6-sat-${{ github.run_id }}
           path: |
             ${{ runner.temp }}/resolved-sha.txt
             ${{ runner.temp }}/checkerboard-alln.log
           if-no-files-found: warn
+
+      - name: Enforce focused result
+        if: always()
+        run: test '${{ steps.sat.outcome }}' = 'success'

From cb0930953bef06e044d9453ba3584321e6695f84 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 01:50:19 -0700
Subject: [PATCH 19/43] Retrigger compact checkerboard n6 SAT audit

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index d08422e9..94258859 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,7 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
 # Focused audit for compact n6 SAT source commit aa165e404a0319c272c2eb6cf76efa29e144b06c.
+# Retriggered after reopening the canonical audit PR.
 
 name: Checkerboard all-n ProofPlaygrond audit
 

From a70f370a92421ad5a5273256da217b202c8d4259 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 01:56:03 -0700
Subject: [PATCH 20/43] Audit pure BitVec checkerboard n6 certificate

---
 .../checkerboard-alln-proofplaygrond-audit.yml      | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 94258859..0ae2231f 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,7 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused audit for compact n6 SAT source commit aa165e404a0319c272c2eb6cf76efa29e144b06c.
-# Retriggered after reopening the canonical audit PR.
+# Focused audit for pure BitVec n6 SAT source commit f7bb9301c63bad3e23121b90117c0df7b4f3a9d2.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -25,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: aa165e404a0319c272c2eb6cf76efa29e144b06c
+          ref: f7bb9301c63bad3e23121b90117c0df7b4f3a9d2
           fetch-depth: 1
 
       - name: Record exact commit
@@ -63,9 +62,7 @@ jobs:
           done
           exit 1
 
-      - name: Test compact n6 SAT certificate
-        id: sat
-        continue-on-error: true
+      - name: Test pure BitVec n6 SAT certificate
         run: |
           set -o pipefail
           "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
@@ -80,7 +77,3 @@ jobs:
             ${{ runner.temp }}/resolved-sha.txt
             ${{ runner.temp }}/checkerboard-alln.log
           if-no-files-found: warn
-
-      - name: Enforce focused result
-        if: always()
-        run: test '${{ steps.sat.outcome }}' = 'success'

From d78cc44815c4f37b7e22cd8305b707d3c70591d6 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 02:04:25 -0700
Subject: [PATCH 21/43] Generate checkerboard n6 LRAT certificates

---
 .../checkerboard-alln-proofplaygrond-audit.yml   | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 0ae2231f..eb0f0251 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused audit for pure BitVec n6 SAT source commit f7bb9301c63bad3e23121b90117c0df7b4f3a9d2.
+# One-time LRAT generation for source commit d8650ce8d9e2528adaf92c91bb58a8e9d8e23231.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -20,11 +20,11 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout exact migrated proof project
+      - name: Checkout exact LRAT-generation source
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: f7bb9301c63bad3e23121b90117c0df7b4f3a9d2
+          ref: d8650ce8d9e2528adaf92c91bb58a8e9d8e23231
           fetch-depth: 1
 
       - name: Record exact commit
@@ -62,18 +62,20 @@ jobs:
           done
           exit 1
 
-      - name: Test pure BitVec n6 SAT certificate
+      - name: Generate LRAT certificates
         run: |
           set -o pipefail
           "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-alln.log"
+          find Checkerboard -maxdepth 1 -name '*.lrat' -print
 
-      - name: Upload focused transcript
+      - name: Upload generated LRAT and transcript
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: checkerboard-n6-sat-${{ github.run_id }}
+          name: checkerboard-n6-lrat-${{ github.run_id }}
           path: |
             ${{ runner.temp }}/resolved-sha.txt
             ${{ runner.temp }}/checkerboard-alln.log
-          if-no-files-found: warn
+            Checkerboard/*.lrat
+          if-no-files-found: error

From 4d81d244c9f6b008002a3e0dbd1932a5a061b1d3 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 02:07:49 -0700
Subject: [PATCH 22/43] Audit kernel-only checkerboard n6 omega certificate

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 24 ++++++++++++-------
 1 file changed, 15 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index eb0f0251..d5d9f17a 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# One-time LRAT generation for source commit d8650ce8d9e2528adaf92c91bb58a8e9d8e23231.
+# Focused audit for kernel-only n6 source commit ddac364bedbd748af9a4b3c3f8643ee3f65e5f7d.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -20,11 +20,11 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout exact LRAT-generation source
+      - name: Checkout exact omega-certificate source
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: d8650ce8d9e2528adaf92c91bb58a8e9d8e23231
+          ref: ddac364bedbd748af9a4b3c3f8643ee3f65e5f7d
           fetch-depth: 1
 
       - name: Record exact commit
@@ -62,20 +62,26 @@ jobs:
           done
           exit 1
 
-      - name: Generate LRAT certificates
+      - name: Compile kernel-only n6 certificate
         run: |
           set -o pipefail
           "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-alln.log"
-          find Checkerboard -maxdepth 1 -name '*.lrat' -print
 
-      - name: Upload generated LRAT and transcript
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-alln.log"; then
+            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
+            exit 1
+          fi
+
+      - name: Upload focused transcript
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: checkerboard-n6-lrat-${{ github.run_id }}
+          name: checkerboard-n6-omega-${{ github.run_id }}
           path: |
             ${{ runner.temp }}/resolved-sha.txt
             ${{ runner.temp }}/checkerboard-alln.log
-            Checkerboard/*.lrat
-          if-no-files-found: error
+          if-no-files-found: warn

From 47538e69a2d846163ff8fc0afb61faca09b93ec6 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 02:09:18 -0700
Subject: [PATCH 23/43] Run full checkerboard all-n kernel audit at ddac364b

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 33 +++++++++++++++----
 1 file changed, 26 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index d5d9f17a..da8a501c 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused audit for kernel-only n6 source commit ddac364bedbd748af9a4b3c3f8643ee3f65e5f7d.
+# Full all-n audit for kernel-only source commit ddac364bedbd748af9a4b3c3f8643ee3f65e5f7d.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -20,7 +20,7 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout exact omega-certificate source
+      - name: Checkout exact repaired all-n source
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
@@ -62,13 +62,32 @@ jobs:
           done
           exit 1
 
-      - name: Compile kernel-only n6 certificate
+      - name: Reject proof holes and trust shortcuts
+        run: |
+          set -euo pipefail
+          files=(Checkerboard.lean Checkerboard/*.lean)
+          if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then
+            echo 'Forbidden placeholder or trust shortcut found in checkerboard proof chain.' >&2
+            exit 1
+          fi
+
+      - name: Build exact all-n library
         run: |
           set -o pipefail
-          "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
+          "$HOME/.elan/bin/lake" build Checkerboard \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-alln.log"
 
-      - name: Enforce axiom policy
+      - name: Run terminal axiom audit
+        run: |
+          set -o pipefail
+          cat > CheckerboardAllNAxiomAudit.lean <<'EOF'
+          import Checkerboard.AllNTheorem
+          #print axioms Checkerboard.checkerboard_upper_all_n
+          EOF
+          "$HOME/.elan/bin/lake" env lean CheckerboardAllNAxiomAudit.lean \
+            2>&1 | tee -a "$RUNNER_TEMP/checkerboard-alln.log"
+
+      - name: Enforce final axiom policy
         run: |
           set -euo pipefail
           if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-alln.log"; then
@@ -76,11 +95,11 @@ jobs:
             exit 1
           fi
 
-      - name: Upload focused transcript
+      - name: Upload full transcript
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: checkerboard-n6-omega-${{ github.run_id }}
+          name: checkerboard-alln-full-${{ github.run_id }}
           path: |
             ${{ runner.temp }}/resolved-sha.txt
             ${{ runner.temp }}/checkerboard-alln.log

From b1a6bfce312fcd3bc5c9430342fbc34b89ea2912 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 02:15:31 -0700
Subject: [PATCH 24/43] Commit kernel-checked checkerboard n6 LRAT certificates

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 159 +++++++++++-------
 1 file changed, 101 insertions(+), 58 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index da8a501c..cb7311d7 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,5 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Full all-n audit for kernel-only source commit ddac364bedbd748af9a4b3c3f8643ee3f65e5f7d.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -13,22 +12,19 @@ on:
   workflow_dispatch:
 
 permissions:
-  contents: read
+  contents: write
 
 jobs:
-  audit:
+  certify-n6:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout exact repaired all-n source
+      - name: Checkout checkerboard proof branch
         uses: actions/checkout@v6
         with:
-          repository: DomTheDeveloper/ProofPlaygrond
-          ref: ddac364bedbd748af9a4b3c3f8643ee3f65e5f7d
-          fetch-depth: 1
-
-      - name: Record exact commit
-        run: git rev-parse HEAD | tee "$RUNNER_TEMP/resolved-sha.txt"
+          ref: migrate/checkerboard-alln-27a80067
+          fetch-depth: 0
+          token: ${{ secrets.GITHUB_TOKEN }}
 
       - name: Install repository-pinned Lean
         run: |
@@ -37,70 +33,117 @@ jobs:
             | sh -s -- -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
-      - name: Restore checkerboard Lean cache
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            .lake/packages
-            .lake/build
-          key: checkerboard-432-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.lean') }}
-          restore-keys: checkerboard-432-${{ runner.os }}-
-
-      - name: Resolve pinned Mathlib
+      - name: Resolve pinned Mathlib and cache
         run: |
           set -euo pipefail
           "$HOME/.elan/bin/lake" update
+          "$HOME/.elan/bin/lake" exe cache get
 
-      - name: Fetch Mathlib olean cache
+      - name: Restore pure BitVec SAT source
         run: |
-          set -euo pipefail
-          for attempt in 1 2 3; do
-            if "$HOME/.elan/bin/lake" exe cache get; then
-              exit 0
-            fi
-            sleep 10
-          done
-          exit 1
+          cat > Checkerboard/N6SATTest.lean <<'EOF'
+          import Mathlib
 
-      - name: Reject proof holes and trust shortcuts
-        run: |
-          set -euo pipefail
-          files=(Checkerboard.lean Checkerboard/*.lean)
-          if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then
-            echo 'Forbidden placeholder or trust shortcut found in checkerboard proof chain.' >&2
-            exit 1
-          fi
+          namespace Checkerboard
 
-      - name: Build exact all-n library
-        run: |
-          set -o pipefail
-          "$HOME/.elan/bin/lake" build Checkerboard \
-            2>&1 | tee "$RUNNER_TEMP/checkerboard-alln.log"
+          private def pop18 (x : BitVec 18) : BitVec 18 :=
+            go x 0 18
+          where
+            go (x pop : BitVec 18) : Nat → BitVec 18
+              | 0 => pop
+              | n + 1 => go (x >>> 1) (pop + (x &&& 1)) n
 
-      - name: Run terminal axiom audit
-        run: |
-          set -o pipefail
-          cat > CheckerboardAllNAxiomAudit.lean <<'EOF'
-          import Checkerboard.AllNTheorem
-          #print axioms Checkerboard.checkerboard_upper_all_n
+          private theorem p0_sat (x : BitVec 18)
+              (h0 : pop18 (x &&& 0x7#18) ≤ 2#18)
+              (h1 : pop18 (x &&& 0x38#18) ≤ 2#18)
+              (h2 : pop18 (x &&& 0x1c0#18) ≤ 2#18)
+              (h3 : pop18 (x &&& 0xe00#18) ≤ 2#18)
+              (h4 : pop18 (x &&& 0x7000#18) ≤ 2#18)
+              (h5 : pop18 (x &&& 0x38000#18) ≤ 2#18)
+              (h6 : pop18 (x &&& 0x1041#18) ≤ 2#18)
+              (h7 : pop18 (x &&& 0x2082#18) ≤ 2#18)
+              (h8 : pop18 (x &&& 0x4104#18) ≤ 2#18)
+              (h9 : pop18 (x &&& 0x8208#18) ≤ 2#18)
+              (h10 : pop18 (x &&& 0x10410#18) ≤ 2#18)
+              (h11 : pop18 (x &&& 0x20820#18) ≤ 2#18)
+              (h12 : pop18 (x &&& 0x4a#18) ≤ 2#18)
+              (h13 : pop18 (x &&& 0x1294#18) ≤ 2#18)
+              (h14 : pop18 (x &&& 0xa520#18) ≤ 2#18)
+              (h15 : pop18 (x &&& 0x14800#18) ≤ 2#18)
+              (h16 : pop18 (x &&& 0x24489#18) ≤ 2#18)
+              (h17 : pop18 (x &&& 0x912#18) ≤ 2#18)
+              (h18 : pop18 (x &&& 0x12240#18) ≤ 2#18) :
+              pop18 x ≤ 8#18 := by
+            dsimp [pop18, pop18.go] at *
+            bv_decide?
+
+          private theorem p1_sat (x : BitVec 18)
+              (h0 : pop18 (x &&& 0x7#18) ≤ 2#18)
+              (h1 : pop18 (x &&& 0x38#18) ≤ 2#18)
+              (h2 : pop18 (x &&& 0x1c0#18) ≤ 2#18)
+              (h3 : pop18 (x &&& 0xe00#18) ≤ 2#18)
+              (h4 : pop18 (x &&& 0x7000#18) ≤ 2#18)
+              (h5 : pop18 (x &&& 0x38000#18) ≤ 2#18)
+              (h6 : pop18 (x &&& 0x1041#18) ≤ 2#18)
+              (h7 : pop18 (x &&& 0x2082#18) ≤ 2#18)
+              (h8 : pop18 (x &&& 0x4104#18) ≤ 2#18)
+              (h9 : pop18 (x &&& 0x8208#18) ≤ 2#18)
+              (h10 : pop18 (x &&& 0x10410#18) ≤ 2#18)
+              (h11 : pop18 (x &&& 0x20820#18) ≤ 2#18)
+              (h12 : pop18 (x &&& 0x252#18) ≤ 2#18)
+              (h13 : pop18 (x &&& 0x94a4#18) ≤ 2#18)
+              (h14 : pop18 (x &&& 0x12900#18) ≤ 2#18)
+              (h15 : pop18 (x &&& 0x4891#18) ≤ 2#18)
+              (h16 : pop18 (x &&& 0x122#18) ≤ 2#18)
+              (h17 : pop18 (x &&& 0x22448#18) ≤ 2#18)
+              (h18 : pop18 (x &&& 0x11200#18) ≤ 2#18) :
+              pop18 x ≤ 8#18 := by
+            dsimp [pop18, pop18.go] at *
+            bv_decide?
+
+          end Checkerboard
           EOF
-          "$HOME/.elan/bin/lake" env lean CheckerboardAllNAxiomAudit.lean \
-            2>&1 | tee -a "$RUNNER_TEMP/checkerboard-alln.log"
 
-      - name: Enforce final axiom policy
+      - name: Generate, rename, and verify LRAT certificates
         run: |
           set -euo pipefail
-          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-alln.log"; then
-            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
+          "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean
+          p0=$(find Checkerboard -maxdepth 1 -name '*p0_sat*.lrat' -print -quit)
+          p1=$(find Checkerboard -maxdepth 1 -name '*p1_sat*.lrat' -print -quit)
+          test -n "$p0" && test -n "$p1"
+          mv "$p0" Checkerboard/N6P0.lrat
+          mv "$p1" Checkerboard/N6P1.lrat
+          python3 - <<'PY'
+          from pathlib import Path
+          p = Path('Checkerboard/N6SATTest.lean')
+          text = p.read_text()
+          text = text.replace('bv_decide?', 'bv_check "N6P0.lrat"', 1)
+          text = text.replace('bv_decide?', 'bv_check "N6P1.lrat"', 1)
+          text = text.replace('\nend Checkerboard\n', '\n#print axioms p0_sat\n#print axioms p1_sat\n\nend Checkerboard\n')
+          p.write_text(text)
+          PY
+          "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
+            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-bvcheck.log"
+          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' \
+              "$RUNNER_TEMP/checkerboard-n6-bvcheck.log"; then
+            echo 'Forbidden trust dependency detected.' >&2
             exit 1
           fi
 
-      - name: Upload full transcript
+      - name: Commit certificate and checked source
+        run: |
+          set -euo pipefail
+          git config user.name 'ProofOrchestrator'
+          git config user.email 'proof-orchestrator@users.noreply.github.com'
+          git add Checkerboard/N6SATTest.lean Checkerboard/N6P0.lrat Checkerboard/N6P1.lrat
+          git diff --cached --check
+          git commit -m 'Add kernel-checked n6 checkerboard LRAT certificates'
+          git push origin HEAD:migrate/checkerboard-alln-27a80067
+
+      - name: Upload verification transcript
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: checkerboard-alln-full-${{ github.run_id }}
-          path: |
-            ${{ runner.temp }}/resolved-sha.txt
-            ${{ runner.temp }}/checkerboard-alln.log
+          name: checkerboard-n6-bvcheck-${{ github.run_id }}
+          path: ${{ runner.temp }}/checkerboard-n6-bvcheck.log
           if-no-files-found: warn

From 3addd2c3fea8b3c4dc88a6f7b26816c0a55f5ac1 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 02:23:12 -0700
Subject: [PATCH 25/43] Audit pure omega bridge for checkerboard n6

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 132 ++++--------------
 1 file changed, 30 insertions(+), 102 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index cb7311d7..b34badc4 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,5 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
+# Focused pure-kernel bridge audit for source commit 0b6ac8fe2444f8b42a871cb397d276b36829a5e9.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -12,19 +13,22 @@ on:
   workflow_dispatch:
 
 permissions:
-  contents: write
+  contents: read
 
 jobs:
-  certify-n6:
+  audit:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout checkerboard proof branch
+      - name: Checkout exact omega bridge source
         uses: actions/checkout@v6
         with:
-          ref: migrate/checkerboard-alln-27a80067
-          fetch-depth: 0
-          token: ${{ secrets.GITHUB_TOKEN }}
+          repository: DomTheDeveloper/ProofPlaygrond
+          ref: 0b6ac8fe2444f8b42a871cb397d276b36829a5e9
+          fetch-depth: 1
+
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/resolved-sha.txt"
 
       - name: Install repository-pinned Lean
         run: |
@@ -39,111 +43,35 @@ jobs:
           "$HOME/.elan/bin/lake" update
           "$HOME/.elan/bin/lake" exe cache get
 
-      - name: Restore pure BitVec SAT source
-        run: |
-          cat > Checkerboard/N6SATTest.lean <<'EOF'
-          import Mathlib
-
-          namespace Checkerboard
-
-          private def pop18 (x : BitVec 18) : BitVec 18 :=
-            go x 0 18
-          where
-            go (x pop : BitVec 18) : Nat → BitVec 18
-              | 0 => pop
-              | n + 1 => go (x >>> 1) (pop + (x &&& 1)) n
-
-          private theorem p0_sat (x : BitVec 18)
-              (h0 : pop18 (x &&& 0x7#18) ≤ 2#18)
-              (h1 : pop18 (x &&& 0x38#18) ≤ 2#18)
-              (h2 : pop18 (x &&& 0x1c0#18) ≤ 2#18)
-              (h3 : pop18 (x &&& 0xe00#18) ≤ 2#18)
-              (h4 : pop18 (x &&& 0x7000#18) ≤ 2#18)
-              (h5 : pop18 (x &&& 0x38000#18) ≤ 2#18)
-              (h6 : pop18 (x &&& 0x1041#18) ≤ 2#18)
-              (h7 : pop18 (x &&& 0x2082#18) ≤ 2#18)
-              (h8 : pop18 (x &&& 0x4104#18) ≤ 2#18)
-              (h9 : pop18 (x &&& 0x8208#18) ≤ 2#18)
-              (h10 : pop18 (x &&& 0x10410#18) ≤ 2#18)
-              (h11 : pop18 (x &&& 0x20820#18) ≤ 2#18)
-              (h12 : pop18 (x &&& 0x4a#18) ≤ 2#18)
-              (h13 : pop18 (x &&& 0x1294#18) ≤ 2#18)
-              (h14 : pop18 (x &&& 0xa520#18) ≤ 2#18)
-              (h15 : pop18 (x &&& 0x14800#18) ≤ 2#18)
-              (h16 : pop18 (x &&& 0x24489#18) ≤ 2#18)
-              (h17 : pop18 (x &&& 0x912#18) ≤ 2#18)
-              (h18 : pop18 (x &&& 0x12240#18) ≤ 2#18) :
-              pop18 x ≤ 8#18 := by
-            dsimp [pop18, pop18.go] at *
-            bv_decide?
-
-          private theorem p1_sat (x : BitVec 18)
-              (h0 : pop18 (x &&& 0x7#18) ≤ 2#18)
-              (h1 : pop18 (x &&& 0x38#18) ≤ 2#18)
-              (h2 : pop18 (x &&& 0x1c0#18) ≤ 2#18)
-              (h3 : pop18 (x &&& 0xe00#18) ≤ 2#18)
-              (h4 : pop18 (x &&& 0x7000#18) ≤ 2#18)
-              (h5 : pop18 (x &&& 0x38000#18) ≤ 2#18)
-              (h6 : pop18 (x &&& 0x1041#18) ≤ 2#18)
-              (h7 : pop18 (x &&& 0x2082#18) ≤ 2#18)
-              (h8 : pop18 (x &&& 0x4104#18) ≤ 2#18)
-              (h9 : pop18 (x &&& 0x8208#18) ≤ 2#18)
-              (h10 : pop18 (x &&& 0x10410#18) ≤ 2#18)
-              (h11 : pop18 (x &&& 0x20820#18) ≤ 2#18)
-              (h12 : pop18 (x &&& 0x252#18) ≤ 2#18)
-              (h13 : pop18 (x &&& 0x94a4#18) ≤ 2#18)
-              (h14 : pop18 (x &&& 0x12900#18) ≤ 2#18)
-              (h15 : pop18 (x &&& 0x4891#18) ≤ 2#18)
-              (h16 : pop18 (x &&& 0x122#18) ≤ 2#18)
-              (h17 : pop18 (x &&& 0x22448#18) ≤ 2#18)
-              (h18 : pop18 (x &&& 0x11200#18) ≤ 2#18) :
-              pop18 x ≤ 8#18 := by
-            dsimp [pop18, pop18.go] at *
-            bv_decide?
-
-          end Checkerboard
-          EOF
-
-      - name: Generate, rename, and verify LRAT certificates
+      - name: Reject proof holes and trust shortcuts
         run: |
           set -euo pipefail
-          "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean
-          p0=$(find Checkerboard -maxdepth 1 -name '*p0_sat*.lrat' -print -quit)
-          p1=$(find Checkerboard -maxdepth 1 -name '*p1_sat*.lrat' -print -quit)
-          test -n "$p0" && test -n "$p1"
-          mv "$p0" Checkerboard/N6P0.lrat
-          mv "$p1" Checkerboard/N6P1.lrat
-          python3 - <<'PY'
-          from pathlib import Path
-          p = Path('Checkerboard/N6SATTest.lean')
-          text = p.read_text()
-          text = text.replace('bv_decide?', 'bv_check "N6P0.lrat"', 1)
-          text = text.replace('bv_decide?', 'bv_check "N6P1.lrat"', 1)
-          text = text.replace('\nend Checkerboard\n', '\n#print axioms p0_sat\n#print axioms p1_sat\n\nend Checkerboard\n')
-          p.write_text(text)
-          PY
-          "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
-            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-bvcheck.log"
-          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' \
-              "$RUNNER_TEMP/checkerboard-n6-bvcheck.log"; then
-            echo 'Forbidden trust dependency detected.' >&2
+          files=(Checkerboard/N6SATTest.lean Checkerboard/N6BridgeTest.lean)
+          if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|bv_decide|bv_check|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then
+            echo 'Forbidden placeholder or trust shortcut found in checkerboard bridge.' >&2
             exit 1
           fi
 
-      - name: Commit certificate and checked source
+      - name: Compile omega certificate bridge
+        run: |
+          set -o pipefail
+          "$HOME/.elan/bin/lake" env lean Checkerboard/N6BridgeTest.lean \
+            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-bridge.log"
+
+      - name: Enforce axiom policy
         run: |
           set -euo pipefail
-          git config user.name 'ProofOrchestrator'
-          git config user.email 'proof-orchestrator@users.noreply.github.com'
-          git add Checkerboard/N6SATTest.lean Checkerboard/N6P0.lrat Checkerboard/N6P1.lrat
-          git diff --cached --check
-          git commit -m 'Add kernel-checked n6 checkerboard LRAT certificates'
-          git push origin HEAD:migrate/checkerboard-alln-27a80067
+          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-n6-bridge.log"; then
+            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
+            exit 1
+          fi
 
-      - name: Upload verification transcript
+      - name: Upload bridge transcript
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: checkerboard-n6-bvcheck-${{ github.run_id }}
-          path: ${{ runner.temp }}/checkerboard-n6-bvcheck.log
+          name: checkerboard-n6-bridge-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/resolved-sha.txt
+            ${{ runner.temp }}/checkerboard-n6-bridge.log
           if-no-files-found: warn

From c71edc9c00da0916ca67ddfc16d0f0174a85aadd Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 02:27:06 -0700
Subject: [PATCH 26/43] Audit checkerboard bv_omega bridge at 4738bccd

---
 .../workflows/checkerboard-alln-proofplaygrond-audit.yml  | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index b34badc4..b5b5e34b 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused pure-kernel bridge audit for source commit 0b6ac8fe2444f8b42a871cb397d276b36829a5e9.
+# Focused pure-kernel bridge audit for source commit 4738bccd062f9e6d744ac81da2cef598e1b5303b.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -20,11 +20,11 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout exact omega bridge source
+      - name: Checkout exact checkerboard bridge source
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 0b6ac8fe2444f8b42a871cb397d276b36829a5e9
+          ref: 4738bccd062f9e6d744ac81da2cef598e1b5303b
           fetch-depth: 1
 
       - name: Record exact commit
@@ -52,7 +52,7 @@ jobs:
             exit 1
           fi
 
-      - name: Compile omega certificate bridge
+      - name: Compile bv_omega certificate bridge
         run: |
           set -o pipefail
           "$HOME/.elan/bin/lake" env lean Checkerboard/N6BridgeTest.lean \

From eb5e7fc238cd1d42c769f66c548cd053bf0e31e3 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 02:28:02 -0700
Subject: [PATCH 27/43] Build checkerboard omega bridge through Lake

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index b5b5e34b..46268652 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -52,10 +52,10 @@ jobs:
             exit 1
           fi
 
-      - name: Compile bv_omega certificate bridge
+      - name: Build omega certificate bridge through Lake
         run: |
           set -o pipefail
-          "$HOME/.elan/bin/lake" env lean Checkerboard/N6BridgeTest.lean \
+          "$HOME/.elan/bin/lake" build Checkerboard.N6BridgeTest \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-bridge.log"
 
       - name: Enforce axiom policy

From 26cb96c4525eef6f09f494294721329a1962d21f Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 02:37:41 -0700
Subject: [PATCH 28/43] Pin checkerboard audit to both n6 color bridges

---
 .../workflows/checkerboard-alln-proofplaygrond-audit.yml    | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 46268652..9db7cee0 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused pure-kernel bridge audit for source commit 4738bccd062f9e6d744ac81da2cef598e1b5303b.
+# Focused pure-kernel bridge audit for source commit b2c96dd991abcf06da14ea35b19a5a319b036511.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 4738bccd062f9e6d744ac81da2cef598e1b5303b
+          ref: b2c96dd991abcf06da14ea35b19a5a319b036511
           fetch-depth: 1
 
       - name: Record exact commit
@@ -52,7 +52,7 @@ jobs:
             exit 1
           fi
 
-      - name: Build omega certificate bridge through Lake
+      - name: Build both omega certificate bridges through Lake
         run: |
           set -o pipefail
           "$HOME/.elan/bin/lake" build Checkerboard.N6BridgeTest \

From 7412aabe24a699faf21d05c000f1e18ed3b46d59 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 02:45:10 -0700
Subject: [PATCH 29/43] Capture checkerboard bridge compiler transcript

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 31 ++++++++++++-------
 1 file changed, 20 insertions(+), 11 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 9db7cee0..f76f4691 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused pure-kernel bridge audit for source commit b2c96dd991abcf06da14ea35b19a5a319b036511.
+# Diagnostic pure-kernel bridge audit for source commit b2c96dd991abcf06da14ea35b19a5a319b036511.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -52,19 +52,18 @@ jobs:
             exit 1
           fi
 
-      - name: Build both omega certificate bridges through Lake
+      - name: Build bridge dependencies
         run: |
-          set -o pipefail
-          "$HOME/.elan/bin/lake" build Checkerboard.N6BridgeTest \
-            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-bridge.log"
+          set -euo pipefail
+          "$HOME/.elan/bin/lake" build Checkerboard.FourCertificate Checkerboard.N6SATTest
 
-      - name: Enforce axiom policy
+      - name: Compile both omega certificate bridges
+        id: compile
+        continue-on-error: true
         run: |
-          set -euo pipefail
-          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-n6-bridge.log"; then
-            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
-            exit 1
-          fi
+          set -o pipefail
+          "$HOME/.elan/bin/lake" env lean Checkerboard/N6BridgeTest.lean \
+            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-bridge.log"
 
       - name: Upload bridge transcript
         if: always()
@@ -75,3 +74,13 @@ jobs:
             ${{ runner.temp }}/resolved-sha.txt
             ${{ runner.temp }}/checkerboard-n6-bridge.log
           if-no-files-found: warn
+
+      - name: Enforce result and axiom policy
+        if: always()
+        run: |
+          set -euo pipefail
+          test '${{ steps.compile.outcome }}' = 'success'
+          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-n6-bridge.log"; then
+            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
+            exit 1
+          fi

From 683d5b35688d887164cb896b4dc21c8138b36703 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 03:13:34 -0700
Subject: [PATCH 30/43] Capture checkerboard arithmetic certificate failure
 exactly

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 34 +++++++++++++------
 1 file changed, 23 insertions(+), 11 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index f76f4691..a0a321d4 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Diagnostic pure-kernel bridge audit for source commit b2c96dd991abcf06da14ea35b19a5a319b036511.
+# Isolated arithmetic-certificate diagnostic for source commit b2c96dd991abcf06da14ea35b19a5a319b036511.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -20,7 +20,7 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 120
     steps:
-      - name: Checkout exact checkerboard bridge source
+      - name: Checkout exact checkerboard certificate source
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
@@ -48,30 +48,40 @@ jobs:
           set -euo pipefail
           files=(Checkerboard/N6SATTest.lean Checkerboard/N6BridgeTest.lean)
           if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|bv_decide|bv_check|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then
-            echo 'Forbidden placeholder or trust shortcut found in checkerboard bridge.' >&2
+            echo 'Forbidden placeholder or trust shortcut found in checkerboard certificate.' >&2
             exit 1
           fi
 
-      - name: Build bridge dependencies
+      - name: Build geometric dependency
         run: |
           set -euo pipefail
-          "$HOME/.elan/bin/lake" build Checkerboard.FourCertificate Checkerboard.N6SATTest
+          "$HOME/.elan/bin/lake" build Checkerboard.FourCertificate
 
-      - name: Compile both omega certificate bridges
-        id: compile
+      - name: Compile arithmetic certificate with transcript
+        id: sat
+        continue-on-error: true
+        run: |
+          set -o pipefail
+          "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
+            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-sat.log"
+
+      - name: Compile geometric bridge when certificate succeeds
+        id: bridge
+        if: steps.sat.outcome == 'success'
         continue-on-error: true
         run: |
           set -o pipefail
           "$HOME/.elan/bin/lake" env lean Checkerboard/N6BridgeTest.lean \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-bridge.log"
 
-      - name: Upload bridge transcript
+      - name: Upload all diagnostic transcripts
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: checkerboard-n6-bridge-${{ github.run_id }}
+          name: checkerboard-n6-diagnostic-${{ github.run_id }}
           path: |
             ${{ runner.temp }}/resolved-sha.txt
+            ${{ runner.temp }}/checkerboard-n6-sat.log
             ${{ runner.temp }}/checkerboard-n6-bridge.log
           if-no-files-found: warn
 
@@ -79,8 +89,10 @@ jobs:
         if: always()
         run: |
           set -euo pipefail
-          test '${{ steps.compile.outcome }}' = 'success'
-          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-n6-bridge.log"; then
+          test '${{ steps.sat.outcome }}' = 'success'
+          test '${{ steps.bridge.outcome }}' = 'success'
+          cat "$RUNNER_TEMP/checkerboard-n6-sat.log" "$RUNNER_TEMP/checkerboard-n6-bridge.log" > "$RUNNER_TEMP/checkerboard-n6-all.log"
+          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-n6-all.log"; then
             echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
             exit 1
           fi

From 20887f6f58db89ba546d05688a23d1defa16486c Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 03:24:56 -0700
Subject: [PATCH 31/43] Run checkerboard bridge unconditionally

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 36 ++++++++-----------
 1 file changed, 14 insertions(+), 22 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index a0a321d4..22675579 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Isolated arithmetic-certificate diagnostic for source commit b2c96dd991abcf06da14ea35b19a5a319b036511.
+# Trust-free arithmetic and bridge audit for source commit b2c96dd991abcf06da14ea35b19a5a319b036511.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -57,42 +57,34 @@ jobs:
           set -euo pipefail
           "$HOME/.elan/bin/lake" build Checkerboard.FourCertificate
 
-      - name: Compile arithmetic certificate with transcript
-        id: sat
-        continue-on-error: true
+      - name: Compile arithmetic certificate
         run: |
           set -o pipefail
           "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-sat.log"
 
-      - name: Compile geometric bridge when certificate succeeds
-        id: bridge
-        if: steps.sat.outcome == 'success'
-        continue-on-error: true
+      - name: Compile both geometric bridges
         run: |
           set -o pipefail
           "$HOME/.elan/bin/lake" env lean Checkerboard/N6BridgeTest.lean \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-bridge.log"
 
-      - name: Upload all diagnostic transcripts
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          cat "$RUNNER_TEMP/checkerboard-n6-sat.log" "$RUNNER_TEMP/checkerboard-n6-bridge.log" > "$RUNNER_TEMP/checkerboard-n6-all.log"
+          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-n6-all.log"; then
+            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
+            exit 1
+          fi
+
+      - name: Upload certificate transcripts
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: checkerboard-n6-diagnostic-${{ github.run_id }}
+          name: checkerboard-n6-certificate-${{ github.run_id }}
           path: |
             ${{ runner.temp }}/resolved-sha.txt
             ${{ runner.temp }}/checkerboard-n6-sat.log
             ${{ runner.temp }}/checkerboard-n6-bridge.log
           if-no-files-found: warn
-
-      - name: Enforce result and axiom policy
-        if: always()
-        run: |
-          set -euo pipefail
-          test '${{ steps.sat.outcome }}' = 'success'
-          test '${{ steps.bridge.outcome }}' = 'success'
-          cat "$RUNNER_TEMP/checkerboard-n6-sat.log" "$RUNNER_TEMP/checkerboard-n6-bridge.log" > "$RUNNER_TEMP/checkerboard-n6-all.log"
-          if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-n6-all.log"; then
-            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
-            exit 1
-          fi

From 1bf12a16906ccf3d8c87ff97cc223674058cdf22 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 10:29:55 -0700
Subject: [PATCH 32/43] Audit repaired checkerboard n6 certificate

---
 .../workflows/checkerboard-alln-proofplaygrond-audit.yml    | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 22675579..9f004a7f 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Trust-free arithmetic and bridge audit for source commit b2c96dd991abcf06da14ea35b19a5a319b036511.
+# Focused arithmetic and bridge audit for source commit 108f18a86c6388ab0b1996d8621e0b4113b83195.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: b2c96dd991abcf06da14ea35b19a5a319b036511
+          ref: 108f18a86c6388ab0b1996d8621e0b4113b83195
           fetch-depth: 1
 
       - name: Record exact commit
@@ -79,7 +79,7 @@ jobs:
           fi
 
       - name: Upload certificate transcripts
-        if: always()
+        if: ${{ always() }}
         uses: actions/upload-artifact@v4
         with:
           name: checkerboard-n6-certificate-${{ github.run_id }}

From 3721e1818770ba267ebd9e14b94cf028972b6f27 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 10:37:17 -0700
Subject: [PATCH 33/43] Audit split checkerboard n6 certificates

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 9f004a7f..df5fafdc 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused arithmetic and bridge audit for source commit 108f18a86c6388ab0b1996d8621e0b4113b83195.
+# Focused arithmetic and bridge audit for source commit bb9e424da60caa687e45303361e5ee43d27c3430.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 108f18a86c6388ab0b1996d8621e0b4113b83195
+          ref: bb9e424da60caa687e45303361e5ee43d27c3430
           fetch-depth: 1
 
       - name: Record exact commit

From 47505835729bc5565928d42d21e178ea3d7917f6 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 10:42:00 -0700
Subject: [PATCH 34/43] Audit opaque checkerboard n6 indicators

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index df5fafdc..e2ae29ae 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused arithmetic and bridge audit for source commit bb9e424da60caa687e45303361e5ee43d27c3430.
+# Focused arithmetic and bridge audit for source commit ad1baeac925239fa830496fc3169e9f057748c50.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: bb9e424da60caa687e45303361e5ee43d27c3430
+          ref: ad1baeac925239fa830496fc3169e9f057748c50
           fetch-depth: 1
 
       - name: Record exact commit

From 45e80bedd04632386249baa606a079998b0d2fa1 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 10:46:54 -0700
Subject: [PATCH 35/43] Audit sparse checkerboard n6 supports

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index e2ae29ae..09e1868e 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused arithmetic and bridge audit for source commit ad1baeac925239fa830496fc3169e9f057748c50.
+# Focused arithmetic and bridge audit for source commit 100efa954491eb2c201796d251764d94dbb65edf.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: ad1baeac925239fa830496fc3169e9f057748c50
+          ref: 100efa954491eb2c201796d251764d94dbb65edf
           fetch-depth: 1
 
       - name: Record exact commit

From 5d9951fa46d1fb339a0d694245facdd433ed6d70 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 10:50:56 -0700
Subject: [PATCH 36/43] Build checkerboard n6 certificate module before bridge

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 09e1868e..efd44a5d 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -57,10 +57,10 @@ jobs:
           set -euo pipefail
           "$HOME/.elan/bin/lake" build Checkerboard.FourCertificate
 
-      - name: Compile arithmetic certificate
+      - name: Build arithmetic certificate module
         run: |
           set -o pipefail
-          "$HOME/.elan/bin/lake" env lean Checkerboard/N6SATTest.lean \
+          "$HOME/.elan/bin/lake" build Checkerboard.N6SATTest \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-sat.log"
 
       - name: Compile both geometric bridges

From 860e6fa47810b1535e88f727a7e9bedd4ce027f9 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 10:52:43 -0700
Subject: [PATCH 37/43] Audit checkerboard compatibility repairs

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index efd44a5d..66a4b09f 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused arithmetic and bridge audit for source commit 100efa954491eb2c201796d251764d94dbb65edf.
+# Focused arithmetic and bridge audit for source commit 2151891ca7ed01b573139491a6e20c59dac729a2.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 100efa954491eb2c201796d251764d94dbb65edf
+          ref: 2151891ca7ed01b573139491a6e20c59dac729a2
           fetch-depth: 1
 
       - name: Record exact commit

From ed7c2db2bec4f20e75bcfa368ce1c14ffc1a3e94 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 10:57:51 -0700
Subject: [PATCH 38/43] Audit checkerboard Boolean-card bridge

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 66a4b09f..10651610 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused arithmetic and bridge audit for source commit 2151891ca7ed01b573139491a6e20c59dac729a2.
+# Focused arithmetic and bridge audit for source commit 5fa90d646295dfc48baef23a90fe1e2883366ec5.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 2151891ca7ed01b573139491a6e20c59dac729a2
+          ref: 5fa90d646295dfc48baef23a90fe1e2883366ec5
           fetch-depth: 1
 
       - name: Record exact commit

From f03338ac8b352996ceb004b088d9abb25080164b Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 10:58:33 -0700
Subject: [PATCH 39/43] Audit production checkerboard n6 module

---
 ...checkerboard-alln-proofplaygrond-audit.yml | 33 ++++++++++---------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 10651610..2995bf6d 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused arithmetic and bridge audit for source commit 5fa90d646295dfc48baef23a90fe1e2883366ec5.
+# Focused 6×6 production-module audit for source commit 5fa90d646295dfc48baef23a90fe1e2883366ec5.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -46,33 +46,34 @@ jobs:
       - name: Reject proof holes and trust shortcuts
         run: |
           set -euo pipefail
-          files=(Checkerboard/N6SATTest.lean Checkerboard/N6BridgeTest.lean)
+          files=(Checkerboard/N6SATTest.lean Checkerboard/N6Base.lean)
           if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|bv_decide|bv_check|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then
             echo 'Forbidden placeholder or trust shortcut found in checkerboard certificate.' >&2
             exit 1
           fi
 
-      - name: Build geometric dependency
-        run: |
-          set -euo pipefail
-          "$HOME/.elan/bin/lake" build Checkerboard.FourCertificate
-
-      - name: Build arithmetic certificate module
+      - name: Build production 6x6 proof
         run: |
           set -o pipefail
-          "$HOME/.elan/bin/lake" build Checkerboard.N6SATTest \
-            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-sat.log"
+          "$HOME/.elan/bin/lake" build Checkerboard.N6Base \
+            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-build.log"
 
-      - name: Compile both geometric bridges
+      - name: Print public base-case axioms
         run: |
+          set -euo pipefail
+          cat > "$RUNNER_TEMP/CheckerboardN6AxiomAudit.lean" <<'EOF'
+          import Checkerboard.N6Base
+          #print axioms Checkerboard.n6_zero_upper
+          #print axioms Checkerboard.n6_one_upper
+          EOF
           set -o pipefail
-          "$HOME/.elan/bin/lake" env lean Checkerboard/N6BridgeTest.lean \
-            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-bridge.log"
+          "$HOME/.elan/bin/lake" env lean "$RUNNER_TEMP/CheckerboardN6AxiomAudit.lean" \
+            2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-axioms.log"
 
       - name: Enforce axiom policy
         run: |
           set -euo pipefail
-          cat "$RUNNER_TEMP/checkerboard-n6-sat.log" "$RUNNER_TEMP/checkerboard-n6-bridge.log" > "$RUNNER_TEMP/checkerboard-n6-all.log"
+          cat "$RUNNER_TEMP/checkerboard-n6-build.log" "$RUNNER_TEMP/checkerboard-n6-axioms.log" > "$RUNNER_TEMP/checkerboard-n6-all.log"
           if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-n6-all.log"; then
             echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
             exit 1
@@ -85,6 +86,6 @@ jobs:
           name: checkerboard-n6-certificate-${{ github.run_id }}
           path: |
             ${{ runner.temp }}/resolved-sha.txt
-            ${{ runner.temp }}/checkerboard-n6-sat.log
-            ${{ runner.temp }}/checkerboard-n6-bridge.log
+            ${{ runner.temp }}/checkerboard-n6-build.log
+            ${{ runner.temp }}/checkerboard-n6-axioms.log
           if-no-files-found: warn

From c13e93d3bdbe4e291255dfb076bb28111cace7f6 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 11:02:28 -0700
Subject: [PATCH 40/43] Audit checkerboard finite-sum scope repair

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 2995bf6d..2ba650c2 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused 6×6 production-module audit for source commit 5fa90d646295dfc48baef23a90fe1e2883366ec5.
+# Focused 6×6 production-module audit for source commit 4bee2a930d94250c444f32bd7f055ca7d54f255a.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 5fa90d646295dfc48baef23a90fe1e2883366ec5
+          ref: 4bee2a930d94250c444f32bd7f055ca7d54f255a
           fetch-depth: 1
 
       - name: Record exact commit

From 9b444c3ccfc8097ad23176a066f2d2c7d2d583cf Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 11:06:45 -0700
Subject: [PATCH 41/43] Audit explicit Finset sums in checkerboard n6 bridge

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 2ba650c2..dd5233e3 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused 6×6 production-module audit for source commit 4bee2a930d94250c444f32bd7f055ca7d54f255a.
+# Focused 6×6 production-module audit for source commit 09ec4378778afaa244a8b8d01e6a47c2989b2f34.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 4bee2a930d94250c444f32bd7f055ca7d54f255a
+          ref: 09ec4378778afaa244a8b8d01e6a47c2989b2f34
           fetch-depth: 1
 
       - name: Record exact commit

From 7b361d21fcad215f13608aed338e372d109758ee Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 11:17:46 -0700
Subject: [PATCH 42/43] Audit explicit checkerboard n6 bridge

---
 .../checkerboard-alln-proofplaygrond-audit.yml         | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index dd5233e3..6aea4e6c 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused 6×6 production-module audit for source commit 09ec4378778afaa244a8b8d01e6a47c2989b2f34.
+# Focused 6×6 production-module audit for source commit 865f796eb97fa53fc17820be2478d4268b7b5363.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 09ec4378778afaa244a8b8d01e6a47c2989b2f34
+          ref: 865f796eb97fa53fc17820be2478d4268b7b5363
           fetch-depth: 1
 
       - name: Record exact commit
@@ -46,7 +46,7 @@ jobs:
       - name: Reject proof holes and trust shortcuts
         run: |
           set -euo pipefail
-          files=(Checkerboard/N6SATTest.lean Checkerboard/N6Base.lean)
+          files=(Checkerboard/N6SATTest.lean Checkerboard/N6Explicit.lean)
           if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|bv_decide|bv_check|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then
             echo 'Forbidden placeholder or trust shortcut found in checkerboard certificate.' >&2
             exit 1
@@ -55,14 +55,14 @@ jobs:
       - name: Build production 6x6 proof
         run: |
           set -o pipefail
-          "$HOME/.elan/bin/lake" build Checkerboard.N6Base \
+          "$HOME/.elan/bin/lake" build Checkerboard.N6Explicit \
             2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-build.log"
 
       - name: Print public base-case axioms
         run: |
           set -euo pipefail
           cat > "$RUNNER_TEMP/CheckerboardN6AxiomAudit.lean" <<'EOF'
-          import Checkerboard.N6Base
+          import Checkerboard.N6Explicit
           #print axioms Checkerboard.n6_zero_upper
           #print axioms Checkerboard.n6_one_upper
           EOF

From d4aa8ba938a80c4dd17fdb77c7b35f0090d335b9 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Thu, 23 Jul 2026 11:21:37 -0700
Subject: [PATCH 43/43] Audit normalized explicit checkerboard bridge

---
 .github/workflows/checkerboard-alln-proofplaygrond-audit.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
index 6aea4e6c..062af9c0 100644
--- a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
+++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml
@@ -1,6 +1,6 @@
 # Copyright 2026 Dominic Dabish
 # Licensed under the Apache License, Version 2.0.
-# Focused 6×6 production-module audit for source commit 865f796eb97fa53fc17820be2478d4268b7b5363.
+# Focused 6×6 production-module audit for source commit 913adfd724cbedd5c47b52a2c538a94a7c7cf785.
 
 name: Checkerboard all-n ProofPlaygrond audit
 
@@ -24,7 +24,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: DomTheDeveloper/ProofPlaygrond
-          ref: 865f796eb97fa53fc17820be2478d4268b7b5363
+          ref: 913adfd724cbedd5c47b52a2c538a94a7c7cf785
           fetch-depth: 1
 
       - name: Record exact commit