diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml
index 29bf9c3..882c0bd 100644
--- a/.machine_readable/6a2/META.a2ml
+++ b/.machine_readable/6a2/META.a2ml
@@ -28,7 +28,7 @@ author = "Jonathan D.A. Jewell (hyperpolymath)"
 build-tool = "just"
 container-runtime = "podman"
 ci-platform = "github-actions"
-package-manager = "cargo"  # Rust crate; guix/nix dev-shells are a future addition.
+package-manager = "cargo"  # Rust crate; guix/guix dev-shells are a future addition.
 
 [maintenance-axes]
 scoping-first = true
@@ -52,7 +52,7 @@ perfective-source = "axis-1 honest state after corrective/adaptive updates"
 [axis-3-audit-rules]
 audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed"
 compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks"
-drift-risk-example = "single exception broadening into policy violation (e.g. ReScript->TypeScript spread)"
+drift-risk-example = "single exception broadening into policy violation (e.g. AffineScript->TypeScript spread)"
 effects-evidence = "benchmark execution/results and maintainer status dialogue/review"
 
 [design-rationale]
diff --git a/.machine_readable/rsr-profile.a2ml b/.machine_readable/rsr-profile.a2ml
index ac23c1e..69da224 100644
--- a/.machine_readable/rsr-profile.a2ml
+++ b/.machine_readable/rsr-profile.a2ml
@@ -19,6 +19,6 @@ remove = []   # preset capabilities this repo does NOT have
 no-abi = "language-agnostic engine; no C-ABI/FFI seam, no Idris2 ABI proofs (no abi.ipkg / src/interface/)"
 no-formal-proofs = "consumes Agda — shells out to agda / agda-unused — but contains no in-tree proofs (no verification/proofs/)"
 no-container = "ships a CLI binary, not a container image"
-no-reproducible-build = "cargo build only for now; guix.scm / flake.nix are a future addition, not present"
+no-reproducible-build = "cargo build only for now; guix.scm / flake.guix are a future addition, not present"
 no-affinescript = "pure Rust; the planned AffineScript visual layer is a separate repo (arghda-studio)"
 no-governance-tier = "leaf tool; declines the full AUDIT / AFFIRMATION / GOVERNANCE / MAINTAINERS trio"
diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc
new file mode 100644
index 0000000..1c0a7a6
--- /dev/null
+++ b/ARCHITECTURE.adoc
@@ -0,0 +1,48 @@
+== 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
+
+* *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
+
+=== 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
+
+* Code follows consistent style guidelines
+* Pull requests require review and CI checks
+* Issues and discussions are tracked transparently
+
+'''''
+
+_Last updated: 2026-07-18_
diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md
deleted file mode 100644
index 607e3d8..0000000
--- a/ARCHITECTURE.md
+++ /dev/null
@@ -1,47 +0,0 @@
-# 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
-
-- **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
-
-## 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
-
-- Code follows consistent style guidelines
-- Pull requests require review and CI checks
-- Issues and discussions are tracked transparently
-
----
-
-*Last updated: 2026-07-18*
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
new file mode 100644
index 0000000..2f466e2
--- /dev/null
+++ b/CHANGELOG.adoc
@@ -0,0 +1,92 @@
+== Changelog
+
+All notable changes to arghda-core are documented here. The format
+follows https://keepachangelog.com/[Keep a Changelog], and this project
+adheres to https://semver.org/[Semantic Versioning].
+
+=== [Unreleased]
+
+==== Changed
+
+* Standards / RSR alignment and root cleanup: `+README.md+` →
+`+README.adoc+` (adoc-first; refreshed to the feature-complete v0.1
+status), no duplicate doc formats. Added `+EXPLAINME.adoc+` (orientation
+pointer), `+LICENSE+` (full MPL-2.0 text), and `+CODE_OF_CONDUCT.md+`
+(Contributor Covenant 2.1). Prose docs carry `+CC-BY-SA-4.0+`;
+code/config/state stay `+MPL-2.0+` (per the estate licence policy).
+Refreshed `+.machine_readable/6a2/STATE.a2ml+` + `+META.a2ml+` and the
+`+0-AI-MANIFEST.a2ml+` read-order; removed local `+dist-newstyle/+`
+build cruft.
+* Formal SPDX licence invariant (owner-directed): every tracked file
+carries the correct header — `+MPL-2.0+` for code/config/scripts/state,
+`+CC-BY-SA-4.0+` for prose — applied per file (incl. all `+src/*.rs+`)
+and enforced by `+scripts/check-spdx.sh+`, wired into `+just check+` and
+Rust CI. Third-party, generated (`+Cargo.lock+`), and test-data
+(`+tests/fixtures/+`) files are explicitly excluded and never
+relicensed; `+docs/*.adoc+` normalised from `+CC-BY-4.0+` to
+`+CC-BY-SA-4.0+`. Declared in
+`+.machine_readable/licensing-policy.toml+`.
+
+==== Added
+
+* `+dag+` command emitting the dependency-DAG JSON contract (nodes with
+lint-derived status, import edges, and a `+blocked+` list covering
+self-blocks and prerequisite-blocks).
+* `+check+` command: Agda typecheck fused with the lint report
+(`+proven-eligible+` / `+rejected+` / `+agda-unavailable+`); degrades
+gracefully when `+agda+` is absent.
+* Workspace state machine — `+claim+` / `+promote+` / `+reject+` /
+`+requeue+` / `+invalidate+` as validated file moves, each logged to
+`+.arghda/events.jsonl+`; plus `+events+` to replay the log.
+* First-class import graph (`+graph+` module) with multi-root
+reachability: orphan detection is the union of auto-discovered
+`+All.agda+` / `+Smoke.agda+` CI roots (or `+--entry+`, repeatable).
+* Lint rules: `+unjustified-postulate+` (hard-block), `+escape-hatch+`
+(warn: `+TERMINATING+`-family pragmas + `+believe_me+` /
+`+primTrustMe+`), `+tab-mix+` (warn).
+* `+unpinned-headline+` (warn): flags a top-level theorem whose name
+matches the headline pattern but is not pinned in any `+Smoke.agda+` via
+a `+using ( … )+` clause. The pattern is operator-configurable via
+`+--headline-pattern <regex>+` on `+scan+` / `+dag+` (default
+`+^[a-z][A-Za-z0-9-]*$+`, per the spec). Detects top-level (column-0)
+signatures only, which gives the export-only filter for free; tolerant
+of multi-line `+using+` lists; self-skips when no `+Smoke.agda+` is in
+scope.
+* `+unused-import+` (warn): re-emits the findings of the external
+`+agda-unused+` tool (spec §Linter rules). Opt-in behind
+`+scan --unused+`; runs `+agda-unused+` per file in local mode with
+`+LC_ALL=C.UTF-8+`, parses its `+--json+` output, and re-emits each
+finding as an `+unused-import+` warning attributed to the file. Degrades
+gracefully (with a note) when `+agda-unused+` is not on `+PATH+`,
+mirroring how `+check+` tolerates a missing `+agda+`.
+* `+.arghda/config.toml+` operator configuration (the spec’s
+open-question surface): `+scan+` / `+dag+` read a
+`+[lint] headline_pattern+` override from `+<PATH>/.arghda/config.toml+`
+(or an explicit `+--config <file>+`). Precedence is built-in default <
+`+config.toml+` < CLI `+--headline-pattern+`. Missing file ⇒ defaults;
+unknown keys are rejected so typos surface.
+* DAG `+headlines+` field: each `+dag+` node now carries the sorted,
+deduped list of top-level headline theorem names it declares (the spec’s
+per-node `+headlines+` array), extracted with the same logic as
+`+unpinned-headline+` and honouring the configured headline pattern.
+Completes the v0 DAG schema.
+* RSR scaffolding: `+.machine_readable/6a2/+` artefacts,
+`+0-AI-MANIFEST.a2ml+`, `+Justfile+`, `+.well-known/+`, and
+community-health files.
+* Content-hash invalidation of `+proven+`: promotion records a SHA-256
+of the file in `+.arghda/hashes.json+`; the `+stale+` command reports
+proven files edited since promotion, and `+stale --invalidate+` moves
+them back to inbox (the `+proven -> inbox+` invalidation).
+Dependency-free SHA-256, pinned against the NIST test vectors.
+
+==== Notes
+
+* Verified against Agda 2.6.3 and dogfooded on the echo-types corpus
+(193 modules, 903 import edges; the known `+VarianceGate.agda+` orphan
+and the out-of-cone files are surfaced correctly).
+
+=== [0.1.0] — 2026-05-30
+
+* Initial extraction from echo-types: workspace scaffold, filesystem
+watcher, `+missing-safe-pragma+` + `+orphan-module+` lints, and the
+`+scan+` CLI.
diff --git a/CHANGELOG.md b/CHANGELOG.md
deleted file mode 100644
index 818ba11..0000000
--- a/CHANGELOG.md
+++ /dev/null
@@ -1,85 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-# Changelog
-
-All notable changes to arghda-core are documented here. The format follows
-[Keep a Changelog](https://keepachangelog.com/), and this project adheres to
-[Semantic Versioning](https://semver.org/).
-
-## [Unreleased]
-
-### Changed
-
-- Standards / RSR alignment and root cleanup: `README.md` → `README.adoc`
-  (adoc-first; refreshed to the feature-complete v0.1 status), no duplicate
-  doc formats. Added `EXPLAINME.adoc` (orientation pointer), `LICENSE` (full
-  MPL-2.0 text), and `CODE_OF_CONDUCT.md` (Contributor Covenant 2.1). Prose
-  docs carry `CC-BY-SA-4.0`; code/config/state stay `MPL-2.0` (per the estate
-  licence policy). Refreshed `.machine_readable/6a2/STATE.a2ml` + `META.a2ml`
-  and the `0-AI-MANIFEST.a2ml` read-order; removed local `dist-newstyle/`
-  build cruft.
-- Formal SPDX licence invariant (owner-directed): every tracked file carries
-  the correct header — `MPL-2.0` for code/config/scripts/state, `CC-BY-SA-4.0`
-  for prose — applied per file (incl. all `src/*.rs`) and enforced by
-  `scripts/check-spdx.sh`, wired into `just check` and Rust CI. Third-party,
-  generated (`Cargo.lock`), and test-data (`tests/fixtures/`) files are
-  explicitly excluded and never relicensed; `docs/*.adoc` normalised from
-  `CC-BY-4.0` to `CC-BY-SA-4.0`. Declared in
-  `.machine_readable/licensing-policy.toml`.
-
-### Added
-
-- `dag` command emitting the dependency-DAG JSON contract (nodes with
-  lint-derived status, import edges, and a `blocked` list covering
-  self-blocks and prerequisite-blocks).
-- `check` command: Agda typecheck fused with the lint report
-  (`proven-eligible` / `rejected` / `agda-unavailable`); degrades gracefully
-  when `agda` is absent.
-- Workspace state machine — `claim` / `promote` / `reject` / `requeue` /
-  `invalidate` as validated file moves, each logged to
-  `.arghda/events.jsonl`; plus `events` to replay the log.
-- First-class import graph (`graph` module) with multi-root reachability:
-  orphan detection is the union of auto-discovered `All.agda` / `Smoke.agda`
-  CI roots (or `--entry`, repeatable).
-- Lint rules: `unjustified-postulate` (hard-block), `escape-hatch` (warn:
-  `TERMINATING`-family pragmas + `believe_me` / `primTrustMe`), `tab-mix`
-  (warn).
-- `unpinned-headline` (warn): flags a top-level theorem whose name matches
-  the headline pattern but is not pinned in any `Smoke.agda` via a
-  `using ( … )` clause. The pattern is operator-configurable via
-  `--headline-pattern <regex>` on `scan` / `dag` (default
-  `^[a-z][A-Za-z0-9-]*$`, per the spec). Detects top-level (column-0)
-  signatures only, which gives the export-only filter for free; tolerant of
-  multi-line `using` lists; self-skips when no `Smoke.agda` is in scope.
-- `unused-import` (warn): re-emits the findings of the external `agda-unused`
-  tool (spec §Linter rules). Opt-in behind `scan --unused`; runs `agda-unused`
-  per file in local mode with `LC_ALL=C.UTF-8`, parses its `--json` output,
-  and re-emits each finding as an `unused-import` warning attributed to the
-  file. Degrades gracefully (with a note) when `agda-unused` is not on `PATH`,
-  mirroring how `check` tolerates a missing `agda`.
-- `.arghda/config.toml` operator configuration (the spec's open-question
-  surface): `scan` / `dag` read a `[lint] headline_pattern` override from
-  `<PATH>/.arghda/config.toml` (or an explicit `--config <file>`). Precedence
-  is built-in default < `config.toml` < CLI `--headline-pattern`. Missing file
-  ⇒ defaults; unknown keys are rejected so typos surface.
-- DAG `headlines` field: each `dag` node now carries the sorted, deduped list
-  of top-level headline theorem names it declares (the spec's per-node
-  `headlines` array), extracted with the same logic as `unpinned-headline` and
-  honouring the configured headline pattern. Completes the v0 DAG schema.
-- RSR scaffolding: `.machine_readable/6a2/` artefacts, `0-AI-MANIFEST.a2ml`,
-  `Justfile`, `.well-known/`, and community-health files.
-- Content-hash invalidation of `proven`: promotion records a SHA-256 of the
-  file in `.arghda/hashes.json`; the `stale` command reports proven files
-  edited since promotion, and `stale --invalidate` moves them back to inbox
-  (the `proven -> inbox` invalidation). Dependency-free SHA-256, pinned
-  against the NIST test vectors.
-
-### Notes
-
-- Verified against Agda 2.6.3 and dogfooded on the echo-types corpus
-  (193 modules, 903 import edges; the known `VarianceGate.agda` orphan and
-  the out-of-cone files are surfaced correctly).
-
-## [0.1.0] — 2026-05-30
-
-- Initial extraction from echo-types: workspace scaffold, filesystem
-  watcher, `missing-safe-pragma` + `orphan-module` lints, and the `scan` CLI.
diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc
new file mode 100644
index 0000000..a672ecc
--- /dev/null
+++ b/CODE_OF_CONDUCT.adoc
@@ -0,0 +1,8 @@
+== Code of Conduct
+
+This project follows the
+https://www.contributor-covenant.org/version/2/1/code_of_conduct/[Contributor
+Covenant 2.1].
+
+Reports go to `+j.d.a.jewell@open.ac.uk+`. Reports are confidential by
+default.
diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
deleted file mode 100644
index 999b538..0000000
--- a/CODE_OF_CONDUCT.md
+++ /dev/null
@@ -1,7 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
-# Code of Conduct
-
-This project follows the [Contributor Covenant 2.1](https://www.contributor-covenant.org/version/2/1/code_of_conduct/).
-
-Reports go to `j.d.a.jewell@open.ac.uk`. Reports are confidential by default.
diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc
new file mode 100644
index 0000000..03c0630
--- /dev/null
+++ b/CONTRIBUTING.adoc
@@ -0,0 +1,34 @@
+== Contributing to arghda-core
+
+arghda-core is the Rust engine for the arghda proof-workspace tool.
+
+=== Ground rules
+
+* *arghda never proves.* Agda (directly, or via echidna) proves; arghda
+organises, lints, and emits the DAG / event JSON. Don’t add a prover or
+claim a result Agda didn’t return.
+* *Licence:* MPL-2.0. New files carry an SPDX header from birth. Don’t
+bulk-rewrite existing headers.
+* *Green gate.* Every change keeps `+just check+` (`+cargo fmt --check+`
++ `+clippy -D warnings+` + `+build+` + `+test+`) green, and adds tests
+for new behaviour.
+
+=== Workflow
+
+[arabic]
+. Branch from `+main+`.
+. Make the change; `+just check+` must pass.
+. Open a PR. CI runs build / test / clippy / fmt.
+
+=== Layout
+
+* `+src/+` — the library plus the thin `+arghda+` CLI (`+src/main.rs+`).
+* `+src/lint/+` — one module per lint rule (`+LintRule+` trait is the
+extension point).
+* `+src/graph.rs+` — the first-class Agda import graph.
+* `+tests/+` — integration tests; `+tests/fixtures/+` — tiny Agda
+fixtures.
+* `+docs/+` — `+.adoc+` spec (`+arghda-spec.adoc+`) and vision/roadmap
+(`+arghda-vision.adoc+`).
+* `+.machine_readable/6a2/+` — RSR machine-readable state; update
+`+STATE.a2ml+` as work lands.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
deleted file mode 100644
index 8ad261f..0000000
--- a/CONTRIBUTING.md
+++ /dev/null
@@ -1,33 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-# Contributing to arghda-core
-
-arghda-core is the Rust engine for the arghda proof-workspace tool.
-
-## Ground rules
-
-- **arghda never proves.** Agda (directly, or via echidna) proves; arghda
-  organises, lints, and emits the DAG / event JSON. Don't add a prover or
-  claim a result Agda didn't return.
-- **Licence:** MPL-2.0. New files carry an SPDX header from birth. Don't
-  bulk-rewrite existing headers.
-- **Green gate.** Every change keeps `just check`
-  (`cargo fmt --check` + `clippy -D warnings` + `build` + `test`) green,
-  and adds tests for new behaviour.
-
-## Workflow
-
-1. Branch from `main`.
-2. Make the change; `just check` must pass.
-3. Open a PR. CI runs build / test / clippy / fmt.
-
-## Layout
-
-- `src/` — the library plus the thin `arghda` CLI (`src/main.rs`).
-- `src/lint/` — one module per lint rule (`LintRule` trait is the
-  extension point).
-- `src/graph.rs` — the first-class Agda import graph.
-- `tests/` — integration tests; `tests/fixtures/` — tiny Agda fixtures.
-- `docs/` — `.adoc` spec (`arghda-spec.adoc`) and vision/roadmap
-  (`arghda-vision.adoc`).
-- `.machine_readable/6a2/` — RSR machine-readable state; update
-  `STATE.a2ml` as work lands.
diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc
new file mode 100644
index 0000000..9b836fb
--- /dev/null
+++ b/GOVERNANCE.adoc
@@ -0,0 +1,60 @@
+== Governance
+
+=== Overview
+
+This project is governed by the following principles and structures to
+ensure transparent, inclusive, and effective decision-making.
+
+=== Roles and Responsibilities
+
+==== Maintainers
+
+Maintainers are responsible for: - Reviewing and merging pull requests -
+Managing releases and versioning - Ensuring code quality and standards -
+Triaging issues and bug reports - Community engagement and support
+
+==== Contributors
+
+Contributors are expected to: - Follow the code of conduct - Submit
+well-documented pull requests - Write tests for new functionality -
+Maintain existing tests - Update documentation as needed
+
+=== Decision Making
+
+==== Minor Changes
+
+* Can be made by any maintainer
+* Include bug fixes, documentation updates, dependency updates
+
+==== Major Changes
+
+* Require discussion in issues or pull requests
+* Include new features, architectural changes, API changes
+* Need approval from at least 2 maintainers
+
+==== Breaking Changes
+
+* Require RFC (Request for Comments) process
+* Need approval from majority of maintainers
+* Must include migration guide
+
+=== Code of Conduct
+
+All participants are expected to follow our Code of Conduct. Violations
+can be reported to the maintainers.
+
+=== Communication
+
+* *Issues*: For bug reports and feature requests
+* *Discussions*: For questions and general discussion
+* *Pull Requests*: For code contributions
+
+=== Licensing
+
+All contributions are made under the terms of the repository’s LICENSE
+file. By submitting a pull request, you agree to license your
+contributions accordingly.
+
+'''''
+
+_Last updated: 2026-07-18_
diff --git a/GOVERNANCE.md b/GOVERNANCE.md
deleted file mode 100644
index e27364c..0000000
--- a/GOVERNANCE.md
+++ /dev/null
@@ -1,60 +0,0 @@
-# Governance
-
-## Overview
-
-This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making.
-
-## Roles and Responsibilities
-
-### Maintainers
-
-Maintainers are responsible for:
-- Reviewing and merging pull requests
-- Managing releases and versioning
-- Ensuring code quality and standards
-- Triaging issues and bug reports
-- Community engagement and support
-
-### Contributors
-
-Contributors are expected to:
-- Follow the code of conduct
-- Submit well-documented pull requests
-- Write tests for new functionality
-- Maintain existing tests
-- Update documentation as needed
-
-## Decision Making
-
-### Minor Changes
-- Can be made by any maintainer
-- Include bug fixes, documentation updates, dependency updates
-
-### Major Changes
-- Require discussion in issues or pull requests
-- Include new features, architectural changes, API changes
-- Need approval from at least 2 maintainers
-
-### Breaking Changes
-- Require RFC (Request for Comments) process
-- Need approval from majority of maintainers
-- Must include migration guide
-
-## Code of Conduct
-
-All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers.
-
-## Communication
-
-- **Issues**: For bug reports and feature requests
-- **Discussions**: For questions and general discussion
-- **Pull Requests**: For code contributions
-
-## Licensing
-
-All contributions are made under the terms of the repository's LICENSE file.
-By submitting a pull request, you agree to license your contributions accordingly.
-
----
-
-*Last updated: 2026-07-18*
diff --git a/README.adoc b/README.adoc
new file mode 100644
index 0000000..2ad5aa4
--- /dev/null
+++ b/README.adoc
@@ -0,0 +1,166 @@
+https://github.com/sponsors/hyperpolymath[image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor]]
+https://www.mozilla.org/MPL/2.0/[image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License]]
+
+Lightweight proof-workspace manager for Agda — the language-agnostic
+engine half of *arghda*. Extracted from
+https://github.com/hyperpolymath/echo-types[`+hyperpolymath/echo-types+`]
+to its own repository on 2026-05-30 (see echo-types#159 for the move
+record).
+
+arghda-core organises, lints, and reports on an Agda proof workspace; it
+*never proves anything itself* — Agda does. It manages a four-state
+triage workspace (inbox → working → proven → rejected) as file moves,
+runs a lint pack targeting the _silent-failure_ class (cases where Agda
+appears to succeed but the file is not actually in the verified suite),
+builds a first-class import-graph DAG, and emits a JSON + event-stream
+contract a visual layer consumes.
+
+== Status
+
+v0.1 is feature-complete against `+docs/arghda-spec.adoc+`: all seven v0
+Agda lint rules, the four-state workspace state machine, the
+import-graph `+dag+`, the `+check+` command (Agda typecheck + lint
+verdict), content-hash invalidation of `+proven+`, and
+`+.arghda/config.toml+` operator configuration. The live status of
+record is link:.machine_readable/6a2/STATE.a2ml[`+STATE.a2ml+`].
+
+== Lint rules
+
+Hard-block (forbids the `+working+` `+→+` `+proven+` transition):
+
+* `+missing-safe-pragma+` — file lacks `+{-#+` `+OPTIONS+` `+--safe+`
+`+--without-K+` `+#-}+`.
+* `+orphan-module+` — `+.agda+` file unreachable from any CI root (roots
+are auto-discovered as `+All.agda+`/`+Smoke.agda+`, or passed via
+`+--entry+`; reachability is the _union_, so a module verified from any
+root is not an orphan).
+* `+unjustified-postulate+` — `+postulate+` without an adjacent `+--+`
+`+JUSTIFY:+` comment.
+
+Warn (surfaced, non-blocking):
+
+* `+escape-hatch+` — termination overrides (`+TERMINATING+`,
+`+NON_TERMINATING+`, `+NO_TERMINATION_CHECK+`) and trust primitives
+(`+believe_me+`/`+primTrustMe+`).
+* `+tab-mix+` — a tab in leading whitespace.
+* `+unpinned-headline+` — a top-level theorem whose name matches the
+headline pattern is not pinned in any `+Smoke.agda+` via a `+using+`
+`+(+` `+…+` `+)+` clause (the estate "`every headline pinned in Smoke`"
+discipline). The pattern is operator-configurable; its default
+`+^[a-z][A-Za-z0-9-]*$+` is deliberately broad, so operators narrow it
+to their own convention. Self-skips when no `+Smoke.agda+` is in scope.
+* `+unused-import+` — re-emits the findings of the external
+https://github.com/msuperdock/agda-unused[`+agda-unused+`] tool. Opt-in
+behind `+scan+` `+--unused+`; invoked per file in local mode with
+`+LC_ALL=C.UTF-8+`; skipped with a note if the binary is not on
+`+PATH+`.
+
+== Commands
+
+The CLI is `+arghda+`.
+
+[width="100%",cols="50%,50%",options="header",]
+|===
+|Command |What it does
+|`+init+` |Create the four-state workspace layout at a path.
+
+|`+scan+` |Lint every `+.agda+` file under a path. `+--unused+` adds the
+agda-unused pass; `+--config+`/`+--headline-pattern+` tune
+configuration.
+
+|`+check+` |Run Agda on one file and lint it; combined verdict (degrades
+when `+agda+` is absent).
+
+|`+dag+` |Emit the dependency-DAG JSON — nodes (lint status + declared
+`+headlines+`), import edges, and a blocked list.
+
+|`+claim+` / `+promote+` / `+reject+` / `+requeue+` / `+invalidate+`
+|State-machine transitions; each is a file move logged to
+`+.arghda/events.jsonl+`.
+
+|`+events+` |Replay the workspace event log.
+
+|`+stale+` |List `+proven+` files whose content changed since promotion;
+`+--invalidate+` returns them to inbox.
+
+|`+watch+` |Watch `+inbox/+` and `+working/+` and print events.
+|===
+
+== Configuration
+
+`+scan+` and `+dag+` read `+.arghda/config.toml+` (from
+`+<PATH>/.arghda/config.toml+`, or an explicit `+--config+` `+<file>+`).
+Precedence is built-in default < `+config.toml+` < CLI flag.
+
+[source,toml]
+----
+[lint]
+headline_pattern = "^[a-z][A-Za-z0-9-]*$"
+----
+
+== Build
+
+[source,sh]
+----
+just check    # fmt-check + clippy (-D warnings) + build + test — the CI gate
+cargo build
+cargo test
+----
+
+`+agda+` and `+agda-unused+` are optional: the `+check+` and `+scan+`
+`+--unused+` paths degrade gracefully (with a note) when the binary is
+absent, so the rest of the engine still works in an Agda-less
+environment.
+
+== Smoke against an Agda workspace
+
+[source,sh]
+----
+cargo run -- scan path/to/your/agda/sources
+----
+
+Dogfooded against the echo-types corpus (193 modules): `+dag+` emits the
+903-edge import graph; multi-root discovery (`+All.agda+`,
+`+Smoke.agda+`, `+Ordinal/Buchholz/Smoke.agda+`,
+`+characteristic/All.agda+`, `+examples/All.agda+`) narrows orphan
+reports from 38 to the 17 genuine orphans.
+
+== Ecosystem
+
+Part of the https://github.com/hyperpolymath[hyperpolymath ecosystem].
+arghda splits into `+arghda-core+` (this engine) and the planned
+`+arghda-studio+` / `+arghda-panll+` visual layers, which consume the
+`+dag+` JSON + `+events.jsonl+` contract. The motivating workspace was
+the echo-types proof pipeline, but arghda-core has no
+echo-types-specific code.
+
+Adjacent projects:
+
+* https://github.com/hyperpolymath/echo-types[echo-types] — the Agda
+library that motivated arghda’s design (not a build dependency).
+* https://github.com/hyperpolymath/absolute-zero[absolute-zero] — a
+sister Agda library under the same `+--safe+` `+--without-K+`
+discipline.
+
+== Machine-readable
+
+Per the Rhodium Standard, structured project metadata lives under
+link:.machine_readable/6a2/[`+.machine_readable/6a2/+`] — `+STATE+`,
+`+META+`, `+ECOSYSTEM+`, `+AGENTIC+`, `+NEUROSYM+`, `+PLAYBOOK+` in A2ML
+— with link:0-AI-MANIFEST.a2ml[`+0-AI-MANIFEST.a2ml+`] as the AI entry
+point and link:EXPLAINME.adoc[`+EXPLAINME.adoc+`] as the orientation
+pointer.
+
+== Licence
+
+Code, configuration and scripts are `+MPL-2.0+` (see LICENSE); prose
+documentation is `+CC-BY-SA-4.0+`, per the
+https://github.com/hyperpolymath/standards[hyperpolymath licence policy]
+(Rule 1). This split is a *formal invariant*: every tracked file carries
+the appropriate SPDX header, checked by `+scripts/check-spdx.sh+` in
+`+just+` `+check+` and in CI. Third-party, generated, and test-data
+files are explicitly excluded
+(link:.machine_readable/licensing-policy.toml[`+licensing-policy.toml+`])
+and are never relicensed — vendoring third-party source in-tree fails
+the check until it is listed as excluded with its original SPDX
+preserved.
diff --git a/README.md b/README.md
deleted file mode 100644
index bf770c2..0000000
--- a/README.md
+++ /dev/null
@@ -1,152 +0,0 @@
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
-
-[![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath)
-[![License](https://img.shields.io/badge/License-MPL_2.0-blue.svg)](https://www.mozilla.org/MPL/2.0/)
-
-Lightweight proof-workspace manager for Agda — the language-agnostic
-engine half of **arghda**. Extracted from
-[`hyperpolymath/echo-types`](https://github.com/hyperpolymath/echo-types)
-to its own repository on 2026-05-30 (see echo-types#159 for the move
-record).
-
-arghda-core organises, lints, and reports on an Agda proof workspace; it
-**never proves anything itself** — Agda does. It manages a four-state
-triage workspace (inbox → working → proven → rejected) as file moves,
-runs a lint pack targeting the *silent-failure* class (cases where Agda
-appears to succeed but the file is not actually in the verified suite),
-builds a first-class import-graph DAG, and emits a JSON + event-stream
-contract a visual layer consumes.
-
-# Status
-
-v0.1 is feature-complete against `docs/arghda-spec.adoc`: all seven v0
-Agda lint rules, the four-state workspace state machine, the
-import-graph `dag`, the `check` command (Agda typecheck + lint verdict),
-content-hash invalidation of `proven`, and `.arghda/config.toml`
-operator configuration. The live status of record is
-[`STATE.a2ml`](.machine_readable/6a2/STATE.a2ml).
-
-# Lint rules
-
-Hard-block (forbids the `working` `→` `proven` transition):
-
-- `missing-safe-pragma` — file lacks `{-#` `OPTIONS` `--safe`
-  `--without-K` `#-}`.
-
-- `orphan-module` — `.agda` file unreachable from any CI root (roots are
-  auto-discovered as `All.agda`/`Smoke.agda`, or passed via `--entry`;
-  reachability is the *union*, so a module verified from any root is not
-  an orphan).
-
-- `unjustified-postulate` — `postulate` without an adjacent `--`
-  `JUSTIFY:` comment.
-
-Warn (surfaced, non-blocking):
-
-- `escape-hatch` — termination overrides (`TERMINATING`,
-  `NON_TERMINATING`, `NO_TERMINATION_CHECK`) and trust primitives
-  (`believe_me`/`primTrustMe`).
-
-- `tab-mix` — a tab in leading whitespace.
-
-- `unpinned-headline` — a top-level theorem whose name matches the
-  headline pattern is not pinned in any `Smoke.agda` via a `using` `(`
-  `…` `)` clause (the estate "every headline pinned in Smoke"
-  discipline). The pattern is operator-configurable; its default
-  `^[a-z][A-Za-z0-9-]*$` is deliberately broad, so operators narrow it
-  to their own convention. Self-skips when no `Smoke.agda` is in scope.
-
-- `unused-import` — re-emits the findings of the external
-  [`agda-unused`](https://github.com/msuperdock/agda-unused) tool.
-  Opt-in behind `scan` `--unused`; invoked per file in local mode with
-  `LC_ALL=C.UTF-8`; skipped with a note if the binary is not on `PATH`.
-
-# Commands
-
-The CLI is `arghda`.
-
-| Command | What it does |
-|----|----|
-| `init` | Create the four-state workspace layout at a path. |
-| `scan` | Lint every `.agda` file under a path. `--unused` adds the agda-unused pass; `--config`/`--headline-pattern` tune configuration. |
-| `check` | Run Agda on one file and lint it; combined verdict (degrades when `agda` is absent). |
-| `dag` | Emit the dependency-DAG JSON — nodes (lint status + declared `headlines`), import edges, and a blocked list. |
-| `claim` / `promote` / `reject` / `requeue` / `invalidate` | State-machine transitions; each is a file move logged to `.arghda/events.jsonl`. |
-| `events` | Replay the workspace event log. |
-| `stale` | List `proven` files whose content changed since promotion; `--invalidate` returns them to inbox. |
-| `watch` | Watch `inbox/` and `working/` and print events. |
-
-# Configuration
-
-`scan` and `dag` read `.arghda/config.toml` (from
-`<PATH>/.arghda/config.toml`, or an explicit `--config` `<file>`).
-Precedence is built-in default \< `config.toml` \< CLI flag.
-
-```toml
-[lint]
-headline_pattern = "^[a-z][A-Za-z0-9-]*$"
-```
-
-# Build
-
-```sh
-just check    # fmt-check + clippy (-D warnings) + build + test — the CI gate
-cargo build
-cargo test
-```
-
-`agda` and `agda-unused` are optional: the `check` and `scan` `--unused`
-paths degrade gracefully (with a note) when the binary is absent, so the
-rest of the engine still works in an Agda-less environment.
-
-# Smoke against an Agda workspace
-
-```sh
-cargo run -- scan path/to/your/agda/sources
-```
-
-Dogfooded against the echo-types corpus (193 modules): `dag` emits the
-903-edge import graph; multi-root discovery (`All.agda`, `Smoke.agda`,
-`Ordinal/Buchholz/Smoke.agda`, `characteristic/All.agda`,
-`examples/All.agda`) narrows orphan reports from 38 to the 17 genuine
-orphans.
-
-# Ecosystem
-
-Part of the [hyperpolymath ecosystem](https://github.com/hyperpolymath).
-arghda splits into `arghda-core` (this engine) and the planned
-`arghda-studio` / `arghda-panll` visual layers, which consume the `dag`
-JSON + `events.jsonl` contract. The motivating workspace was the
-echo-types proof pipeline, but arghda-core has no echo-types-specific
-code.
-
-Adjacent projects:
-
-- [echo-types](https://github.com/hyperpolymath/echo-types) — the Agda
-  library that motivated arghda’s design (not a build dependency).
-
-- [absolute-zero](https://github.com/hyperpolymath/absolute-zero) — a
-  sister Agda library under the same `--safe` `--without-K` discipline.
-
-# Machine-readable
-
-Per the Rhodium Standard, structured project metadata lives under
-[`.machine_readable/6a2/`](.machine_readable/6a2/) — `STATE`, `META`,
-`ECOSYSTEM`, `AGENTIC`, `NEUROSYM`, `PLAYBOOK` in A2ML — with
-[`0-AI-MANIFEST.a2ml`](0-AI-MANIFEST.a2ml) as the AI entry point and
-[`EXPLAINME.adoc`](EXPLAINME.adoc) as the orientation pointer.
-
-# Licence
-
-Code, configuration and scripts are `MPL-2.0` (see [LICENSE](LICENSE));
-prose documentation is `CC-BY-SA-4.0`, per the [hyperpolymath licence
-policy](https://github.com/hyperpolymath/standards) (Rule 1). This split
-is a **formal invariant**: every tracked file carries the appropriate
-SPDX header, checked by `scripts/check-spdx.sh` in `just` `check` and in
-CI. Third-party, generated, and test-data files are explicitly excluded
-([`licensing-policy.toml`](.machine_readable/licensing-policy.toml)) and
-are never relicensed — vendoring third-party source in-tree fails the
-check until it is listed as excluded with its original SPDX preserved.
diff --git a/SECURITY.adoc b/SECURITY.adoc
new file mode 100644
index 0000000..cd052a7
--- /dev/null
+++ b/SECURITY.adoc
@@ -0,0 +1,31 @@
+== Security Policy
+
+=== Supported versions
+
+arghda-core is alpha (0.1.x). Only the latest `+main+` is supported.
+
+=== Reporting a vulnerability
+
+Please report suspected security issues *privately* to
+*j.d.a.jewell@open.ac.uk*. Do not open a public issue for a suspected
+vulnerability.
+
+Where possible, include:
+
+* a description of the issue and its impact;
+* steps or a proof-of-concept to reproduce;
+* the commit or version affected.
+
+=== Response
+
+We aim to acknowledge a report within 7 days and to agree a disclosure
+timeline with the reporter.
+
+=== Scope
+
+This policy covers the arghda-core engine. arghda reads `+.agda+` files
+as text and shells out to the configured `+agda+` (and, in future,
+`+agda-unused+`) binary on files you point it at; it never executes
+proof code itself. Reports about untrusted-input handling — path
+traversal, command construction, denial of service on malformed input —
+are especially welcome.
diff --git a/SECURITY.md b/SECURITY.md
deleted file mode 100644
index 9aa8ee8..0000000
--- a/SECURITY.md
+++ /dev/null
@@ -1,32 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-# Security Policy
-
-## Supported versions
-
-arghda-core is alpha (0.1.x). Only the latest `main` is supported.
-
-## Reporting a vulnerability
-
-Please report suspected security issues **privately** to
-**j.d.a.jewell@open.ac.uk**. Do not open a public issue for a suspected
-vulnerability.
-
-Where possible, include:
-
-- a description of the issue and its impact;
-- steps or a proof-of-concept to reproduce;
-- the commit or version affected.
-
-## Response
-
-We aim to acknowledge a report within 7 days and to agree a disclosure
-timeline with the reporter.
-
-## Scope
-
-This policy covers the arghda-core engine. arghda reads `.agda` files as
-text and shells out to the configured `agda` (and, in future,
-`agda-unused`) binary on files you point it at; it never executes proof
-code itself. Reports about untrusted-input handling — path traversal,
-command construction, denial of service on malformed input — are
-especially welcome.
diff --git a/docs/arghda-spec.adoc b/docs/arghda-spec.adoc
index dc21728..21df649 100644
--- a/docs/arghda-spec.adoc
+++ b/docs/arghda-spec.adoc
@@ -47,7 +47,7 @@ CLI, a library API, and a JSON event stream. Runs in CI, standalone,
 or embedded.
 
 `arghda-panll`:: PanLL presentation layer. Gossamer webview +
-ReScript panel consuming `arghda-core`'s event stream. Lives in the
+AffineScript panel consuming `arghda-core`'s event stream. Lives in the
 PanLL surface, probably adjacent to Pane-W.
 
 Rationale for the split: