WIP: finish mathematical implementation and verification infrastructure (certify in successor PR)

.github/workflows/application.yml

@@ -6,6 +6,10 @@ on:
   pull_request:
     branches: [main]
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
 

.github/workflows/e1-approx-quotient-smoke.yml

@@ -16,6 +16,10 @@ on:
       - '.github/workflows/e1-approx-quotient-smoke.yml'
   workflow_dispatch:
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
 

.github/workflows/f1-multiagent-protocols-smoke.yml

@@ -16,6 +16,10 @@ on:
       - '.github/workflows/f1-multiagent-protocols-smoke.yml'
   workflow_dispatch:
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
 

.github/workflows/lean.yml

@@ -6,6 +6,10 @@ on:
   pull_request:
     branches: [main]
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
 

.github/workflows/pr113-all-case-compiler.yml

@@ -0,0 +1,113 @@
+name: PR113 All-Case Compiler Candidate
+
+on:
+  push:
+    branches: [research/final-mathematical-closure]
+    paths:
+      - '.github/workflows/pr113-all-case-compiler.yml'
+      - 'PermanssonResearch/**'
+      - 'PermanssonResearch.lean'
+      - 'verification/research/final_closure_complete_lean_evidence.py'
+      - 'verification/research/closure_elaborated_type.py'
+      - 'verification/research/final_closure_merge_compiler_shards.py'
+      - 'research/paper_closures/post_merge_112/acceptance_case_source_map.json'
+      - 'research/paper_closures/post_merge_112/claim_declaration_map.json'
+  workflow_dispatch:
+
+concurrency:
+  group: pr113-all-case-compiler-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  inventory-preflight:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065
+        with:
+          python-version: '3.13'
+      - name: Bind genuine branch checkout and resolve ALL historical theorem names
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git rev-parse HEAD)" = "$GITHUB_SHA"
+          test "$GITHUB_REPOSITORY" = "HMarcusWH/PermanssonLean"
+          mkdir -p "$RUNNER_TEMP/all-case-inventory"
+          python3 verification/research/final_closure_complete_lean_evidence.py \
+            --head "$GITHUB_SHA" \
+            --output "$RUNNER_TEMP/not-written" \
+            --inventory-only \
+            > "$RUNNER_TEMP/all-case-inventory/inventory.json"
+          python3 - <<'PY'
+          import json, os
+          from pathlib import Path
+          inv = json.loads((Path(os.environ["RUNNER_TEMP"]) /
+              "all-case-inventory/inventory.json").read_text())
+          assert inv["cases"] == 45 and inv["claims"] == 11
+          assert inv["proof_targets"] > 11
+          assert len(inv["declarations"]) == inv["proof_targets"]
+          assert inv["status"] == "SOURCE_CANDIDATE_UNREVIEWED"
+          print("All-case compile candidates:", inv["proof_targets"])
+          PY
+      - name: Preserve source inventory candidate
+        if: ${{ always() }}
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: pr113-all-case-owner-inventory
+          path: ${{ runner.temp }}/all-case-inventory/
+          retention-days: 30
+          if-no-files-found: warn
+
+  compiler-shard:
+    needs: inventory-preflight
+    runs-on: ubuntu-latest
+    timeout-minutes: 110
+    strategy:
+      fail-fast: false
+      max-parallel: 2
+      matrix:
+        shard: [0, 1, 2, 3]
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065
+        with:
+          python-version: '3.13'
+      - name: Build pinned research library before theorem probes
+        uses: leanprover/lean-action@24581d74d674803a25a81b10b059c5c0cdd344c6
+        with:
+          auto-config: false
+          build: true
+          build-args: PermanssonResearch
+          test: false
+          lint: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          axiom-audit: true
+          axiom-audit-root: PermanssonResearch
+      - name: Execute original 45-case and 11-claim assigned compiler shard
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git rev-parse HEAD)" = "$GITHUB_SHA"
+          python3 verification/research/final_closure_complete_lean_evidence.py \
+            --head "$GITHUB_SHA" \
+            --output "$RUNNER_TEMP/complete-shard" \
+            --shard-index "${{ matrix.shard }}" --shard-count 4
+      - name: Preserve unreviewed theorem type and axiom logs
+        if: ${{ always() }}
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: pr113-compiler-shard-${{ matrix.shard }}
+          path: ${{ runner.temp }}/complete-shard/
+          retention-days: 30
+          if-no-files-found: warn

.github/workflows/pr113-all-original-semantic-candidates.yml

@@ -0,0 +1,76 @@
+name: PR113 All Original Semantic Candidate Evidence
+
+on:
+  push:
+    branches:
+      - research/final-mathematical-closure
+    paths:
+      - '.github/workflows/pr113-all-original-semantic-candidates.yml'
+      - 'PermanssonResearch/**'
+      - 'PermanssonResearch.lean'
+      - 'verification/research/final_closure_*'
+      - 'verification/research/test_pr113_semantic_*.py'
+      - 'verification/research/test_final_closure_all_original_semantics.py'
+      - 'research/paper_closures/post_merge_112/acceptance_case_source_map.json'
+  workflow_dispatch:
+
+concurrency:
+  group: pr113-original-semantic-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  semantic-candidate-shard:
+    runs-on: ubuntu-latest
+    timeout-minutes: 110
+    strategy:
+      fail-fast: false
+      max-parallel: 3
+      matrix:
+        shard: [0, 1, 2, 3, 4, 5, 6, 7, 8]
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065
+        with:
+          python-version: '3.13'
+      - name: Check exact Git checkout before mathematical work
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git rev-parse HEAD)" = "$GITHUB_SHA"
+          test "$GITHUB_REPOSITORY" = "HMarcusWH/PermanssonLean"
+          test -z "$(git status --porcelain=v1 --untracked-files=all -- PermanssonResearch PermanssonLean verification/research)"
+      - name: Build pinned Lean research tree and audit axioms
+        uses: leanprover/lean-action@24581d74d674803a25a81b10b059c5c0cdd344c6
+        with:
+          auto-config: false
+          build: true
+          build-args: PermanssonResearch
+          test: false
+          lint: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          axiom-audit: true
+          axiom-audit-root: PermanssonResearch
+      - name: Run exact source/mutant candidates (not approval)
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git rev-parse HEAD)" = "$GITHUB_SHA"
+          python3 verification/research/final_closure_all_original_semantics.py \
+            --head "$GITHUB_SHA" \
+            --shard-index "${{ matrix.shard }}" --shard-count 9 \
+            --out "$RUNNER_TEMP/pr113-semantic-source-${{ matrix.shard }}"
+      - name: Preserve unreviewed source/mutant compiler evidence
+        if: ${{ always() }}
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: pr113-all-original-semantic-candidates-${{ matrix.shard }}
+          path: ${{ runner.temp }}/pr113-semantic-source-${{ matrix.shard }}/
+          retention-days: 30
+          if-no-files-found: error

.github/workflows/pr113-clean-paper-rebuild.yml

@@ -0,0 +1,79 @@
+name: PR113 Clean Paper Rebuild Candidate
+
+on:
+  push:
+    branches:
+      - research/final-mathematical-closure
+    paths:
+      - 'release/mathematical-closure-1/**'
+      - 'research_papers/mathematical_closure/**'
+      - '.github/workflows/pr113-clean-paper-rebuild.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  clean-paper-rebuild:
+    runs-on: ubuntu-latest
+    timeout-minutes: 100
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065
+        with:
+          python-version: '3.13'
+      - name: Install independent TeX/PDF render dependencies
+        run: |
+          sudo apt-get update -qq
+          sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -qq \
+            texlive-latex-base texlive-latex-recommended \
+            texlive-latex-extra texlive-pictures \
+            texlive-fonts-recommended poppler-utils
+      - name: Rebuild exact H from two separate no-hardlink source clones
+        shell: bash
+        run: |
+          set -euo pipefail
+          python3 release/mathematical-closure-1/reproduce_clean_sources.py \
+            --source-head "$GITHUB_SHA" \
+            --out "$RUNNER_TEMP/perm-clean-rebuild"
+      - name: Attach honest execution identity, NOT approval
+        shell: bash
+        run: |
+          set -euo pipefail
+          python3 - <<'PY'
+          import json, os
+          from pathlib import Path
+          out = Path(os.environ["RUNNER_TEMP"]) / "perm-clean-rebuild"
+          report = json.loads((out/"reproduction_receipt.json").read_text())
+          assert report["status"] == "REPRODUCIBLE_DRAFT_ONLY"
+          assert report["source_commit_sha"] == os.environ["GITHUB_SHA"]
+          assert report["independent_source_roots"] == 2
+          identity = {
+              "format": "Permansson.CICleanRebuildCandidate.v1",
+              "status": "EXECUTED_DRAFT_ONLY_NO_SCHOLARLY_REVIEW",
+              "source_head": os.environ["GITHUB_SHA"],
+              "github_repository": os.environ["GITHUB_REPOSITORY"],
+              "github_workflow": os.environ["GITHUB_WORKFLOW"],
+              "github_run_id": int(os.environ["GITHUB_RUN_ID"]),
+              "github_run_attempt": int(os.environ["GITHUB_RUN_ATTEMPT"]),
+              "github_job": os.environ["GITHUB_JOB"],
+              "pdf_sha256": report["pdf_sha256"],
+              "archive_sha256": report["archive_sha256"],
+              "authenticated_ci_artifact": False,
+              "scientific_release_approved": False,
+          }
+          assert identity["github_repository"] == "HMarcusWH/PermanssonLean"
+          assert identity["github_job"] == "clean-paper-rebuild"
+          (out/"ci_execution_identity.json").write_text(
+              json.dumps(identity, sort_keys=True, indent=2)+"\n")
+          PY
+      - name: Retain both genuine draft source-root outputs for independent verification
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: pr113-clean-paper-rebuild-draft
+          path: ${{ runner.temp }}/perm-clean-rebuild/
+          retention-days: 30
+          if-no-files-found: error