docs: finish de-monorepo-ing the trackers and prose

Sweep the stale in-tree / count residue the reconciliation PRs did not reach:
- PROOF-NEEDS.md: drop the ~456,000-LOC count and reframe the in-tree paths as
  living in each language's own repo (this coordinator holds no proof code).
- README.adoc: disambiguate the Tangle language from the out-of-scope KRL
  resolution stack (heading, database-relationship line, entry-point note).
- EXPLAINME.adoc: reconcile the language count (was 'ten / eight core + two') to
  the current 14 languages + KitchenSpeak DSL, pointing at LANGUAGES.a2ml as
  canonical and noting the representative table is a subset.
- language-status-tracker.jl: make the repos dir overridable via
  HYPERPOLYMATH_REPOS_DIR so it is not pinned to ~/Documents.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016t5KLJDtqdeDi1EMNqNx6K

Author: claude

EXPLAINME.adoc

@@ -22,20 +22,21 @@ NOTE: `tentacles-agentic-syllabus` is NOT a programming language. It is an
 educational framework using My-Lang's dialects as a curriculum vehicle. Never
 audit it as a language implementation.
 
-== Claim 1: "Ten languages that cover the full spectrum of modern software challenges"
+== Claim 1: "A family of languages covering the full spectrum of modern software challenges"
 
 [quote, README]
 ____
-A coordinated effort to design and develop ten programming languages that
+A coordinated effort to design and develop a family of programming languages that
 collectively cover the full spectrum of modern software challenges, from
 AI-native development to formally verified real-time systems.
 ____
 
 === How it works
 
-The eight core languages plus two specialised languages are designed to
-complement each other, not compete. They occupy distinct cells in the design
-space (each maintained as a standalone `hyperpolymath/<lang>` repo):
+The family currently spans fourteen languages plus the KitchenSpeak DSL — the canonical
+list is `.machine_readable/LANGUAGES.a2ml`. They are designed to complement each other, not
+compete, each occupying a distinct cell in the design space (each maintained as a standalone
+`hyperpolymath/<lang>` repo). The table below shows the representative core:
 
 [cols="1,1,2,1"]
 |===
@@ -90,9 +91,14 @@ Gossamer backend. Rust compiler, Coq proofs.
 | Rust (17 crates), Coq proofs
 |===
 
+NOTE: The table shows a representative core. The full family also includes *betlang*
+(probabilistic), *JtV* (systems / Harvard architecture), *Haec* (trope-particularity),
+*error-lang* (pedagogical), *Tangle* (topological), and *007* (a private agent
+meta-language) — see `.machine_readable/LANGUAGES.a2ml` for the canonical registry.
+
 NOTE: *KitchenSpeak* — an experimental applied-type-theory teaching DSL
 (seven-type kitchen orchestration: Tropical, Linear, Choreographic, Echo,
-Dyadic, Ceremonial, Primitive) — is NOT one of the ten core languages and is
+Dyadic, Ceremonial, Primitive) — is NOT one of the core languages above and is
 no longer carried in this repo. It is canonical at the standalone
 link:https://github.com/hyperpolymath/kitchenspeak[`hyperpolymath/kitchenspeak`]
 repository (v2.0: physics-in-the-types, reference OCaml compiler, machine-checked

PROOF-NEEDS.md

@@ -6,10 +6,14 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 ## Current State
 
-- **src/abi/*.idr**: YES (in oblibeny) — `Interface.idr`
-- **Dangerous patterns**: 4 `Admitted` in ephapax/formal/Semantics.v (ctx_transfer 15/24, subst_lemma, preservation)
-- **LOC**: ~456,000 (OCaml + Rust + Coq + Idris2 + Lean)
-- **Existing proofs**: Ephapax has Coq proofs, Tangle has Lean proofs, Idris2 in multiple sub-languages
+`nextgen-languages` is a pure coordinator and holds **no** proof code. This file tracks the
+family's proof gaps across the standalone `hyperpolymath/<lang>` repos; every path below is
+relative to the named language's own repo, not this one.
+
+- **Ephapax** — Coq proofs present; 4 `Admitted` remain in `formal/Semantics.v` (ctx_transfer 15/24, subst_lemma, preservation, + one more).
+- **Tangle** — Lean proofs present (`Tangle.lean`); coverage partial.
+- **Oblíbený** — Idris2 ABI present (`src/abi/Interface.idr`); minimal.
+- **AffineScript** — OCaml type checker + Rust runtime; soundness proofs outstanding.
 
 ## What Needs Proving
 

README.adoc

@@ -43,9 +43,9 @@ Status: design-stage, with partial specifications and experimental implementatio
 
 ---
 
-=== KRL — Knot Resolution Language (Tangle)
+=== Tangle
 
-A topologically inspired language where programs are represented as tangles (braids), and equivalence is defined by isotopy.
+A topologically inspired language where programs are represented as tangles (braids), and equivalence is defined by isotopy. Its IR (TangleIR) is consumed by the separate *KRL resolution stack* (`krl → TangleIR → VeriSimCore → Skein.jl / QuandleDB`), which is tracked by the database estate — not part of this coordinator's language family.
 
 * Composition and tensor operations correspond to braid structure
 * Formal semantics specified
@@ -141,7 +141,7 @@ Type-theoretic boundaries are made explicit: total proof-like fragments are dist
 
 These languages are designed to work with systems that treat equivalence, provenance, and semantic identity as first-class concepts:
 
-KRL ↔ QuandleDB / Skein
+Tangle (via the separate KRL resolution stack) ↔ QuandleDB / Skein
 JtV ↔ future equivalence-aware runtime and storage models
 
 See the nextgen-databases repository for details.
@@ -196,7 +196,7 @@ production system. The work it tracks spans, across the individual language repo
 Each language lives in its own `hyperpolymath/<lang>` repo; start there. For orientation:
 
 * link:https://github.com/hyperpolymath/tangle[`hyperpolymath/tangle`] — `Tangle.lean`, the
-  mechanised type-safety proof for the Tangle (KRL) core; topological language design
+  mechanised type-safety proof for the Tangle core; topological language design
 * link:https://github.com/hyperpolymath/jtv[`hyperpolymath/jtv`] — computation as
   path-based construction
 

language-status-tracker.jl

@@ -5,7 +5,7 @@
 
 using Dates
 
-const REPOS_DIR = joinpath(homedir(), "Documents/hyperpolymath-repos")
+const REPOS_DIR = get(ENV, "HYPERPOLYMATH_REPOS_DIR", joinpath(homedir(), "Documents/hyperpolymath-repos"))
 
 # All known language repos
 const LANGUAGES = [