Proof reachability: preserve the 62-row historical cut and add post-C126 proof routes

.github/workflows/proof-reachability.yml

@@ -0,0 +1,36 @@
+name: Proof reachability table
+
+'on':
+  pull_request:
+    paths:
+      - 'docs/integration/2026-10-02-proof-reachability.md'
+      - 'tools/check_proof_reachability.py'
+      - 'tests/test_proof_reachability.py'
+      - '.github/workflows/proof-reachability.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  reachability:
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+        with:
+          persist-credentials: false
+          fetch-depth: 0
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065
+        with:
+          python-version: '3.11.16'
+      - name: Re-derive every row from git at the pinned cut, in both interpreter modes
+        env:
+          PYTHONDONTWRITEBYTECODE: '1'
+        run: |
+          set -euo pipefail
+          python -B -S tools/check_proof_reachability.py
+          python -B -O -S tools/check_proof_reachability.py
+          python -B -S -m unittest -v tests.test_proof_reachability
+          python -B -O -S -m unittest -v tests.test_proof_reachability
+          git diff --exit-code

PROOF_INDEX.md

@@ -153,3 +153,7 @@ The packets below landed on `main` after this index was last checked (2026-09-26
 ## Repository rule
 
 A reviewed/closed theorem or lemma must have its full proof or immutable byte-bound mirror in this repository plus the exact review/certificate. An open theorem with a complete candidate proof must link it here. An open item without a complete proof must link the strongest partial derivation and state the missing proof explicitly. Superseded/refuted work stays available. Tests and hashes are evidence, not substitutes for analytic proof. A navigation refresh records source availability and existing review scope; any change to [claims/LANDING_CLAIMS.json](claims/LANDING_CLAIMS.json) or the D0-D7 graph requires its own source-bound reconciliation through the existing validators.
+
+## Later frontier proof paths
+
+[Frontier proof reachability and the post-C126 supplement](docs/integration/2026-10-02-proof-reachability.md) retain the original 2 October inventory and add a separately pinned 3 October cut, including routes to the nested soft-layer and A4 records. These are dated availability inventories, not new verdicts or a count of distinct theorems.