diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 6732615..a16a168 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -51,8 +51,8 @@ is a layer over the same fragment (section "Asynchrony" below).
 
 == K-CUT-WARRANT, bound form (Kripke.agda, Bound.agda)
 
-epistemic-types' `Warrant.agda` is imported (same kernel, pinned commit
-495db9c), not re-declared, so "SoundWarrant" below is their record.
+epistemic-types' `Warrant.agda` is imported (same kernel; pinned commit
+`6ce8c74` since #40, 2026-11-07, previously `495db9c`), not re-declared, so "SoundWarrant" below is their record.
 
 [cols="1,3,1",options="header"]
 |===
@@ -76,15 +76,20 @@ 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' unindexed `AccessibleModality` cannot express this frame directly: 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)` in the local `IndexedAccessible` record, the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); the current sibling pin lacks the upstream Kripke/Indexed module. The newer upstream interface exists, but updating the pin and adapting this local instance remain pending
+| T-6 | epistemic-types' unindexed `AccessibleModality` cannot express this frame directly: 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)` in the local `IndexedAccessible` record, the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); the sibling pin 6ce8c74 contains the upstream Kripke/Indexed module, but this repository still uses the local record. Only local integration (importing the upstream record and adapting `knowledge`) remains pending
 |===
 
-The upstream indexed interface is available at epistemic-types commit
-`5422cd5bf1418c44321bf0f77e894737a451d8f5`; the gate still pins
-`495db9cca003e12066a3cb9c9f2d7afa1a953aec`. Upstream packages `E` and
-`map` in an `IndexedModality` field, so integration requires adapting
-`knowledge` as well as replacing the local record. See
-link:docs/toolchain-and-prompts-2026-11-01.md[the pending integration plan].
+The upstream indexed interface was first verified at epistemic-types commit
+`5422cd5bf1418c44321bf0f77e894737a451d8f5`. The pin update is complete: the
+gate pins `6ce8c74e8a91e5021cb0c1fb4fc805bdff837178` (since #40), which contains
+`EpistemicTypes.Kripke.Indexed`, but no module here imports it yet. Upstream
+packages `E` and `map` in an `IndexedModality` field, so integration requires
+adapting `knowledge` as well as replacing the local record. The historical
+link:docs/toolchain-and-prompts-2026-11-01.md[integration plan] predates the
+pin update and suggests pinning `5422cd5`; do not follow that step. `5422cd5`
+lacks `EpistemicTypes.PartialRecovery`, which `Choreographic.PartialRecovery`
+imports, so keep the pin at `6ce8c74`. Only steps 2 to 4 of that plan (the
+local integration) remain.
 
 == Asynchrony (Async.agda, AsyncKnowledge.agda, AsyncBound.agda)
 
@@ -222,7 +227,7 @@ warrants is documented precisely: the type provides the warrant
 structure and type-determined evidence (Kripke knowledge) but not
 data-dependent evidence or soundness.
 
-epistemic-types' `SoundWarrant` (pinned commit `495db9cc`) is imported,
+epistemic-types' `SoundWarrant` (pinned commit `6ce8c74`, previously `495db9cc`) is imported,
 not re-declared: `Warrant` carries an `Evidence` type; `SoundWarrant`
 adds `sound : Evidence → A`. A sound warrant alone can have an empty
 evidence type. The receiver-local side condition therefore also requires
diff --git a/docs/LANDING.adoc b/docs/LANDING.adoc
index 9660e44..9d2be24 100644
--- a/docs/LANDING.adoc
+++ b/docs/LANDING.adoc
@@ -13,7 +13,8 @@ Order matters: nothing below is citable until step 6 is green.
   sibling — the clone's HEAD on 2026-10-12). Open a PR; CodeRabbit and the
   estate workflows run; address every finding before merge (standing rule).
 . Fill `RESOURCE_ALGEBRA_COMMIT` in `scripts/fetch-siblings.sh` with the SHA
-  from step 1; the epistemic-types pin `495db9c` is already set.
+  from step 1; the epistemic-types pin is already set (`6ce8c74` since #40;
+  `495db9c` when this guide was written).
 . Splice `docs/README-keystone-section.adoc` into README (replacing the OPEN
   keystone section) and `docs/applications-header-patch.adoc` into the
   applications file; `CHANGELOG-entry.adoc` into CHANGELOG.