hyperpolymath · Oct 5, 2026 · Oct 5, 2026 · Oct 5, 2026
diff --git a/.machine_readable/descriptiles/META.a2ml b/.machine_readable/descriptiles/META.a2ml
@@ -73,8 +73,8 @@ consequence = "No-smuggling holds structurally rather than by side-condition. Th
 title = "Secret types and information-flow control are specified outside this repository"
 status = "accepted"
 context = "Issue #29 preserved a secret-types research note here; issue #32 then proposed an in-repository security model. On 2026-10-04 the owner ruled that hyperpolymath/secret-types is the standalone home, with D153 (a secret type is a value whose flow is constrained by a confidentiality label with explicit declassification, registered in the type-family map on that boundary) and D154 (reuse an existing lattice, two-point first then general; prove noninterference; declassify only at explicit audited points)."
-decision = "This repository adds no Secret API and no information-flow implementation. docs/secret-types.adoc is retained as the boundary/history note; the specification itself, lattice reuse, the noninterference theorem, and audited declassification belong to hyperpolymath/secret-types."
-consequence = "The epistemic core keeps its scope: no confidentiality claim attaches to BeliefModality, Echo grades, or Access. epistemic-types#29 stays closed; the move of issue #32 must not be duplicated."
+decision = "This repository adds no Secret API and no information-flow implementation. docs/secret-types.adoc is retained as the boundary/history note; the specification itself (canonical text in hyperpolymath/secret-types docs/secret-types.adoc; placement in docs/decisions/0004-standalone-repo-and-scope.adoc, PR #4 d1122d8), lattice reuse, the noninterference theorem, and audited declassification belong to hyperpolymath/secret-types."
+consequence = "The epistemic core keeps its scope: no confidentiality claim attaches to BeliefModality, Echo grades, or Access. epistemic-types#29 stays closed. Issue #32 stays in this repository and stays open as the origin/decision record - no transfer and no duplicate - until the standalone specification's review checklist is completed item by item (docs/secret-types.adoc, docs/secret-types-transition-review-2026-10-05.adoc)."
 
 [development-practices]
 build-tool = "just"

diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml
@@ -1,7 +1,7 @@
 [metadata]
 project = "epistemic-types"
 version = "0.1.0"
-last-updated = "2026-10-04"
+last-updated = "2026-10-05"
 status = "prototype"  # prototype | active | paused | archived
 
 [project-context]
@@ -20,7 +20,7 @@ discipline = "Constructive. Compiles under {-# OPTIONS --safe --without-K #-}. N
 honesty-rule = "Laws appear as explicit fields when not derivable; lawful instances are added only after proving or explicitly assuming the laws. No smuggling."
 
 [boundaries]
-secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153: label-constrained flow with explicit declassification and type-family-map registration; D154: reuse an existing lattice two-point-first, prove noninterference, declassify only at explicit audited points). This repository adds no Secret API and no information-flow implementation; docs/secret-types.adoc is retained as the boundary/history note. epistemic-types#29 is resolved and stays closed; the transfer of epistemic-types#32 to secret-types is pending GitHub issue-write access and must not be duplicated."
+secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153: label-constrained flow with explicit declassification and type-family-map registration; D154: reuse an existing lattice two-point-first, prove noninterference, declassify only at explicit audited points). This repository adds no Secret API and no information-flow implementation; docs/secret-types.adoc is retained as the boundary/history note. epistemic-types#29 is resolved and stays closed; epistemic-types#32 stays in this repository and stays open as the origin/decision record (no transfer) and must not be duplicated. It closes only after the standalone specification's review checklist is completed item by item; see docs/secret-types.adoc and docs/secret-types-transition-review-2026-10-05.adoc."
 
 [build]
 checker = "Agda 2.6.4.3 (CI-matched)"

diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
@@ -41,7 +41,7 @@ agda-options = "{-# OPTIONS --safe --without-K #-} ; no postulates; no Agda stan
 agda-version = "2.6.4.3"
 echo-distinction = "Do not collapse Echo C y and E κ A. Echo retains certified residues; epistemic types are standpoint/warrant/access modalities. Their composition is meaningful; they are not the same modality."
 ci = "Proof and security workflows configured; required merge checks are described in docs/ci-safety.adoc"
-secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153/D154). Do not add a Secret API or information-flow implementation here; docs/secret-types.adoc is the boundary/history note. epistemic-types#29 stays closed."
+secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153/D154). Do not add a Secret API or information-flow implementation here; docs/secret-types.adoc is the boundary/history note. epistemic-types#29 stays closed; issue #32 stays open here as the origin/decision record (no transfer) until the standalone specification's review checklist completes."
 
 [first-run]
 dev-container = ".devcontainer/ — Debian 13 pinned to the same base image digest as CI, agda-bin=2.6.4.3-1+b2; postCreateCommand runs 'just check'."
@@ -107,7 +107,7 @@ rules = [
   "Keep a2ml / Nickel / k9 files under .machine_readable/ only.",
   "License and SPDX changes are owner-manual; do not add LICENSE files or SPDX headers.",
   "Maintain owner-authorized proof and security CI; do not bypass failing checks.",
-  "Secret types and information-flow control stay outside this repository (D153/D154, docs/secret-types.adoc); do not duplicate the move of issue #32.",
+  "Secret types and information-flow control stay outside this repository (D153/D154; canonical specification in hyperpolymath/secret-types). Issue #32 stays in this repository, open, as the origin/decision record: do not transfer it, close it, or duplicate it, and treat closure as pending the standalone specification's review checklist (docs/secret-types.adoc, docs/secret-types-transition-review-2026-10-05.adoc).",
 ]
 
 [ecosystem]

diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
@@ -12,6 +12,22 @@ the changelog records what is actually proved, not what is aspired to.
 
 === https://github.com/hyperpolymath/epistemic-types/compare/v0.1.0...HEAD[Unreleased]
 
+[[changed--2026-10-05]]
+==== Changed — 2026-10-05
+
+* Cross-reference review of the Secret Types transition. `docs/secret-types.adoc`
+  now records that issue #32 **stays in this repository, open**, as the
+  origin/decision record: the specification moved to
+  `hyperpolymath/secret-types` (canonical spec and ADR 0004, PR #4 `d1122d8`,
+  2026-10-04), but no issue transfer occurs, and closure waits on the standalone
+  specification's own review checklist. The provenance blob (`583017cfd5fa…`,
+  the PR #33 revision) was verified, the stale downstream cross-references were
+  recorded, and the exact proposed issue update (prepared, not posted) is in
+  `docs/secret-types-transition-review-2026-10-05.adoc`. `README`, the
+  documentation index, `STATE.a2ml`, `META.a2ml` (ADR-007) and
+  `0-AI-MANIFEST.a2ml` were corrected where they described a pending transfer of
+  issue #32. No Agda source changed.
+
 [[changed--2026-10-04]]
 ==== Changed — 2026-10-04
 

diff --git a/README.adoc b/README.adoc
@@ -206,7 +206,10 @@ This is a prototype, not a complete epistemic logic. The following are **intenti
   out of scope for this repository. The standalone home is
   link:https://github.com/hyperpolymath/secret-types[`hyperpolymath/secret-types`]
   (D153/D154); link:docs/secret-types.adoc[the boundary/history note] records
-  the decision and the pointer. No `Secret` API exists here.
+  the decision and the pointer. No `Secret` API exists here. Issue #32 stays
+  open in this repository as the origin/decision record (no transfer);
+  link:docs/secret-types-transition-review-2026-10-05.adoc[the transition
+  review] records the cross-references.
 
 == Build
 

diff --git a/docs/README.adoc b/docs/README.adoc
@@ -40,7 +40,14 @@ authority.
   `hyperpolymath/secret-types` is the standalone home (D153/D154), the retained
   two-level information-flow proposal (label order, attacker and observation
   boundary, noninterference target), and the reason no `Secret` API or security
-  theorem exists in this repository.
+  theorem exists in this repository. Issue #32 stays open here as the
+  origin/decision record (no transfer).
+
+| `docs/secret-types-transition-review-2026-10-05.adoc`
+| Cross-reference review of the Secret Types transition: the evidence and
+  verified provenance of `secret-types` PR #4, the ownership split (what moved,
+  what remains here, where follow-up belongs), the stale downstream trackers,
+  and the exact proposed issue #32 update (prepared, not posted).
 |===
 
 == Continuity foundations