Skip to content

type-map: register occupancy-types; cost/state vocabulary split; boundary notes for kategoria/typell/absolute-zero/januskey; secret-types pending #118

Description

@arena-ai-coding-agent

Context

docs/TYPE-CONNECTIONS.adoc is the estate's coherence mechanism for the type-research families: shared glossary, boundary statements, connection obligations, ownership routing. A 2026-09-27 sweep of the type-set shows three drift risks the map does not yet cover, plus two naming hazards. This issue tracks the sweep; per-repo issues link back here.

Checked this date: nextgen-typing, occupancy-types, kategoria, typell, absolute-zero, januskey, secret-types, echo-types, epistemic-types, residual-evidence-types, choreographic-types, tropical-types (README/description/state via API). Related: #115 (TYPE-CONNECTIONS receipts), echo-types#197 (clade registration).

Gaps

  1. occupancy-types is unregistered. It is the state-resource counterpart of Tropical Types (cost): its thesis is the cost/state separation (max-plus vs the HWM monoid (p₁,n₁)·(p₂,n₂) = (max(p₁, n₁+p₂), n₁+n₂)) and protocol-frontier reclamation. Its ULTRAPLAN §5 vocabulary fence (cost grade ≠ occupancy grade ≠ echo index ≠ residue measure ≠ warrant) is an extension of this map's glossary that nobody has cross-checked. Its T2 ("buffer grade commutes with endpoint projection") and R5 are precisely the Tropical→Choreographic-style obligations the map tracks. It has shipped a working Session IR checker + stepper (14/14 fixtures green, 2026-09-27) and is exactly the kind of node that drifts when unlisted. (I have opened its README/glossary side of the link already: occupancy-types@1004e49.)
  2. secret-types is un-minted (README is still {{PROJECT_NAME}} template text) yet referenced by epistemic-types#32 and by occupancy-types' ULTRAPLAN no-import list. It cannot take a map row until it has a question and a boundary; the row must wait, the tracking must not.
  3. Boundary notes missing for non-family type-set repos. The map's "Where things belong" covers kategoria/typell but nothing on absolute-zero (CNO/OND) and januskey (reversible file ops). Two vocabulary collisions surfaced:
    • absolute-zero ships a "residue list of out-of-scope observables" — this map's glossary defines Residue as "information retained after a transformation". Three-way collision with the numerical residual already fenced here.
    • kategoria's "10 levels of type safety" is a strength ladder; this map states families "are complementary research questions, not successive ranks in a universal hierarchy of type-system strength". Both are legitimate; the two taxonomies need an explicit non-conflation note.
  4. Naming hazards (one is already half-documented): tropical-resource-typing (used in occupancy-types ULTRAPLAN D1/R0-A) resolves to tropical-types; katagoria→ideas-to-alphas ≠ kategoria. Occupancy-types has recorded the errata in its decision log. Suggest the map's naming note grows one line covering the ULTRAPLAN spelling.

Proposed patch to TYPE-CONNECTIONS.adoc (owner wording wins)

"What each family means" table — new row:

| Occupancy Types | How do live-state footprints compose, and when are they reclaimed? Acquired-and-released resources compose by the high-water-mark monoid (p₁,n₁)·(p₂,n₂) = (max(p₁, n₁+p₂), n₁+n₂); closing a session endpoint names the reclamation point of its epoch. | An occupancy bound is not a cost bound: costs compose with +/max (max-plus), state composes by the HWM monoid, and neither reduces to the other. A measured live-byte count is a run statistic, not an occupancy grade. |

"Shared glossary" — additions:

| Occupancy grade | An element of a state-resource algebra (the HWM monoid) bounding live acquired-and-not-released resources. Distinct in kind from a cost grade. |
| High-water-mark monoid | (p₁,n₁)·(p₂,n₂) = (max(p₁, n₁+p₂), n₁+n₂), unit (0,0); sequential composition of state resources. Non-commutative, unlike max-plus. |

Optionally amend the existing Resource grade row: "…used for compositional usage or cost accounting. Resource algebras are of two kinds — cost (e.g. max-plus) and state (e.g. the HWM monoid) — and are not interchangeable."

"What each connection asks us to establish" — additions:

| Tropical → Occupancy | Costs and state are separate axes; a certificate may carry both, and one program may carry two bounds. | The separation statement with non-commutativity witnesses (occupancy-types R2 / algebra sibling tropical-types); a proof that the HWM monoid does not reduce to max-plus. |
| Occupancy → Choreographic | Compose buffer/occupancy grades when a global protocol is projected to participants. | A grade-preserving projection theorem (occupancy-types' T2; its R5 is the same question from the projection side). |

"Where things belong" — additions:

  • occupancy-types: the session-IR calculus, checker and stepper, the Occ occupancy spike, and stackcert. Registered here as the state-resource family node.
  • absolute-zero, januskey: applications/verification projects outside the five-family map. absolute-zero's "residue list" is an out-of-scope-observables list — not the glossary's Residue; reconcile or rename (its issue linked below). januskey's pending reversibility formalisation is a candidate consumer of, or sibling to, absolute-zero's CNO pillar — decided there, not here.

Naming note — one line: "occupancy-types ULTRAPLAN (D1/R0-A) uses the historical tropical-resource-typing spelling; canonical is tropical-types."

Checklist

  • Map patch above lands (PR from owner preferred; this issue body is the source)
  • type-connections.dot + SVG rebuilt (just type-map)
  • occupancy-types README/glossary reciprocal links (done upstream, 1004e49)
  • kategoria issue (taxonomy non-conflation + reciprocal link) — filed, see below
  • typell issue (reciprocal link + vocabulary alignment) — filed, see below
  • absolute-zero issue (residue-list collision + proposed OND connection rows) — filed, see below
  • januskey issue (cross-link to CNO pillar or IS-NOT) — filed, see below
  • secret-types issue (mint + define + register) — filed, see below
  • choreographic-types: reviewer for the Occupancy→Choreographic row (its ci(rust): convert rust-ci.yml to thin wrapper (standards#174 refile) #15 covers the separate overclaim problem; the "echo loss-grade" reconciliation already noted in the map stays open)

Per-repo issue links will be edited into this body as they land.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions