From 6ff3d932a2f8ccf01e9e5f416bc6eb97d9422f62 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 17 Aug 2026 16:11:25 +0100
Subject: [PATCH] Add EXPLAINME document detailing claims and implementations

This document outlines the claims and implementations related to the type theory pipeline, including governance patterns, historical records, and known gaps in the repository.

Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
---
 EXPLAINME-new.adoc | 107 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 107 insertions(+)
 create mode 100644 EXPLAINME-new.adoc

diff --git a/EXPLAINME-new.adoc b/EXPLAINME-new.adoc
new file mode 100644
index 0000000..9a37782
--- /dev/null
+++ b/EXPLAINME-new.adoc
@@ -0,0 +1,107 @@
+// SPDX-License-Identifier: MPL-2.0
+= Ideas to Alphas — EXPLAINME
+:toc: preamble
+:toc-title: Contents
+:icons: font
+:doctype: article
+
+This file backs every factual claim in link:README.adoc[README.adoc] with code paths and honest caveats. Read it if you are doing due diligence on whether the story matches the code.
+
+== Claim-to-implementation map
+
+=== This is the theory→practice incubator in the type theory pipeline
+
+[quote, README.adoc]
+____
+Findings from the lab (Kategoria) are matured from idea to alpha here, before earning their own production repository.
+____
+
+How this is implemented::
+The pipeline role is documented in `link:dev-notes/2026-06-16-typing-sub-estate-roles-and-lifecycle.adoc[]`. The repository contains prototype formalisations (Idris 2, Lean 4, Agda), research notes, and experimental definitions. No production code exists here; the graduation path to `typell` is by design, not by current automation.
+
+Caveat::
+**The pipeline is a governance pattern, not a CI pipeline.** There is no automated promotion from "idea" to "alpha" to "production." Graduation is a human decision based on review, proof stability, and downstream readiness.
+
+=== The L1–L10 framework was designed here first
+
+[quote, README.adoc]
+____
+The current L1-L10 implementation in typell was designed here first, then graduated.____
+
+How this is implemented::
+The historical record is in the git log and research notes. The type-safety level definitions originated as speculative research artefacts before being promoted to `typell`'s formal specification layer.
+
+Caveat::
+This is a provenance claim about the development history, not a mathematical claim. The levels themselves are assembled from standard type theory; the contribution is the 10-level framing and the progressive-safety architecture, not the individual levels.
+
+=== a-sounder-constitution contains an Idris 2 formalisation
+
+[quote, README.adoc]
+____a-sounder-constitution/: Idris 2 formalisation of soundness constraints____
+
+How this is implemented::
+`link:a-sounder-constitution/[]` contains Idris 2 modules. CI gates the proof with `idris2 --check` (see `.github/workflows/`). The formalisation addresses soundness constraints for the type theory pipeline.
+
+Caveat::
+This is a proof-of-concept, not a production proof. It may not cover all soundness obligations for the full pipeline. Its value is as a constitutional scaffold—a statement of what we intend to prove, with initial proof structure.
+
+=== This repo is deliberately unstable
+
+[quote, README.adoc]
+____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.
+
+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.
+
+== Known gaps
+
+[CAUTION]
+====
+**Pre-alpha with minimal content.** The repository was created 2026-04-11. Most directories contain scaffolding from `rsr-template-repo` rather than mature research artefacts. Substantive content is accumulating over time.
+====
+
+[CAUTION]
+====
+**Mid-rename.** The GitHub repository is still named `kategoria-pipeline`. The rename to `ideas-to-alphas` is documented but not executed. References to the old name may persist in CI, documentation, and cross-repo links.
+====
+
+[CAUTION]
+====
+**No automated graduation.** The idea→alpha→production pipeline is a governance pattern, not automated. There are no CI gates that promote artefacts or block premature promotion.
+====
+
+[CAUTION]
+====
+**Experimental levels are speculative.** Any candidate for L11+ defined here is a research hypothesis, not an accepted level. It may be retracted, merged with an existing level, or restructured.
+====
+
+== Evidence Index
+
+[cols="2,3", options="header"]
+|===
+| Path | Proves / Contains
+
+| `a-sounder-constitution/`
+| Idris 2 soundness constraint formalisation (proof-of-concept)
+
+| `research/`
+| Reading notes, paper formalisations, experimental definitions
+
+| `verification/`
+| Prototype proofs and proof-of-concept checkers
+
+| `silo/`
+| Secret-silo ALARP design incubation
+
+| `dev-notes/2026-06-16-typing-sub-estate-roles-and-lifecycle.adoc`
+| Pipeline role definitions and lifecycle
+
+| `PROOF-STATUS.md`
+| Proof status tracking
+
+| `ROADMAP.adoc`
+| Research roadmap
+|===