Prove the dimension-2 and dimension-3 SIC-POVM benchmarks

.github/workflows/sic-low-dim-audit.yml

@@ -0,0 +1,83 @@
+name: SIC low-dimensional proof audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/sic-low-dim-audit.yml'
+      - 'FormalConjectures/OpenQuantumProblems/23.lean'
+
+concurrency:
+  group: sic-low-dimensional-proof-audit
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    steps:
+      - uses: actions/checkout@v6
+        with:
+          fetch-depth: 1
+      - name: Install Lean
+        run: |
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: sic-low-dim-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: sic-low-dim-${{ runner.os }}-${{ runner.arch }}-
+      - name: Get Mathlib cache
+        run: |
+          set -euo pipefail
+          for attempt in 1 2 3; do
+            lake exe cache get && exit 0
+            sleep 10
+          done
+          exit 1
+      - name: Build exact local import dependency
+        run: |
+          set -o pipefail
+          lake build FormalConjectures.Util.ProblemImports 2>&1 | tee /tmp/sic-low-dim-dependency.log
+      # Compile the canonical numeric module directly; Lake target syntax treats `23` as a path.
+      - name: Compile canonical module
+        run: |
+          set -o pipefail
+          lake env lean FormalConjectures/OpenQuantumProblems/23.lean 2>&1 | tee /tmp/sic-low-dim-compile.log
+      - name: Audit canonical theorem axioms in the same compilation
+        if: success()
+        run: |
+          cp FormalConjectures/OpenQuantumProblems/23.lean /tmp/SICLowDimCanonicalAudit.lean
+          cat >> /tmp/SICLowDimCanonicalAudit.lean <<'EOF'
+
+          #print axioms OpenQuantumProblem23.qubitSICFamily_pairwise
+          #print axioms OpenQuantumProblem23.hasSICPOVM_two
+          #print axioms OpenQuantumProblem23.hesseFamily_pairwise
+          #print axioms OpenQuantumProblem23.hasSICPOVM_three
+          EOF
+          lake env lean /tmp/SICLowDimCanonicalAudit.lean 2>&1 | tee /tmp/sic-low-dim-axioms.log
+          ! grep -E 'sorryAx|Lean\.ofReduceBool|Lean\.trustCompiler' /tmp/sic-low-dim-axioms.log
+      - name: Save partial build cache
+        if: always()
+        uses: actions/cache/save@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: sic-low-dim-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+      - name: Upload diagnostics
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: sic-low-dim-${{ github.run_id }}
+          path: |
+            /tmp/sic-low-dim-dependency.log
+            /tmp/sic-low-dim-compile.log
+            /tmp/sic-low-dim-axioms.log
+          if-no-files-found: warn