Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
# Cross-repo maintenance baseline (machine-readable canonical)

[metadata]
name = "Cross-repo maintenance checklist"
version = "1.1.0"
last-updated = "2026-02-24"
scope = "cross-repo"
Expand Down
4 changes: 1 addition & 3 deletions EXPLAINME-new.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ This is a proof-of-concept, not a production proof. It may not cover all soundne
____Anything with stability guarantees — this repo is deliberately unstable.____

How this is implemented::
There is no versioning contract, no API stability guarantee, and no ABI freeze. Artefacts may be retracted or rewritten. The `PROOF-STATUS.md` and `ROADMAP.adoc` track what exists and what is speculative.
There is no versioning contract, no API stability guarantee, and no ABI freeze. Artefacts may be retracted or rewritten. The `PROOF-STATUS.md` tracks what exists and what is speculative.

Caveat::
This is the correct stance for an incubator. Downstream repositories (`typell`, `typed-wasm`) must not depend on this repo at build time. Importing ideas from here is by port-and-reprove, not by dependency.
Expand Down Expand Up @@ -102,6 +102,4 @@ This is the correct stance for an incubator. Downstream repositories (`typell`,
| `PROOF-STATUS.md`
| Proof status tracking

| `ROADMAP.adoc`
| Research roadmap
|===
26 changes: 26 additions & 0 deletions GRADUATION.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
// SPDX-License-Identifier: CC-BY-SA-4.0
= Graduation rule — katagoria is an incubator, not a family
:revdate: 2026-10-12

An idea may live here as a sketch, a prototype, or a prover-agnostic
scribble. It *leaves* only when a family repo (echo, choreographic, tropical,
epistemic, occupancy, residual-evidence, secret) holds its core theorem
kernel-checked under the family ruling (Agda `--safe --without-K`) with the
six-item kit: a theorem a reader could bet against, a separation witness
from its nearest sibling, reject controls, a laws census, one sibling
connection discharged by import, and a PROOF-STATUS where prose and
artefact agree. Until then its status here is DESIGNED at best, and this
file is the only place that may say so.

== Register

[cols="1,2,1",options="header"]
|===
| Candidate | Where it stands | Status
| L11 modal box | Superseded by the graded rewrite; the box modality now lives in epistemic-types `Kripke/` (indexed, with correspondences) | CLOSED — superseded, 2026-10-12
| TropicalKleene (Idris) | Fourth formalisation of max-plus; the family instance is resource-algebra `MaxPlus` (Agda). Keep as the Idris runtime sketch, not as a proof | DESIGNED (runtime sketch)
| Constitution formalisation | Prototype | DESIGNED
|===

PROOF-STATUS.adoc's "0 of 7" is therefore not a debt: an incubator carries
no proof obligations of its own. The template ROADMAP is retired by this file.
Comment thread
hyperpolymath marked this conversation as resolved.
22 changes: 0 additions & 22 deletions ROADMAP.adoc

This file was deleted.

1 change: 1 addition & 0 deletions docs/governance/MAINTENANCE-CHECKLIST.a2ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
# Cross-repo maintenance baseline (machine-readable canonical)

[metadata]
name = "Cross-repo maintenance checklist"
version = "1.1.0"
last-updated = "2026-02-24"
scope = "cross-repo"
Expand Down
Loading