Focused audit: repaired checkerboard n6 arithmetic certificate

.github/workflows/checkerboard-alln-proofplaygrond-audit.yml

@@ -0,0 +1,91 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+# Focused 6×6 production-module audit for source commit 913adfd724cbedd5c47b52a2c538a94a7c7cf785.
+
+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 checkerboard certificate source
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/ProofPlaygrond
+          ref: 913adfd724cbedd5c47b52a2c538a94a7c7cf785
+          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: Resolve pinned Mathlib and cache
+        run: |
+          set -euo pipefail
+          "$HOME/.elan/bin/lake" update
+          "$HOME/.elan/bin/lake" exe cache get
+
+      - name: Reject proof holes and trust shortcuts
+        run: |
+          set -euo pipefail
+          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
+          fi
+
+      - name: Build production 6x6 proof
+        run: |
+          set -o pipefail
+          "$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.N6Explicit
+          #print axioms Checkerboard.n6_zero_upper
+          #print axioms Checkerboard.n6_one_upper
+          EOF
+          set -o pipefail
+          "$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-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
+          fi
+
+      - name: Upload certificate transcripts
+        if: ${{ always() }}
+        uses: actions/upload-artifact@v4
+        with:
+          name: checkerboard-n6-certificate-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/resolved-sha.txt
+            ${{ runner.temp }}/checkerboard-n6-build.log
+            ${{ runner.temp }}/checkerboard-n6-axioms.log
+          if-no-files-found: warn