docs(secret-types): sync the #32 pointer to its closure and the standalone proofs

.machine_readable/descriptiles/META.a2ml

@@ -74,7 +74,7 @@ title = "Secret types and information-flow control are specified outside this re
 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 (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)."
+consequence = "The epistemic core keeps its scope: no confidentiality claim attaches to BeliefModality, Echo grades, or Access. epistemic-types#29 stays closed. Issue #32 was closed on 2026-10-05 as delivered here - no transfer and no duplicate; do not reopen it. Its successor guard is epistemic-types#39. The standalone repository is no longer specification-only: at ccdcb3ec42792337a9ab6047e1f99de9d20a4f96 (2026-10-19) TINI at the two-point lattice and over a Lattice record are PROVEN and its proof gate is green; declassification is not yet implemented. See docs/secret-types.adoc section Status update 2026-10-25."
 
 [development-practices]
 build-tool = "just"

.machine_readable/descriptiles/STATE.a2ml

@@ -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; 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."
+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 was closed on 2026-10-05 as delivered here, with no transfer (none required); do not reopen it, transfer it, or duplicate it - the successor guard is epistemic-types#39. The standalone repository is no longer specification-only: at ccdcb3ec42792337a9ab6047e1f99de9d20a4f96 (2026-10-19) its proof gate is green, TINI at the two-point lattice and over a Lattice record are PROVEN, and declassification is not yet implemented. Pointers: docs/secret-types.adoc section Status update 2026-10-25, and docs/secret-types-transition-review-2026-10-05.adoc kept as history."
 
 [build]
 checker = "Agda 2.6.4.3 (CI-matched)"

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; issue #32 stays open here as the origin/decision record (no transfer) until the standalone specification's review checklist completes."
+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 was closed on 2026-10-05 as delivered here (no transfer); do not reopen, transfer, or duplicate it - the successor guard is #39. The standalone repository now carries a proved noninterference theorem (ccdcb3ec42792337a9ab6047e1f99de9d20a4f96, 2026-10-19); see docs/secret-types.adoc section Status update 2026-10-25."
 
 [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; 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).",
+  "Secret types and information-flow control stay outside this repository (D153/D154; canonical specification in hyperpolymath/secret-types). Issue #32 is closed (2026-10-05, delivered here; no transfer): do not reopen, transfer, or duplicate it, and use the successor guard #39 for pointer updates (docs/secret-types.adoc section Status update 2026-10-25).",
 ]
 
 [ecosystem]

CHANGELOG.adoc

@@ -12,6 +12,36 @@ 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-25]]
+==== Changed — 2026-10-25
+
+* Secret-types pointer sync (issue #39, items 1 and 3). `epistemic-types#32` was
+  **closed on 2026-10-05T06:37Z** by the owner as delivered here, with no
+  transfer ("no transfer of this issue occurred or is required, and none should
+  be attempted"); the successor guard is `#39`. The previous text — that #32
+  stays open here and must not be closed — was accurate on 2026-10-05 and is now
+  false, so `docs/secret-types.adoc` (new section *Status update — 2026-10-25*
+  plus corrected boundary, transition-review and decision paragraphs),
+  `docs/secret-types-transition-review-2026-10-05.adoc` (kept as history, with
+  dated supersession notes), `README.adoc`, `docs/README.adoc`, `STATE.a2ml`,
+  `META.a2ml` (ADR-007) and `0-AI-MANIFEST.a2ml` were corrected. The
+  machine-readable agent instruction that said "do not close #32" now says it is
+  closed and must not be reopened.
+* Recorded the standalone repository's current state at
+  `hyperpolymath/secret-types` `main`
+  `ccdcb3ec42792337a9ab6047e1f99de9d20a4f96` (2026-10-19, proof gate green in
+  run 39305922644): N-1, N-2, N-3 and N-7 PROVEN (TINI at the two-point lattice
+  and over an arbitrary `Lattice` record, public-expression agreement,
+  confinement), N-4/N-5/N-6 TESTED, N-8 PROVEN (countermodels). The fragment has
+  no declassification, so D154's audited-declassification requirement is not yet
+  implemented.
+* Recorded that D153's family-map row landed in `nextgen-typing`
+  `docs/TYPE-CONNECTIONS.adoc` on 2026-10-05 and `nextgen-typing#118` is closed
+  (that map's explanatory note still claims no noninterference theorem exists),
+  and that `valence-shell` `docs/THEORY-FEED.adoc` remains stale under `#210`
+  with `#92` unselected. Those corrections belong to their own repositories.
+* No Agda source changed; the proof gates are unaffected.
+
 [[changed--2026-10-05]]
 ==== Changed — 2026-10-05
 

README.adoc

@@ -211,10 +211,13 @@ 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. Issue #32 stays
-  open in this repository as the origin/decision record (no transfer);
+  the decision and the pointer. No `Secret` API exists here. Issue #32 was
+  closed on 2026-10-05 as delivered here (no transfer; the successor guard is
+  link:https://github.com/hyperpolymath/epistemic-types/issues/39[#39]);
   link:docs/secret-types-transition-review-2026-10-05.adoc[the transition
-  review] records the cross-references.
+  review] records the cross-references, and the boundary note's 2026-10-25
+  status update records the standalone repository's proved noninterference
+  theorem.
 
 == Build
 

docs/README.adoc

@@ -40,14 +40,17 @@ 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. Issue #32 stays open here as the
-  origin/decision record (no transfer).
+  theorem exists in this repository. Issue #32 was closed on 2026-10-05 as
+  delivered here (no transfer; successor guard #39), and the note's 2026-10-25
+  status update records the standalone repository's proved noninterference
+  theorem.
 
 | `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).
+  and the exact proposed issue #32 update (prepared, never posted — the owner
+  posted a different closing comment on 2026-10-05). Kept as history.
 |===
 
 == Continuity foundations

docs/secret-types-transition-review-2026-10-05.adoc

@@ -16,6 +16,17 @@ issue ownership is transferred, and nothing is deleted or moved. The exact
 proposed update for issue #32 is prepared at the end of this document; it is
 *not posted*.
 
+[NOTE]
+====
+**Historical record — 2026-10-05.** The text above and throughout this document
+is kept as written on 2026-10-05. It was superseded in part the same day: the
+owner closed `epistemic-types#32` at 06:37Z as delivered here, without a
+transfer, and opened `#39` as the successor guard. See
+link:secret-types.adoc#status_2026_10_25[the 2026-10-25 status update] in
+`docs/secret-types.adoc` for the current state, including the standalone
+repository's proved noninterference theorem. Do not reopen #32.
+====
+
 toc::[]
 
 == Scope and constraint
@@ -78,8 +89,10 @@ repositories, and the destination repositories named below.
   implementation" states that the checklist "has not yet been completed item by
   item"; `epistemic-types` PR #37 carries an unresolved review finding
   (CodeRabbit, `CHANGES_REQUESTED`) about the issue-#32 open-state wording
-| The required review is **not** complete. Issue #32 must not be closed, and the
-  specification must not be described as accepted.
+| *2026-10-05 assessment, now historical:* the required review was judged
+  incomplete, so #32 was not to be closed and the specification was not to be
+  described as accepted. The owner closed #32 later that day (06:37Z); the
+  specification is still not described as accepted.
 |===
 
 == Findings
@@ -145,8 +158,9 @@ repositories, and the destination repositories named below.
 | `epistemic-types` (`docs/secret-types.adoc`, retained)
 
 | Origin/decision-record issue
-| `epistemic-types#32` — **open, no transfer**; closure only after the standalone
-  review checklist is completed item by item
+| `epistemic-types#32` — as of 2026-10-05, open with no transfer; **closed
+  2026-10-05T06:37Z as delivered here** (no transfer), with `#39` as the
+  successor guard
 
 | Non-claims about `Access.Preorder`, `BeliefModality`, `Warrant`,
   `EchoBridge.Grade`, and the `--safe --without-K` proof gate
@@ -159,15 +173,18 @@ repositories, and the destination repositories named below.
 | `secret-types#2`
 |===
 
-== Prepared update for issue #32 — not posted
+== Prepared update for issue #32 — never posted
 
-The exact proposed comment follows. It is **prepared and not posted**: the
+The exact proposed comment follows. It is **prepared and never posted**: the
 tracking gate ("only update or close tracking after the transition is evidenced
-and any required review is complete") is not met, because the standalone
-specification's own review checklist is incomplete and PR #37's review finding
-is unresolved. The credential state for issue writes was documented as
-unavailable (`403`) on 2026-10-04 in `secret-types` PR #4 and was not
-re-verified here. Nothing in this document should be read as posted.
+and any required review is complete") was judged unmet on 2026-10-05, because
+the standalone specification's own review checklist was incomplete and PR #37's
+review finding was unresolved. The credential state for issue writes was
+documented as unavailable (`403`) on 2026-10-04 in `secret-types` PR #4.
+
+The owner instead posted a different closing comment on 2026-10-05T06:37Z and
+closed the issue. The prepared text below is retained unmodified as the record
+of what this review proposed; nothing in it should be read as posted.
 
 [source,markdown]
 ----
@@ -240,15 +257,41 @@ Review record: `epistemic-types`
 (`arena/01a10aaf-epistemic-types`); pending review).
 ----
 
-== What would unblock the tracking update
+== What would unblock the tracking update — historical (2026-10-05)
 
 * The standalone specification's "Review checklist before implementation" is
   completed item by item, or the owner explicitly accepts the baseline; and
 * the unresolved PR #37 review finding is superseded or resolved (this review
   supersedes its wording); and
 * an issue-write credential is available, or the owner posts the prepared text.
 
-Until then: #32 open, in this repository; nothing moved; nothing closed.
+As written on 2026-10-05: "Until then: #32 open, in this repository; nothing
+moved; nothing closed." The owner resolved the question the same day by closing
+#32 (06:37Z) and opening #39 as the guard; see <<status_2026_10_25>>.
+
+[[status_2026_10_25]]
+== Status update — 2026-10-25
+
+* `epistemic-types#32` — **closed** 2026-10-05T06:37Z as delivered here, with
+  no transfer (and none required); `#39` is the successor guard.
+* `epistemic-types#29` — remains closed.
+* `secret-types` `main` `ccdcb3ec42792337a9ab6047e1f99de9d20a4f96`
+  (2026-10-19): proof gate green
+  (link:https://github.com/hyperpolymath/secret-types/actions/runs/39305922644[run 39305922644]);
+  reported status: N-1, N-2, N-3, N-7 and N-8 are **PROVEN**; N-4, N-5 and
+  N-6 are **TESTED**. **D154's audited-declassification requirement is not
+  implemented**: the fragment contains no declassification, and procedures,
+  concurrency and timing are likewise outside it.
+* Family map: the `nextgen-typing` row landed 2026-10-05 and `#118` is closed;
+  its explanatory note still says no noninterference theorem exists, which the
+  proofs supersede.
+* `valence-shell` `docs/THEORY-FEED.adoc` remains stale (un-minted wording,
+  `?` feed grade, "fold it into epistemic-types#32"); `#210` and `#92` remain
+  open.
+* The live specification checklist and status text are owned by
+  `secret-types`; reconciling them is that repository's work, not this one's.
+
+Nothing moved, nothing was deleted, and no `Secret`/IFC claim is added here.
 
 == References