diff --git a/README.adoc b/README.adoc
index 1747c84..486d585 100644
--- a/README.adoc
+++ b/README.adoc
@@ -190,7 +190,7 @@ interface is a breaking correction documented in link:docs/proof-transport.adoc[
 
 [NOTE]
 ====
-2026-10-12: Kripke semantics, the frame-condition correspondences, a non-factive model (`Warrant ≠ SoundWarrant` witnessed), the residual-evidence frame and the dependence test now live under `src/EpistemicTypes/Kripke/`; see link:docs/kripke-status-2026-10-12.adoc[]. Global warrant soundness for type-determined warrants is reported externally in choreographic-types but remains open pending an immutable external revision containing the theorem and its import and a successful type-check (E-6). Soundness for data-dependent warrants remains an assumption.
+2026-10-12: Kripke semantics, the frame-condition correspondences, a non-factive model (`Warrant ≠ SoundWarrant` witnessed), the residual-evidence frame and the dependence test now live under `src/EpistemicTypes/Kripke/`; see link:docs/kripke-status-2026-10-12.adoc[]. Global warrant soundness for type-determined warrants is proved externally in choreographic-types, at the recorded revision `d8536184366f4ac4567aa066c5dbcb9220e3607a` with a successful CI type-check, and is not re-checked here (E-6). Soundness for data-dependent warrants remains an assumption.
 ====
 
 [CAUTION]
diff --git a/docs/kripke-status-2026-10-12.adoc b/docs/kripke-status-2026-10-12.adoc
index 56612fb..5fd088d 100644
--- a/docs/kripke-status-2026-10-12.adoc
+++ b/docs/kripke-status-2026-10-12.adoc
@@ -3,7 +3,7 @@
 
 The modules under `src/EpistemicTypes/Kripke/` formalise Kripke semantics
 and the results below. Complete epistemic logic and soundness for
-data-dependent warrants remain outstanding; E-6 records the open external
+data-dependent warrants remain outstanding; E-6 records the external
 verification for type-determined warrants.
 
 [cols="1,3,1",options="header"]
@@ -14,7 +14,7 @@ verification for type-determined warrants.
 | E-3 | Correspondences, constructively: reflexive ⇔ factive (T, both directions); transitive ⇔ positively introspective (4, both directions); Euclidean ⇒ 5; serial ⇒ D. The converses of 5 and D need classical reasoning and are not claimed | PROVEN / OPEN as stated
 | E-4 | A reflexive frame yields an `IndexedFactive` (`factive`) | PROVEN
 | E-5 | *The non-factive model*: two worlds, access only w₀ → w₁; at w₀ there is a `Warrant` (evidence: a `Box` proof) for a false proposition, and no `sound` field can exist for it. `Warrant ≠ SoundWarrant`, witnessed | PROVEN (`Kripke/Belief.agda`: `believed`, `false-at-w₀`, `no-sound-warrant`); TESTED (`tests/reject/BeliefIsKnowledge`: factivity refused on this frame)
-| E-6 | Global soundness of warrants in a reflexive frame — every type-determined warrant sound — is reported externally in choreographic-types (`Choreographic.Kripke`, citing this repo's `Warrant` at `495db9c`) | OPEN (an immutable external revision containing the theorem and its import, and a successful type-check, are not recorded here)
+| E-6 | Global soundness of warrants in a reflexive frame — every type-determined warrant sound — is proved externally in choreographic-types (`Choreographic.Kripke`, `Frame.sound-warrant`), which imports this repo's `EpistemicTypes.Warrant` at `495db9cca003e12066a3cb9c9f2d7afa1a953aec` (`Warrant.agda`, `Base.agda` and `Access.agda` are unchanged between that commit and this one). Recorded external revision: choreographic-types `d8536184366f4ac4567aa066c5dbcb9220e3607a`. Type-check: its `Agda proofs` workflow, run 39288705455 on that commit, succeeded under Agda 2.6.4.3 with `--safe --without-K --no-libraries --ignore-interfaces --double-check` (the import is pinned by `scripts/fetch-siblings.sh` there) | RECORDED externally on 2026-10-19 (revision and CI run above; the rest of this table is the 2026-10-12 snapshot); not re-checked in this repository
 |===
 
 Separation (family bar, criterion 2): the belief model is a modality with