Date the FRG assessment and clarify the Me projection boundary

.claude/CLAUDE.md

@@ -3,15 +3,15 @@
 
 ## Machine-Readable Artefacts
 
-The following files in `.machine_readable/6a2/` contain structured project
+The following files in `.machine_readable/descriptiles/` contain structured project
 metadata (a2ml format; the earlier `.scm` root-level names are retired):
 
-- `6a2/STATE.a2ml` - Current project state and progress
-- `6a2/META.a2ml` - Architecture decisions (ADRs) and development practices
-- `6a2/ECOSYSTEM.a2ml` - Position in the ecosystem and related projects
-- `6a2/AGENTIC.a2ml` - AI agent interaction patterns
-- `6a2/NEUROSYM.a2ml` - Neurosymbolic integration config
-- `6a2/PLAYBOOK.a2ml` - Operational runbook
+- `descriptiles/STATE.a2ml` - Current project state and progress
+- `descriptiles/META.a2ml` - Architecture decisions (ADRs) and development practices
+- `descriptiles/ECOSYSTEM.a2ml` - Position in the ecosystem and related projects
+- `descriptiles/AGENTIC.a2ml` - AI agent interaction patterns
+- `descriptiles/NEUROSYM.a2ml` - Neurosymbolic integration config
+- `descriptiles/PLAYBOOK.a2ml` - Operational runbook
 
 Self-validation / service metadata lives in `.machine_readable/svc/`
 (`svc/k9/my-lang-metadata.k9.ncl`, `svc/README.adoc`). The scope-arrest anchor
@@ -36,7 +36,7 @@ is the top-level `ANCHOR.scope-arrest.2026-01-01.Jewell.scm`.
 | **Bash/POSIX Shell** | Scripts, automation | Keep minimal |
 | **JavaScript** | Only where AffineScript cannot | MCP protocol glue, Bun APIs |
 | **Nickel** | Configuration language | For complex configs |
-| **Guile Scheme** | State/meta files | `.machine_readable/6a2/{STATE,META,ECOSYSTEM}.a2ml` (the earlier `.scm` names are retired) |
+| **Guile Scheme** | State/meta files | `.machine_readable/descriptiles/{STATE,META,ECOSYSTEM}.a2ml` (the earlier `.scm` names are retired) |
 | **Julia** | Batch scripts, data processing | Per RSR |
 | **OCaml** | AffineScript compiler | Language-specific |
 | **Ada** | Safety-critical systems | Where required |

.github/workflows/hypatia-scan.yml

@@ -20,4 +20,6 @@ permissions:
 
 jobs:
   scan:
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@469605210e767ee94d1c7a9c13cb6a1d0a78cad1
+    with:
+      block-on-high: true

.github/workflows/label-triage.yml

@@ -46,6 +46,7 @@ permissions:
 jobs:
   triage:
     runs-on: ubuntu-latest
+    timeout-minutes: 5
     steps:
       - name: Classify and label
         env:

.github/workflows/labels.yml

@@ -32,6 +32,7 @@ permissions:
 jobs:
   sync:
     runs-on: ubuntu-latest
+    timeout-minutes: 5
     steps:
       - name: Apply canonical labels
         env:

.github/workflows/pages.yml

@@ -1,5 +1,5 @@
-# SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
+# SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 name: GitHub Pages (Ddraig SSG)
@@ -54,4 +54,4 @@ jobs:
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@368f82528645a54fb793d4d04e342629a3f51346 # v5
+        uses: actions/deploy-pages@368f82528645a54fb793d4d04e342629a3f51346

.machine_readable/contractiles/Adjustfile.a2ml

@@ -40,7 +40,7 @@ actions. Advisory — it warns and trends, it does not block.
 - severity: advisory
 
 ### status-doc-currency
-- description: proofs/STATUS.md + 6a2/STATE.a2ml reflect the actual proof state
+- description: proofs/STATUS.md + descriptiles/STATE.a2ml reflect the actual proof state
 - tolerance: Status registry matches the mechanised cores
 - corrective: Refresh STATUS.md / STATE.a2ml after any proof rung lands
 - severity: advisory

.machine_readable/contractiles/Mustfile.a2ml

@@ -33,8 +33,8 @@ pre-commit hooks fail if any check fails. my-lang is a CONSUMER of the RSR
 - severity: critical
 
 ### ai-manifest
-- description: 0-AI-MANIFEST.a2ml must exist (under 6a2/)
-- run: test -f .machine_readable/6a2/0-AI-MANIFEST.a2ml
+- description: 0-AI-MANIFEST.a2ml must exist (under descriptiles/)
+- run: test -f .machine_readable/descriptiles/0-AI-MANIFEST.a2ml
 - severity: critical
 
 ### governance-docs
@@ -68,8 +68,8 @@ pre-commit hooks fail if any check fails. my-lang is a CONSUMER of the RSR
 - severity: critical
 
 ### six-directory-present
-- description: 6a2 directory exists with required files
-- run: test -d .machine_readable/6a2 && test -f .machine_readable/6a2/META.a2ml && test -f .machine_readable/6a2/ECOSYSTEM.a2ml && test -f .machine_readable/6a2/STATE.a2ml && test -f .machine_readable/6a2/PLAYBOOK.a2ml && test -f .machine_readable/6a2/AGENTIC.a2ml && test -f .machine_readable/6a2/NEUROSYM.a2ml
+- description: descriptiles directory exists with required files
+- run: test -d .machine_readable/descriptiles && test -f .machine_readable/descriptiles/META.a2ml && test -f .machine_readable/descriptiles/ECOSYSTEM.a2ml && test -f .machine_readable/descriptiles/STATE.a2ml && test -f .machine_readable/descriptiles/PLAYBOOK.a2ml && test -f .machine_readable/descriptiles/AGENTIC.a2ml && test -f .machine_readable/descriptiles/NEUROSYM.a2ml
 - severity: critical
 
 ### scope-arrest-anchor

.machine_readable/contractiles/dust/detach-echo-types-plugin.a2ml

@@ -62,7 +62,7 @@ be a significant architectural change requiring a clear extension boundary.
 ### 5-update-6a2-state
 - description: Update STATE.a2ml to reflect echo-types as plugin, not built-in
 - corrective: >
-    In 6a2/STATE.a2ml: update echo_integration_status from 'built_in' to 'plugin'.
+    In descriptiles/STATE.a2ml: update echo_integration_status from 'built_in' to 'plugin'.
     Add an ADR in META.a2ml documenting the boundary decision.
 
 ## Completion Criteria

.machine_readable/contractiles/dust/uninstall-coq-toolchain.a2ml

@@ -47,7 +47,7 @@ what must be preserved, and what downstream consumers must be informed of.
 ### 5-update-6a2-state
 - description: Update STATE.a2ml and META.a2ml to reflect Coq retirement
 - corrective: >
-    In 6a2/STATE.a2ml: mark coq_core as retired; in 6a2/META.a2ml: remove
+    In descriptiles/STATE.a2ml: mark coq_core as retired; in descriptiles/META.a2ml: remove
     ADR-009 (open-context subst) as Coq-specific or generalise it.
 
 ### 6-notify-downstream

.machine_readable/6a2/0-AI-MANIFEST.a2ml → .machine_readable/descriptiles/0-AI-MANIFEST.a2ml

@@ -1,11 +1,11 @@
 # SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
-# AI Manifest for 6a2 Directory
+# AI Manifest for Descriptiles Directory
 
 ## Purpose
 
-This manifest declares the AI-assistant context for the 6a2 machine-readable metadata directory.
+This manifest declares the AI-assistant context for the descriptiles machine-readable metadata directory.
 
 ## Canonical Locations
 

.machine_readable/6a2/PLAYBOOK.a2ml → .machine_readable/descriptiles/PLAYBOOK.a2ml

@@ -12,7 +12,7 @@ last-updated = "2026-04-11"
 # target = "container"  # container | binary | library | wasm
 
 [incident-response]
-# 1. Check .machine_readable/STATE.a2ml for current status
+# 1. Check .machine_readable/descriptiles/STATE.a2ml for current status
 # 2. Review recent commits and CI results
 # 3. Run `just validate` to check compliance
 # 4. Run `just security` to audit for vulnerabilities

.machine_readable/6a2/README.adoc → .machine_readable/descriptiles/README.adoc

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
-# A2ML 6a2 Directory
+# A2ML Descriptiles Directory
 
 This directory contains the 6 core A2ML machine-readable metadata files for this repository.
 

.machine_readable/6a2/STATE.a2ml → .machine_readable/descriptiles/STATE.a2ml

@@ -162,3 +162,8 @@ ci-pr = "PRs #143/#146/#147 merged 2026-07-27; no open PRs"
 proof-build = "pass — coqc 10/10 solo-core modules (Quantity, EchoMode, ResourceAlgebra, SoloCore, Tropical, Context, ContextProps, EchoResidue, EchoMeasure, SessionPi; local full clean rebuild 2026-06-14); idris2 --build OK; all per-rung Print Assumptions closed (R-ladder, M1, S1.0–S3c.3-msg, E4)"
 known-local-limitation = "my-llvm cannot be built in the maintainer's WSL environment (no system LLVM 21). `cargo build --workspace` FAILS there; `--exclude my-llvm` succeeds. Do not read a bare workspace build failure as a regression without checking for the llvm-sys compile_error."
 superseded-branch = "origin/feat/stdlib-fs-env-format — SUPERSEDED, safe to delete: main carries every builtin it adds PLUS fs_list_dir, its stdlib.rs is 355 lines behind, it conflicts on stdlib.rs + CONTRIBUTING.md, and it is 188 commits behind main"
+
+[language-portfolio-audit-20260907]
+scope = "Evidence audit and scoped repairs; no blanket readiness upgrade"
+report = "https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/audits/2026-09-07-language-portfolio.md"
+metadata-path = ".machine_readable/descriptiles/"

.well-known/security.txt

@@ -0,0 +1,4 @@
+Contact: https://github.com/hyperpolymath/my-lang/security/advisories/new
+Expires: 2027-09-07T00:00:00Z
+Preferred-Languages: en
+Policy: https://github.com/hyperpolymath/my-lang/blob/main/SECURITY.md

CHANGELOG.adoc

@@ -52,7 +52,7 @@ described `+src/+`, `+config/+` and `+scripts/+` directories that do not
 exist) with the real 15-crate workspace layout, the
 `+solo ⊂ duet ⊂ ensemble+` containment hierarchy (with `+me+` as a
 projector outside it), and the CI gate map.
-* docs: `+README.md+` and `+.machine_readable/6a2/STATE.a2ml+` now
+* docs: `+README.md+` and `+.machine_readable/descriptiles/STATE.a2ml+` now
 record the dialects as nested subsets rather than four co-equal
 surfaces, and carry a security-posture section distinguishing expiring
 baseline debt from permanent scoped exemptions.

DEBT.adoc

@@ -11,7 +11,7 @@ duplicating them:
 proof-status registry
 * link:PROOF-NEEDS.md[`+PROOF-NEEDS.md+`] — proof-side cleanup notes
 * link:TESTING.md[`+TESTING.md+`] — per-crate coverage measurements
-* link:.machine_readable/6a2/STATE.a2ml[`+.machine_readable/6a2/STATE.a2ml+`]
+* link:.machine_readable/descriptiles/STATE.a2ml[`+.machine_readable/descriptiles/STATE.a2ml+`]
 — authoritative machine state
 
 Severity: *HIGH* = correctness, licensing or security exposure ·
@@ -140,7 +140,7 @@ licences.
 ==== L-4 — AGPL text committed while policy bans AGPL · MEDIUM
 
 `+LICENSES/AGPL-3.0-or-later.txt+` (34 KB) is present; nothing in the
-tree declares AGPL, and `+.machine_readable/6a2/AGENTIC.a2ml+` states
+tree declares AGPL, and `+.machine_readable/descriptiles/AGENTIC.a2ml+` states
 _"`Never use AGPL licence`"_. Licence scanners will report AGPL for this
 repository. *Next:* delete unless a dependency genuinely requires the
 text.
@@ -478,7 +478,7 @@ reconcile or scope the patterns to new code.
 nearly all commented placeholders; `+AGENTIC.a2ml+` (2026-04-11) is
 comment-only and states _"`Never place state files in repository root`"_
 while four sit at root. Two different `+0-AI-MANIFEST.a2ml+` files exist
-(root = S-expression, `+6a2/+` = Markdown) with contradictory content.
+(root = S-expression, `+descriptiles/+` = Markdown) with contradictory content.
 `+svc/README.adoc+` documents a `+k9/+` directory that does not exist
 (the file lives in `+self-validating/+`). *Next:* fill or delete;
 deduplicate the manifest.

Justfile

@@ -70,7 +70,7 @@ pipeline:
 # Prepare a release
 release VERSION:
     @echo "Releasing {{VERSION}}..."
-    @echo "Set version = \"{{VERSION}}\" in Cargo.toml [workspace.package] and .machine_readable/6a2/STATE.a2ml, then tag."
+    @echo "Set version = \"{{VERSION}}\" in Cargo.toml [workspace.package] and .machine_readable/descriptiles/STATE.a2ml, then tag."
 
 # Run dialect demos (per golden-path contract)
 # Usage: just demo [dialect]
@@ -124,7 +124,7 @@ verify:
     #!/usr/bin/env bash
     set -uo pipefail
     fail=0
-    for p in .machine_readable .machine_readable/6a2/STATE.a2ml \
+    for p in .machine_readable .machine_readable/descriptiles/STATE.a2ml \
              .hypatia-baseline.json .hypatia-ignore \
              proofs/STATUS.md Cargo.toml; do
         if [[ -e "$p" ]]; then echo "[OK]   $p"

README.adoc

@@ -44,7 +44,7 @@ note].
 |`+frontier-practices/+` |Forward-looking research experiments (not
 shipped).
 
-|`+.machine_readable/+` |Machine-facing state. `+6a2/STATE.a2ml+` is the
+|`+.machine_readable/+` |Machine-facing state. `+descriptiles/STATE.a2ml+` is the
 authoritative project-state file for agents; `+contractiles/+` holds the
 Mustfile / Dustfile invariant and recovery contracts.
 
@@ -430,7 +430,7 @@ cannot be satisfied (a keyword-matching `+coq_axiom+`, a
 keyword-matching `+transmute+`, and `+unsafe_block+` — a bare
 `+unsafe\s*\{+` regex whose "`requires SAFETY comment`" is never
 actually checked). See `+[security-posture]+` in
-link:.machine_readable/6a2/STATE.a2ml[`+.machine_readable/6a2/STATE.a2ml+`]
+link:.machine_readable/descriptiles/STATE.a2ml[`+.machine_readable/descriptiles/STATE.a2ml+`]
 for the machine-readable version.
 
 === Contributing

ROADMAP.adoc

@@ -11,7 +11,7 @@ toc::[]
 [NOTE]
 ====
 This roadmap is *derived*, not authoritative. The machine-readable source of
-truth is `.machine_readable/6a2/STATE.a2ml`; for proofs specifically it is
+truth is `.machine_readable/descriptiles/STATE.a2ml`; for proofs specifically it is
 `proofs/STATUS.md`. Where they disagree with this file, they win.
 ====
 

SECURITY.md

@@ -0,0 +1,9 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+# Security policy
+
+Report suspected vulnerabilities privately to the contact listed in
+[security.txt](.well-known/security.txt). Include the affected commit, reproduction
+steps and expected impact. Do not include credentials in public issues or PRs.
+
+This repository contains research and development work; a successful CI run
+does not certify all language designs, proofs or deployment configurations.

docs/proof-debt.md

@@ -0,0 +1,43 @@
+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
+# Proof debt and the trusted boundary
+
+This register distinguishes abstract interface obligations from global axioms.
+It records the published source inspected on 2026-09-07; it does not promote
+unpublished proof work or establish that every language feature is verified.
+
+## (a) Discharged in concrete instances
+
+The 15 `Axiom` declarations in
+`proofs/verification/coq/solo-core/ResourceAlgebra.v` are fields of Coq module
+types: ten `SEMIRING` laws, three additional `ORDERED_SEMIRING` order laws, and
+two `RESIDUE_MEASURE` homomorphism laws. An abstract soundness functor is
+conditional on these fields. A concrete implementation must supply proofs of
+the fields when checked against its module signature.
+
+The source identifies `Linear3`, `Tropical` and `EchoTraceTropical` as concrete
+instances. Their instantiated theorem dependencies, rather than the spelling
+`Axiom` inside a module type, determine the global trusted base. The existing
+`proofs.yml` workflow checks concrete assumption closure. Passing the structural
+trusted-base policy only establishes that these sites are documented; it is
+not a new execution of the Coq checker or a proof of the Rust implementation.
+
+## (b) Budgeted boundaries
+
+No new refutation budget or runtime extraction guarantee is claimed by this
+audit. See `proofs/STATUS.adoc` for the scope of existing checks.
+
+## (c) Necessary global axioms
+
+The interface fields above are not classified as necessary global axioms.
+This review does not certify the dependency closure of every proof in the tree.
+
+## (d) Open obligations
+
+- **Owner:** repository maintainer, @hyperpolymath.
+- **Scope:** the model/implementation correspondence and remaining obligations
+  recorded in `proofs/STATUS.adoc` and `proofs/ALIGNMENT-PLAN.adoc`.
+- **Plan:** keep each theorem tied to its actual language fragment, concrete
+  resource algebra and executable checker; close the correspondence obligations
+  with compiler/proof checks and counterexample tests before expanding claims.
+- **Deadline:** INDEFINITE: these are separate research obligations, not
+  discharged by the documentation and CI repairs in this PR.

docs/wiki/README.md

@@ -105,7 +105,7 @@ integration is one capability among many — not the defining feature.
 ## Project status
 
 - **Version:** `0.2.0` (early-alpha, experimental; no tagged release) — see
-  [`.machine_readable/6a2/STATE.a2ml`](../../.machine_readable/6a2/STATE.a2ml)
+  [`.machine_readable/descriptiles/STATE.a2ml`](../../.machine_readable/descriptiles/STATE.a2ml)
   for the authoritative state, and [`proofs/STATUS.md`](../../proofs/STATUS.md)
   for the proof-status registry.
 - **Scope:** Solo dialect only in `f0` (per the

docs/wiki/internals/formal-verification.md

@@ -107,4 +107,4 @@ and asserts `progress` is axiom-free.
   a typed hole (`?todo_*`) or a bare `Definition : Prop` is an *obligation*, never
   a result.
 - Architecture decisions are recorded as ADRs in
-  [`.machine_readable/6a2/META.a2ml`](../../../.machine_readable/6a2/META.a2ml).
+  [`.machine_readable/descriptiles/META.a2ml`](../../../.machine_readable/descriptiles/META.a2ml).

docs/wiki/roadmap/compiler.md

@@ -4,7 +4,7 @@
 # Compiler Roadmap
 
 > [!WARNING]
-> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/6a2/STATE.a2ml` are authoritative.
+> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/descriptiles/STATE.a2ml` are authoritative.
 
 
 This document outlines the development plan for the My Language compiler infrastructure.

docs/wiki/roadmap/language.md

@@ -4,7 +4,7 @@
 # Language Roadmap
 
 > [!WARNING]
-> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/6a2/STATE.a2ml` are authoritative.
+> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/descriptiles/STATE.a2ml` are authoritative.
 
 
 This document details the evolution of My Language's core features and syntax.

docs/wiki/roadmap/overview.md

@@ -4,7 +4,7 @@
 # My Language Roadmap Overview
 
 > [!WARNING]
-> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/6a2/STATE.a2ml` are authoritative.
+> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/descriptiles/STATE.a2ml` are authoritative.
 
 
 *Last Updated: 2025-12-17*

docs/wiki/roadmap/tooling.md

@@ -4,7 +4,7 @@
 # Tooling Roadmap
 
 > [!WARNING]
-> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/6a2/STATE.a2ml` are authoritative.
+> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/descriptiles/STATE.a2ml` are authoritative.
 
 
 This document outlines the development plan for My Language development tools.

playground/.machine_readable/6a2/PLAYBOOK.a2ml

@@ -12,7 +12,7 @@ last-updated = "2026-04-11"
 # target = "container"  # container | binary | library | wasm
 
 [incident-response]
-# 1. Check .machine_readable/STATE.a2ml for current status
+# 1. Check .machine_readable/descriptiles/STATE.a2ml for current status
 # 2. Review recent commits and CI results
 # 3. Run `just validate` to check compliance
 # 4. Run `just security` to audit for vulnerabilities