Audit the full Erdős 625 proof stack and isolate reusable results

.github/workflows/erdos625-full-proof-audit.yml

@@ -0,0 +1,111 @@
+name: Erdős 625 full proof audit
+
+on:
+  pull_request:
+    paths:
+      - "625/audits/FULL_THEOREM_LEMMA_AUDIT_2026-07-25.md"
+      - "625/audits/POST_INTEGRATION_STATUS_2026-07-25.md"
+      - "625/proofs/SECTION8_GLOBAL_DECORATION_BRIDGE.md"
+      - "625/proofs/TRANSFERABLE_RESULTS_AND_COROLLARIES_2026-07-25.md"
+      - "625/experiments/full_proof_audit_regression.py"
+      - "625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean"
+      - "625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean"
+      - "625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean"
+      - ".github/workflows/erdos625-full-proof-audit.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-full-audit-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  audit-regression:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Compile audit checker
+        run: python -m py_compile 625/experiments/full_proof_audit_regression.py
+      - name: Run exact audit checks
+        run: python 625/experiments/full_proof_audit_regression.py
+      - name: Run audit checks with optimization enabled
+        run: python -O 625/experiments/full_proof_audit_regression.py
+
+  focused-section8-repair:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in repaired modules
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean \
+            625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean; then
+              exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build the Section 8 simplification dependency closure warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section8SimplificationCore --wfail \
+            > /tmp/erdos625-full-audit-section8.log 2>&1
+          status=$?
+          tail -n 500 /tmp/erdos625-full-audit-section8.log
+          exit $status
+      - name: Upload focused Section 8 compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-full-audit-section8-log
+          path: /tmp/erdos625-full-audit-section8.log
+          if-no-files-found: ignore
+
+  focused-section9-frontier:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in the frontier module
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean; then
+              exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build the exact q-only second-moment frontier warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section9QOnlySecondMomentFrontier --wfail \
+            > /tmp/erdos625-full-audit-section9.log 2>&1
+          status=$?
+          tail -n 500 /tmp/erdos625-full-audit-section9.log
+          exit $status
+      - name: Upload focused Section 9 compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-full-audit-section9-log
+          path: /tmp/erdos625-full-audit-section9.log
+          if-no-files-found: ignore

.github/workflows/erdos625-matching-restriction-envelope.yml

@@ -0,0 +1,59 @@
+name: Erdős 625 matching-restriction envelope
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean"
+      - "625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md"
+      - ".github/workflows/erdos625-matching-restriction-envelope.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  focused-lean-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in the new modules
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean; then
+            exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build the log-square endpoint and dependency closure warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section9ProfileAttachmentMatchingLogScale --wfail \
+            > /tmp/section9-envelope-lean.log 2>&1
+          status=$?
+          tail -n 300 /tmp/section9-envelope-lean.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: section9-matching-envelope-lean-log
+          path: /tmp/section9-envelope-lean.log
+          if-no-files-found: ignore

.github/workflows/erdos625-matching-restriction-product.yml

@@ -0,0 +1,57 @@
+name: Erdős 625 matching-restriction product
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/FiniteRestrictionProduct.lean"
+      - "625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean"
+      - "625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md"
+      - ".github/workflows/erdos625-matching-restriction-product.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-matching-restriction-product-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  focused-lean-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in the finite modules
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/FiniteRestrictionProduct.lean \
+            625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean; then
+              exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build the matching-restriction product warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section9MatchingRestrictionProduct --wfail \
+            > /tmp/section9-matching-restriction-product.log 2>&1
+          status=$?
+          tail -n 500 /tmp/section9-matching-restriction-product.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-matching-restriction-product-log
+          path: /tmp/section9-matching-restriction-product.log
+          if-no-files-found: ignore

.github/workflows/erdos625-q-only-attachment-envelope.yml

@@ -0,0 +1,61 @@
+name: Erdős 625 q-only attachment envelope
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean"
+      - "625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean"
+      - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md"
+      - ".github/workflows/erdos625-q-only-attachment-envelope.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-q-only-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  focused-lean-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean \
+            625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean; then
+            exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build q-only two-regime assembly warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section9QOnlyTwoRegimeAssembly --wfail \
+            > /tmp/q-only-envelope-lean.log 2>&1
+          status=$?
+          tail -n 380 /tmp/q-only-envelope-lean.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: section9-q-only-envelope-lean-log
+          path: /tmp/q-only-envelope-lean.log
+          if-no-files-found: ignore