docs: repo-wide documentation refresh — counts, paths, licence status, debt register (#352)

Reconciles the documentation surface — human, machine-readable, and the
wiki — against what the tree actually contains, and publishes what could
not be reconciled as **measured** debt rather than leaving it unstated.

## Prover counts (#251)

Five figures were in circulation — 48, 105, 128, 138, 141 — because four
different things are all called "the number of provers". Re-measured:

| Figure | Value |
|---|---|
| `ProverKind` variants | **141** |
| Backend implementation files | **105** |
| Implementations with `suggest_tactics` | **102** |
| Default-exposed core (`all_core()`) | **12** |

`docs/PROVER_COUNT.md` is now canonical, explains the denominators, and
**ships the command that reproduces each figure** — all five were run
and reproduce exactly. Present-tense claims elsewhere cite it. Dated
historical records (release notes, completed milestones) keep their
authoring-time numbers: they are records, not claims about today.

## Wiki — corrected and synced

`docs/wiki/` is the source and had drifted **ahead** of the live wiki,
which had never been synced. Two substantive errors fixed:

- the **Tier-1 core list named six backends that aren't core** (Idris 2,
F\*, Alt-Ergo, Dafny, Vampire, E Prover). The real set is Metamath, HOL
Light, Mizar, PVS, ACL2, HOL4 — anyone trusting that page would have
selected backends the default API does not expose.
- the licence was stated as **MPL-2.0** (see below).

The in-repo note claiming the wiki isn't pushable from automation was
wrong; it's replaced with a working sync recipe (note: the wiki's
default branch is `master`).

## Licence — P0, identified and deliberately NOT acted on

The repository states **four different licences**:

| Surface | States |
|---|---|
| `LICENSE`, `Cargo.toml`, README badge | AGPL-3.0-or-later |
| Per-file SPDX headers — **590 source files** | MPL-2.0 |
| Per-file SPDX headers | AGPL — **zero files** |
| `NOTICE` | MPL-2.0, citing `LICENSE` (which is AGPL) for its text |
| `.reuse/dep5` | `PMPL-1.0 AND Palimpsest-0.6` |

GitHub reports the licence as **"Other"** — likely the SPDX line
prepended above the GNU text in `LICENSE`, which stops its detector
matching.

This matters beyond tidiness: MPL is file-level weak copyleft with no
network clause; AGPL reaches users served over a network. An integrator
reading the headers would conclude they may host a modified ECHIDNA
without publishing changes. **Because per-file headers are themselves a
licence grant, that is live exposure.**

**I have not changed any licence.** Re-licensing is an owner decision
affecting existing recipients and contributors. `docs/DEBT.md` sets out
a suggested sequence and stops. Meanwhile the README and wiki now tell
readers not to rely on any surface but `LICENSE`.

## Also in this PR

- **Stale paths (#242)**: `.machine_readable/6a2/` no longer exists
(descriptiles moved to `descriptiles/`) — 17 documents repaired. The
contractile `.ncl` *write destinations* naming `6a2/` were left alone
deliberately: `6a2` is a concept name there, and repointing an evidence
sink is a semantic decision (recorded as D7).
- **Broken links 19 → 13.** The 13 remaining are dated release notes and
the playground sub-project — recorded as D4/D5 rather than silently
rewritten.
- **Root scaffold removed**: `ARCHITECTURE.md` and `GOVERNANCE.md`
contained generic template text with **zero** project-specific words
while the real documents sat elsewhere. GitHub surfaces the `.md`, so
the page most readers landed on described no particular project. Both
are now explicit pointers.
- **OpenSSF badge removed**: a hardcoded green shields.io label linking
to the *registration* form — it would have read "passed" whatever the
real standing, including now, unregistered. Restore the genuine dynamic
badge once registered.
- **Repo description and topics** updated: description had a typo
(`VersisimDB`) and the stale 48; topics dropped languages GitHub already
surfaces (agda/coq/julia), a duplicate (theorem-prover vs
theorem-proving) and a generic (artificial-intelligence), replaced with
capability terms — `proof-assistants`, `proof-search`,
`premise-selection`, `proof-certificates`, `smt-solvers`.

## New: `docs/DEBT.md`

Live debt register — P0 licensing, seven documentation items, four code
items. **Every entry carries the command that measures it**, so entries
can be retired on evidence rather than on feeling. Supersedes
`tech-debt-2026-05-26.md`, which is kept and banner-marked as a dated
snapshot.

## Verification

- R5a bare-prover-count rule: **clean** across all scoped top-level
docs.
- All five `PROVER_COUNT.md` commands run and reproduce their stated
figures.
- `DEBT.md`'s own measurements re-run before commit; one corrected (588
→ 590).
- Wiki push verified by re-cloning and re-reading the live pages.

Known unrelated red: `Governance` fails on `main` for a hypatia scanner
error (#314), not doc drift.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

Author: hyperpolymath

.claude/CLAUDE.md

@@ -2,12 +2,12 @@
 
 The following files in `.machine_readable/` contain structured project metadata:
 
-- `.machine_readable/6a2/STATE.a2ml` - Current project state and progress
-- `.machine_readable/6a2/META.a2ml` - Architecture decisions and development practices
-- `.machine_readable/6a2/ECOSYSTEM.a2ml` - Position in the ecosystem and related projects
-- `.machine_readable/6a2/AGENTIC.a2ml` - AI agent interaction patterns
-- `.machine_readable/6a2/NEUROSYM.a2ml` - Neurosymbolic integration config
-- `.machine_readable/6a2/PLAYBOOK.a2ml` - Operational runbook
+- `.machine_readable/descriptiles/STATE.a2ml` - Current project state and progress
+- `.machine_readable/descriptiles/META.a2ml` - Architecture decisions and development practices
+- `.machine_readable/descriptiles/ECOSYSTEM.a2ml` - Position in the ecosystem and related projects
+- `.machine_readable/descriptiles/AGENTIC.a2ml` - AI agent interaction patterns
+- `.machine_readable/descriptiles/NEUROSYM.a2ml` - Neurosymbolic integration config
+- `.machine_readable/descriptiles/PLAYBOOK.a2ml` - Operational runbook
 - `.machine_readable/bot_directives/*.a2ml` - Per-bot permission and scope rules
 
 ## Canonical Roadmap

.github/PROVEN-INTEGRATION.md

@@ -12,7 +12,7 @@ This document outlines the recommended [proven](https://github.com/hyperpolymath
 
 ## Integration Notes
 
-ECHIDNA as a neurosymbolic theorem proving platform supporting 128 prover backends (12 core; see [docs/PROVER_COUNT.md](../docs/PROVER_COUNT.md)) requires formally verified proof management:
+ECHIDNA as a neurosymbolic theorem proving platform (12 core backends exposed by default; see [docs/PROVER_COUNT.md](../docs/PROVER_COUNT.md) for the full tier table and count semantics) requires formally verified proof management:
 
 - **SafeGraph** models proof dependencies as DAGs. The `Acyclic` proof guarantees no circular dependencies in proof chains, and `topoSort` provides correct ordering for proof verification. `PathExists` verifies lemma reachability.
 

.machine_readable/ER.a2ml

@@ -41,8 +41,9 @@ scope   = "src/rust/core.rs + src/rust/verification/* + src/rust/dispatch.rs"
 # ═══════════════════════════════════════════════════════════════════════════════
 
 # ─── 1. Term ──────────────────────────────────────────────────────────────────
-# Universal mathematical term representation shared across all 105 prover
-# backends.  An ADT with 15 variants; self-referential via boxed children.
+# Universal mathematical term representation shared across every prover backend
+# (see docs/PROVER_COUNT.md for the canonical count and its semantics).
+# An ADT with 15 variants; self-referential via boxed children.
 #
 # No explicit integer PK — terms are compared structurally (PartialEq) or
 # via Display serialisation for hashing in proof_encoding.rs.

.machine_readable/ROADMAP.a2ml

@@ -14,7 +14,8 @@ next-review = "2026-07-13"
 
 [vision]
 summary = """
-Echidna evolves from a proof-solving library (105 provers + neurosymbolic guidance)
+Echidna evolves from a proof-solving library (multi-backend prover surface —
+see docs/PROVER_COUNT.md — plus neurosymbolic guidance)
 into a distributed, trustworthy proof-as-a-service platform accessible to the
 entire hyperpolymath estate and beyond.
 

.machine_readable/contractiles/intend/Intentfile.a2ml

@@ -9,7 +9,8 @@ Declared intent and purpose for Echidna.
 ## Purpose
 
 Echidna is a trust-hardened neurosymbolic theorem proving platform.
-It supports 128 prover backends, records every proof attempt to
+It supports 141 ProverKind variants over 105 backend implementations
+(canonical count semantics: docs/PROVER_COUNT.md), records every proof attempt to
 VeriSimDB, and feeds the Hypatia learning loop so the fleet gets
 smarter over time.
 

.machine_readable/descriptiles/AGENTIC.a2ml

@@ -3,7 +3,8 @@
 #
 # AGENTIC.a2ml — AI agent operational gating and proof-solving dispatch
 # Defines safety constraints, entropy budgets, and explicit-intent gating for AI agents
-# working in echidna (proof-solving service with 105 prover backends, 3GB training corpus).
+# working in echidna (proof-solving service; 141 ProverKind variants over 105 backend
+# implementations — see docs/PROVER_COUNT.md for count semantics; 3GB training corpus).
 
 [metadata]
 version = "0.3.0"

.machine_readable/descriptiles/ECOSYSTEM.a2ml

@@ -12,10 +12,12 @@ ecosystem = "hyperpolymath"
 [project]
 name = "ECHIDNA"
 full-name = "Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance"
-purpose = """Trust-hardened neurosymbolic theorem proving platform. 48 prover backends
-(Agda, Lean4, Isabelle, Coq, Idris2, F*, Z3, CVC5, Vampire, and 39 more). Sandboxed
-solver execution (Podman/bubblewrap), proof certificate checking, axiom tracking,
-GNN-guided proof search, Julia ML inference layer."""
+purpose = """Trust-hardened neurosymbolic theorem proving platform. 141 ProverKind
+variants across 105 backend implementations, 12 exposed by default at GET /api/provers
+(Agda, Coq, Lean 4, Isabelle/HOL, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4);
+canonical tier table and count semantics in docs/PROVER_COUNT.md. Sandboxed solver
+execution (Podman/bubblewrap), proof certificate checking, axiom tracking, GNN-guided
+proof search, Julia ML inference layer."""
 role = "prover-dispatcher"
 
 [position]

0-AI-MANIFEST.a2ml

@@ -46,7 +46,7 @@ proofs = "proofs/"
 container = "container/"
 
 [tech-stack]
-primary = "Rust (48 prover backends, trust pipeline, CLI, REPL, API servers)"
+primary = "Rust (141 ProverKind variants over 105 backend implementations — see docs/PROVER_COUNT.md; trust pipeline, CLI, REPL, API servers)"
 secondary = "Julia (ML inference, port 8090), ReScript+Deno (UI, 33 files, zero TypeScript)"
 optional = "Chapel (parallel proof dispatch)"
 abi = "Idris2 (7 modules, zero believe-me)"
@@ -56,8 +56,9 @@ build = "Justfile (primary), Cargo workspace"
 container = "Podman + Containerfile"
 
 [architecture]
-# Trust-hardened neurosymbolic theorem proving with 48 prover backends
-core = "src/rust/"                  # 48 provers, trust pipeline, dispatch
+# Trust-hardened neurosymbolic theorem proving; canonical backend count and
+# count semantics live in docs/PROVER_COUNT.md
+core = "src/rust/"                  # ProverKind enum + backends, trust pipeline, dispatch
 verification = "src/rust/verification/" # Portfolio, certificates, axiom tracker, confidence, mutation, pareto, statistics
 integrity = "src/rust/integrity/"   # Solver binary integrity (SHAKE3-512, BLAKE3)
 executor = "src/rust/executor/"     # Sandboxed execution (Podman, bubblewrap)

AFFIRMATION.adoc

@@ -36,7 +36,7 @@ available.
   real release line is in `CHANGELOG.md`.
 . *Critical Reception Grade.* CRG-C is complete (unit + smoke + build + P2P +
   E2E + contract + aspect + benchmarks baselined, per
-  `.machine_readable/6a2/STATE.a2ml`); CRG-B criteria are populated but B is
+  `.machine_readable/descriptiles/STATE.a2ml`); CRG-B criteria are populated but B is
   *not* formally affirmed here.
 
 == Verified as of 2026-06-15 (green / reproduced)

ARCHITECTURE.md

@@ -1,47 +1,26 @@
-# Architecture
-
-## Overview
-
-This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability.
-
-## Directory Structure
-
-```
-.
-├── src/           # Source code
-├── tests/        # Test suites
-├── docs/         # Documentation
-├── scripts/      # Utility scripts
-├── config/       # Configuration files
-├── LICENSE       # License file
-├── LICENSES/     # Full license texts
-└── README.adoc   # Project documentation
-```
-
-## Design Principles
+<!--
+  SPDX-License-Identifier: CC-BY-SA-4.0
+  SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
-- **Separation of Concerns**: Each module has a single responsibility
-- **Testability**: Code is written to be easily testable
-- **Documentation**: All public APIs are documented
-- **Configuration**: Environment-specific settings are externalized
+  docs/ARCHITECTURE.md is canonical. This file previously held generic
+  scaffold text ("modular, maintainable architecture designed for clarity,
+  scalability...") that contained no project-specific content — it described
+  no part of ECHIDNA and duplicated nothing real. Replaced with a pointer
+  rather than deleted, because the path is referenced externally.
+-->
 
-## Dependencies
-
-- External dependencies are minimized and clearly declared
-- Version pinning is used for reproducibility
-
-## Security Considerations
-
-- Sensitive data is never committed to the repository
-- Secrets are managed through environment variables or secure vaults
-- Regular dependency audits are performed
-
-## Maintainability
+# Architecture
 
-- Code follows consistent style guidelines
-- Pull requests require review and CI checks
-- Issues and discussions are tracked transparently
+The architecture documentation for ECHIDNA lives in
+[`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md) — the polyglot layout, the
+dispatch path, the trust-hardening pipeline, and how the Rust core, Julia ML
+sidecar, Idris2 ABI, Zig FFI and optional Chapel parallel layer fit together.
 
----
+Related canonical documents:
 
-*Last updated: 2026-07-18*
+- [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md) — backend tier table and what
+  each published count actually counts
+- [`docs/ROADMAP.md`](docs/ROADMAP.md) — stage map and current direction
+- [`docs/DEBT.md`](docs/DEBT.md) — known licence, documentation and code debt
+- [`.machine_readable/descriptiles/META.a2ml`](.machine_readable/descriptiles/META.a2ml)
+  — the machine-readable architecture record