From 1b06017515d7d5102b160a8e2739771a9dba4e9d Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:21:27 -0700 Subject: [PATCH 1/5] ci: audit immutable SIC proof branch --- .../workflows/openai-sic-immutable-audit.yml | 59 +++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 .github/workflows/openai-sic-immutable-audit.yml diff --git a/.github/workflows/openai-sic-immutable-audit.yml b/.github/workflows/openai-sic-immutable-audit.yml new file mode 100644 index 0000000000..7b20e12307 --- /dev/null +++ b/.github/workflows/openai-sic-immutable-audit.yml @@ -0,0 +1,59 @@ +name: OpenAI immutable SIC proof audit + +on: + pull_request: + branches: [main] + paths: + - '.github/workflows/openai-sic-immutable-audit.yml' + +permissions: + contents: read + +jobs: + audit: + runs-on: ubuntu-latest + timeout-minutes: 50 + steps: + - uses: actions/checkout@v6 + with: + ref: 7aeef3c2aca76d413f94d13ebf6044e9b6c1d712 + fetch-depth: 1 + - name: Confirm immutable SIC proof commit + run: test "$(git rev-parse HEAD)" = 7aeef3c2aca76d413f94d13ebf6044e9b6c1d712 + - name: Install pinned Lean toolchain + 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-immutable-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }} + restore-keys: sic-immutable-${{ runner.os }}-${{ runner.arch }}- + - name: Fetch compiled dependencies + run: lake exe cache get + - name: Compile exact canonical source + run: | + set -o pipefail + lake env lean FormalConjectures/OpenQuantumProblems/23.lean 2>&1 | tee /tmp/sic-immutable-build.log + - name: Audit exact theorem axioms + run: | + cp FormalConjectures/OpenQuantumProblems/23.lean /tmp/SICImmutableAxioms.lean + cat >> /tmp/SICImmutableAxioms.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/SICImmutableAxioms.lean 2>&1 | tee /tmp/sic-immutable-axioms.log + ! grep -E 'sorryAx|Lean\.ofReduce|Lean\.ofReduceBool|Lean\.trustCompiler' /tmp/sic-immutable-axioms.log + - uses: actions/upload-artifact@v4 + if: always() + with: + name: sic-immutable-${{ github.run_id }} + path: | + /tmp/sic-immutable-build.log + /tmp/sic-immutable-axioms.log + if-no-files-found: warn From 10f15576a816d1282f00f6bba6f3a8320042cc7c Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:26:23 -0700 Subject: [PATCH 2/5] ci: build the registered immutable SIC module --- .github/workflows/openai-sic-immutable-audit.yml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/.github/workflows/openai-sic-immutable-audit.yml b/.github/workflows/openai-sic-immutable-audit.yml index 7b20e12307..ca56c05a8c 100644 --- a/.github/workflows/openai-sic-immutable-audit.yml +++ b/.github/workflows/openai-sic-immutable-audit.yml @@ -33,15 +33,14 @@ jobs: restore-keys: sic-immutable-${{ runner.os }}-${{ runner.arch }}- - name: Fetch compiled dependencies run: lake exe cache get - - name: Compile exact canonical source + - name: Compile exact registered canonical module run: | set -o pipefail - lake env lean FormalConjectures/OpenQuantumProblems/23.lean 2>&1 | tee /tmp/sic-immutable-build.log + lake build FormalConjectures.OpenQuantumProblems.«23» 2>&1 | tee /tmp/sic-immutable-build.log - name: Audit exact theorem axioms run: | - cp FormalConjectures/OpenQuantumProblems/23.lean /tmp/SICImmutableAxioms.lean - cat >> /tmp/SICImmutableAxioms.lean <<'EOF' - + cat > /tmp/SICImmutableAxioms.lean <<'EOF' + import FormalConjectures.OpenQuantumProblems.«23» #print axioms OpenQuantumProblem23.qubitSICFamily_pairwise #print axioms OpenQuantumProblem23.hasSICPOVM_two #print axioms OpenQuantumProblem23.hesseFamily_pairwise From 3437f7f0ceb0bbdecf61be52ce22a095201b3e96 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:49:42 -0700 Subject: [PATCH 3/5] ci: replay SIC with four exact phase-normalization repairs --- .../workflows/openai-sic-immutable-audit.yml | 67 ++++++++++++++++++- 1 file changed, 66 insertions(+), 1 deletion(-) diff --git a/.github/workflows/openai-sic-immutable-audit.yml b/.github/workflows/openai-sic-immutable-audit.yml index ca56c05a8c..1195cc3b4e 100644 --- a/.github/workflows/openai-sic-immutable-audit.yml +++ b/.github/workflows/openai-sic-immutable-audit.yml @@ -20,6 +20,70 @@ jobs: fetch-depth: 1 - name: Confirm immutable SIC proof commit run: test "$(git rev-parse HEAD)" = 7aeef3c2aca76d413f94d13ebf6044e9b6c1d712 + - name: Apply four deterministic phase-normalization repairs + run: | + python3 - <<'PY' + from pathlib import Path + import re + p = Path('FormalConjectures/OpenQuantumProblems/23.lean') + s = p.read_text() + + def replace_between(start_pat, end_pat, replacement): + global s + pattern = re.escape(start_pat) + r'.*?(?=' + re.escape(end_pat) + r')' + s2, n = re.subn(pattern, replacement.rstrip() + '\n\n', s, count=1, flags=re.S) + if n != 1: + raise SystemExit(f'failed replacement for {start_pat}: {n}') + s = s2 + + replace_between( + '@[simp] private lemma normSq_qubit_offdiag_star_omega_pow_two_audit', + '@[simp] private lemma overlap_three_two_star_pow_audit', + '''@[simp] private lemma normSq_qubit_offdiag_star_omega_pow_two_audit : + Complex.normSq ((1 / 3 : ℂ) + (2 / 3 : ℂ) * + ((starRingEnd ℂ) ω) ^ 2) = (1 / 3 : ℝ) := by + change Complex.normSq ((1 / 3 : ℂ) + (2 / 3 : ℂ) * + ((ω ^ 2) * (ω ^ 2))) = (1 / 3 : ℝ) + rw [omega_sq_mul_omega_sq_audit] + exact normSq_qubit_offdiag_omega_audit''') + + replace_between( + '@[simp] private lemma overlap_three_two_star_pow_audit', + '/-- The tetrahedral qubit SIC family has the correct constant pairwise overlap. -/', + '''@[simp] private lemma overlap_three_two_star_pow_audit : + Complex.normSq ((1 / 3 : ℂ) + (tetraB : ℂ) * + ((starRingEnd ℂ) ω) ^ 2 * ((tetraB : ℂ) * ω)) = (1 / 3 : ℝ) := by + change Complex.normSq ((1 / 3 : ℂ) + (tetraB : ℂ) * + ((ω ^ 2) * (ω ^ 2)) * ((tetraB : ℂ) * ω)) = (1 / 3 : ℝ) + rw [omega_sq_mul_omega_sq_audit] + exact overlap_three_two_simplified_audit''') + + replace_between( + '@[simp] private lemma q3_normSq_half_add_half_mul_star_omega_pow_two', + '@[simp] private lemma q3_normSq_half_add_hesseS_star_omega_pow_two_mul_hesseS_omega', + '''@[simp] private lemma q3_normSq_half_add_half_mul_star_omega_pow_two : + Complex.normSq ((1 / 2 : ℂ) + (1 / 2 : ℂ) * + ((starRingEnd ℂ) ω) ^ 2) = (1 / 4 : ℝ) := by + change Complex.normSq ((1 / 2 : ℂ) + (1 / 2 : ℂ) * + ((ω ^ 2) * (ω ^ 2))) = (1 / 4 : ℝ) + rw [q3_omega_sq_mul_omega_sq] + exact q3_normSq_half_add_half_mul_omega''') + + replace_between( + '@[simp] private lemma q3_normSq_half_add_hesseS_star_omega_pow_two_mul_hesseS_omega', + '@[simp] private lemma q3_normSq_half_mul_omega_sq_add_half', + '''@[simp] private lemma q3_normSq_half_add_hesseS_star_omega_pow_two_mul_hesseS_omega : + Complex.normSq ((1 / 2 : ℂ) + (hesseS : ℂ) * + ((starRingEnd ℂ) ω) ^ 2 * ((hesseS : ℂ) * ω)) = (1 / 4 : ℝ) := by + change Complex.normSq ((1 / 2 : ℂ) + (hesseS : ℂ) * + ((ω ^ 2) * (ω ^ 2)) * ((hesseS : ℂ) * ω)) = (1 / 4 : ℝ) + rw [q3_omega_sq_mul_omega_sq] + exact q3_normSq_half_add_hesseS_omega_mul_hesseS_omega''') + + p.write_text(s) + PY + git diff --check + git diff -- FormalConjectures/OpenQuantumProblems/23.lean > /tmp/sic-four-repairs.patch - name: Install pinned Lean toolchain run: | curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none @@ -33,7 +97,7 @@ jobs: restore-keys: sic-immutable-${{ runner.os }}-${{ runner.arch }}- - name: Fetch compiled dependencies run: lake exe cache get - - name: Compile exact registered canonical module + - name: Compile patched registered canonical module run: | set -o pipefail lake build FormalConjectures.OpenQuantumProblems.«23» 2>&1 | tee /tmp/sic-immutable-build.log @@ -53,6 +117,7 @@ jobs: with: name: sic-immutable-${{ github.run_id }} path: | + /tmp/sic-four-repairs.patch /tmp/sic-immutable-build.log /tmp/sic-immutable-axioms.log if-no-files-found: warn From 1c26569c0bf39c616752c77ff3fd4ed6879b3afc Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:59:01 -0700 Subject: [PATCH 4/5] ci: register a source-only SIC audit trigger --- .github/workflows/openai-sic-immutable-audit.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/openai-sic-immutable-audit.yml b/.github/workflows/openai-sic-immutable-audit.yml index 1195cc3b4e..bf07a0930d 100644 --- a/.github/workflows/openai-sic-immutable-audit.yml +++ b/.github/workflows/openai-sic-immutable-audit.yml @@ -5,6 +5,7 @@ on: branches: [main] paths: - '.github/workflows/openai-sic-immutable-audit.yml' + - '.github/sic-audit-trigger' permissions: contents: read @@ -117,6 +118,7 @@ jobs: with: name: sic-immutable-${{ github.run_id }} path: | + FormalConjectures/OpenQuantumProblems/23.lean /tmp/sic-four-repairs.patch /tmp/sic-immutable-build.log /tmp/sic-immutable-axioms.log From 7b069ab4d589098146dff42c1ada13c3f558a5c0 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:59:20 -0700 Subject: [PATCH 5/5] ci: trigger patched SIC source audit --- .github/sic-audit-trigger | 1 + 1 file changed, 1 insertion(+) create mode 100644 .github/sic-audit-trigger diff --git a/.github/sic-audit-trigger b/.github/sic-audit-trigger new file mode 100644 index 0000000000..1096183dcc --- /dev/null +++ b/.github/sic-audit-trigger @@ -0,0 +1 @@ +trigger patched SIC audit