docs(type-connections): register the Secret Types family (nextgen-typing#118)

.machine_readable/bot_directives/placement.a2ml

@@ -10,7 +10,7 @@
 
 [metadata]
 version = "1.0.0"
-last-updated = "2026-09-09"
+last-updated = "2026-10-05"
 applies-to = "nextgen-typing"
 precedence = "maintainer > this directive > bot defaults"
 
@@ -52,6 +52,7 @@ rules = [
   { subject = "WasmGC memory-safety proofs, verified convergence ABI, aggregate-library conventions", owns = "typed-wasm" },
   { subject = "echo-types library: fiber-based structured loss (Echo/EchoLinear/EchoResidue/EchoCharacteristic)", owns = "echo-types", companion = "EchoTypes.jl" },
   { subject = "standpoint-indexed access, warrants and sound proof transport", owns = "epistemic-types" },
+  { subject = "confidentiality labels / information-flow control (secret types)", owns = "secret-types" },
   { subject = "evidence-indexed residual models, explorer, candidate-world proofs and tests", owns = "residual-evidence-types" },
   { subject = "cross-project type-family map, shared glossary and connection obligations", owns = "nextgen-typing" },
   { subject = "choreographic / multiparty session types", owns = "choreographic-types" },

docs/TYPE-CONNECTIONS.adoc

@@ -4,11 +4,11 @@
 :toc:
 :icons: font
 
-This is the shared reading guide for the five research families in the map.
+This is the shared reading guide for the six research families in the map.
 It coordinates vocabulary and ownership; the owning repositories define
 their formal interfaces and carry their proof evidence.
 
-image::images/type-connections.svg[Five type research families connected by explicitly conceptual arrows, width=1100]
+image::images/type-connections.svg[Six type research families with explicitly conceptual arrows, width=1100]
 
 *Read every dashed arrow as a conceptual use or a proposed research task.*
 An arrow does not assert a package dependency, a checked bridge, an
@@ -58,6 +58,19 @@ a global interaction protocol is projected to local participants?
 |The general K-CUT result is open in the reviewed project description.
 A causal-order frontier called a cut is not Gentzen cut-elimination;
 it is also not a statistical causal-identification result.
+
+|https://github.com/hyperpolymath/secret-types[Secret Types]
+|Which value flows does a confidentiality label permit, and what may a
+lower-cleared observer learn from an output? A `Secret ℓ A` classifies a
+value at a label `ℓ`; the first model is a two-level `Public ⊑ Secret`
+order over a pure, total calculus, targeting termination-insensitive
+noninterference for public observations.
+|A label is not cryptography and not an epistemic standpoint: `Secret ℓ A`
+does not make a value unreadable, authenticate a principal, enforce
+runtime access control, or hide timing, storage or network side channels.
+The baseline declassifies nothing, and no consumer or frontier item is
+selected for it (2026-10-04); the RMO key-provisioning/disclosure fit is
+a name-level inference, not a claim.
 |===
 
 These are complementary research questions, not successive ranks in a
@@ -151,6 +164,12 @@ task, not an equivalence asserted here.
   Agda core, and tests or proofs specific to that model.
 * `echo-types`, `epistemic-types`, `tropical-types`, `choreographic-types`:
   each family's definitions, implementations and own proof evidence.
+* `secret-types`: the confidentiality-label and information-flow
+  specification: its question, boundary, first two-level model and review
+  checklist. It is specification-stage — no `Secret` type, information-flow
+  calculus, declassification rule or noninterference theorem exists there
+  yet — so this guide asserts no connection obligation for it, and a
+  documentation link is not a mechanised dependency.
 * `kategoria`: language-development experiments. It is a separate project
   from the old `katagoria` repository name, which GitHub now resolves to
   `ideas-to-alphas`.
@@ -226,13 +245,24 @@ and in the linked hosted job with Agda 2.6.4.3 under `--safe --without-K`.
 This is a bounded result: the complete constituent proof suites were not
 rerun, and unrelated local Epistemic work is outside the receipt.
 
+The Secret Types row was added on 2026-10-05 from that repository's reviewed
+and merged scope statement (`secret-types` PR #4, merged 2026-10-04, with the
+2026-10-04 owner confirmation and rulings D153 and D154 recorded there). The
+row registers the family on its stated boundary; it is not an implementation
+claim. The scope statement itself records that no `Secret` type,
+information-flow calculus, declassification rule or noninterference theorem
+exists yet, that its review checklist has not been completed item by item, and
+that no consumer or frontier item is selected, so no connection obligation is
+asserted for it in this guide.
+
 Primary project entry points:
 
 * https://github.com/hyperpolymath/echo-types[Echo Types README and foundation contract]
 * https://github.com/hyperpolymath/epistemic-types[Epistemic Types README]
 * https://github.com/hyperpolymath/tropical-types[Tropical Types README]
 * https://github.com/hyperpolymath/choreographic-types[Choreographic Types README]
 * https://github.com/hyperpolymath/residual-evidence-types/blob/main/residual-evidence-assessment.md[Imported residual assessment]
+* https://github.com/hyperpolymath/secret-types[Secret Types README and scope statement]
 
 GitHub repository API lookups on that date resolved `tropical-resource-typing`
 to `tropical-types` and `katagoria` to `ideas-to-alphas`, while `kategoria`

docs/images/type-connections.dot

@@ -3,7 +3,7 @@
 digraph TypeConnections {
   graph [rankdir=TB, bgcolor="#f5f7fb", pad="0.35", nodesep="0.45", ranksep="0.8", splines=polyline,
     fontname="DejaVu Sans", fontsize=22, fontcolor="#17243b", labelloc=t,
-    label="Type research: questions and connections\n\nnextgen-typing · coordination map · September 2026",
+    label="Type research: questions and connections\n\nnextgen-typing · coordination map · October 2026",
     comment="SPDX-License-Identifier: MPL-2.0; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell"];
   node [shape=box, style="rounded,filled", fillcolor="#ffffff", color="#a6b4c9",
     fontname="DejaVu Sans", fontsize=13, fontcolor="#17243b", margin="0.22,0.2", penwidth=1.4];
@@ -27,6 +27,8 @@ digraph TypeConnections {
     choreographic [fillcolor="#ebf3fd", color="#7f9bbb",
       label=<<B>Choreographic Types</B><BR/><BR/>What is preserved when a global protocol<BR/>is projected to its participants?<BR/><BR/><FONT POINT-SIZE="10">choreographic-types · research programme<BR/><B>K-CUT remains open</B></FONT>>,
       URL="https://github.com/hyperpolymath/choreographic-types"];
+    secret [label=<<B>Secret Types</B><BR/><BR/>Which value flows does a<BR/>confidentiality label permit, and what<BR/>may a lower observer learn?<BR/><BR/><FONT POINT-SIZE="10">secret-types · specification only<BR/><B>no calculus or theorem yet · no connections asserted</B></FONT>>,
+      URL="https://github.com/hyperpolymath/secret-types"];
   }
 
   echo -> residual [label="refine the fibre\nwith evidence"];