hyperpolymath · Oct 19, 2026 · Oct 19, 2026 · Oct 19, 2026 · Oct 19, 2026
diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
@@ -20,7 +20,7 @@ workflows:
     '.github/workflows/label-triage.yml': []
     '.github/workflows/labels.yml': []
     '.github/workflows/main-estate-audit.yml':
-        - 'hyperpolymath/cicd-suite@376898bbe872226866ccbc7648d43123b8bb21b9'
+        - 'hyperpolymath/cicd-suite@b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a'
     '.github/workflows/proofs.yml':
         - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
     '.github/workflows/push-email-notify.yml':
@@ -45,9 +45,9 @@ dependencies:
         commit: 'sha1-b96794f015dfd88f77b49b1c93e0fa7110f94c63'
         owner_id: 9919
         repo_id: 259445878
-    'hyperpolymath/cicd-suite@376898bbe872226866ccbc7648d43123b8bb21b9':
-        ref: '376898bbe872226866ccbc7648d43123b8bb21b9'
-        commit: 'sha1-376898bbe872226866ccbc7648d43123b8bb21b9'
+    'hyperpolymath/cicd-suite@b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a':
+        ref: 'b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a'
+        commit: 'sha1-b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a'
         owner_id: 6759885
         repo_id: 1326697643
     'hyperpolymath/smtp-notify-action@v0.2.0':

diff --git a/.github/workflows/main-estate-audit.yml b/.github/workflows/main-estate-audit.yml
@@ -11,10 +11,9 @@ name: Central Estate CI/CD Audit
 # is the check. cicd-suite's templates/track-estate-audit.yml can open those
 # PRs weekly; it needs an AUTOMATION_TOKEN secret.
 #
-# actions.lock lists this file as [], like secret-scanner.yml. A
-# cross-repository reusable-workflow call recorded in the lock startup-fails
-# with zero jobs under sha_pinning_required (see the header of cicd-suite's
-# main-estate-audit.yml).
+# actions.lock records this call at the pinned SHA. An untagged pin keeps the
+# SHA as `ref`, which job setup accepts; move the lock record together with
+# the pin, or the edge dangles and the run startup-fails with zero jobs.
 
 on:
   push:
@@ -27,4 +26,4 @@ permissions:
 
 jobs:
   estate:
-    uses: hyperpolymath/cicd-suite/.github/workflows/main-estate-audit.yml@376898bbe872226866ccbc7648d43123b8bb21b9 # cicd-suite main, #50
+    uses: hyperpolymath/cicd-suite/.github/workflows/main-estate-audit.yml@b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a # cicd-suite main, #55
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
@@ -72,7 +72,7 @@ epistemic-types' `Warrant.agda` is imported (same kernel, pinned commit
 | T-3 | p-accessibility is exactly sameness of p's projected cut (both directions) | PROVEN (`knows-local-cut`, `local-cut-determines`)
 | T-4 | Party access `p ⊑ q` ("q sees at least what p sees") is a preorder — epistemic-types' `Preorder` record, instantiated — and knowledge is monotone along it | PROVEN (`party-access`, `knows-mono`)
 | T-5 | A silent party is below every party; knowledge flows up the preorder only — `1 ⊑ 2` for the witness protocol is refused | PROVEN (`silent-⊑`, `inherited`); TESTED (`tests/reject/AccessWrongWay`)
-| T-6 | epistemic-types' `AccessibleModality` cannot be instantiated as stated: its `E : K → Set → Set` has no world index, and world-free knowledge collapses to the proposition itself (reflexivity). With `E : K → (World → Set) → (World → Set)` — field for field otherwise identical (`IndexedAccessible`) — the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); the mismatch is a finding for epistemic-types
+| T-6 | epistemic-types' `AccessibleModality` cannot be instantiated as stated: its `E : K → Set → Set` has no world index, and world-free knowledge collapses to the proposition itself (reflexivity). With `E : K → (World → Set) → (World → Set)` — field for field otherwise identical (`IndexedAccessible`) — the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); epistemic-types has since added the same world-indexed records (its Kripke/Indexed module), so the mismatch is resolved upstream; this repository still carries its own copy of the indexed record rather than importing theirs
 |===
 
 == Asynchrony (Async.agda, AsyncKnowledge.agda, AsyncBound.agda)

diff --git a/docs/LANDING.adoc b/docs/LANDING.adoc
@@ -19,7 +19,8 @@ Order matters: nothing below is citable until step 6 is green.
   applications file; `CHANGELOG-entry.adoc` into CHANGELOG.
 . Cross-repo: nextgen-typing decision record and TYPE-CONNECTIONS rows;
   absolute-zero T1 exception record (and a ruling on T7); the
-  epistemic-types issue (`cross-repo/`). occupancy-types: an issue linking
+  epistemic-types issue (`cross-repo/`, superseded: upstream did the indexed
+  records itself and its external-verification row is recorded in hyperpolymath/epistemic-types#41). occupancy-types: an issue linking
   H-2 (its R2–R3 algebra will supersede `Instances/HWM.agda`) and A-3.
 . CI: both `proofs.yml` files are DESIGNED until their first green run on
   the Debian `agda-bin=2.6.4.3-1+b2` pin. If the pin fails to install, that

diff --git a/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc b/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc
@@ -1,4 +1,13 @@
 // Issue text for hyperpolymath/epistemic-types.
+// SUPERSEDED 2026-10-19. This text was never filed. epistemic-types'
+// own 2026-10-12 Kripke work (kripke-2026-10-12, #40) already did asks 2
+// and 3: `Kripke/Indexed.agda` has IndexedModality / IndexedFactive /
+// IndexedAccessible, and Warrant, Base and Access are builtins-only. Ask 1
+// (record choreographic-types as an external model in the README) is covered
+// by the README note there; its verification record is the external-verification
+// row of their docs/kripke-status-2026-10-12.adoc, which
+// hyperpolymath/epistemic-types#41 completes with the external revision and CI
+// run it was waiting for. Kept as the record of what was found.
 = An external model discharges "global soundness of warrants" for type-determined warrants
 
 README lists *global soundness of warrants* and *Kripke semantics* as