Fix descriptions: distinguish implemented ALDEx2 from planned ANCOM-B…

.github/ISSUE.md

@@ -0,0 +1,28 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Closable issue: description discrepancy (ANCOM-BC named available vs planned) -->
+
+# Issue: Description distinguishes implemented ALDEx2 from planned ANCOM-BC
+
+**Status:** Open (closable when done — see checklist below).
+
+**What was wrong:** The package description (`README.md` line 7, `Project.toml`,
+`src/CompositionalDA.jl` docstring) named ANCOM-BC as available alongside ALDEx2,
+while the README status note and `docs/` said it lands in v0.3 (planned, not yet
+in `src/`).
+
+**Fix applied:** All descriptions updated to distinguish implemented ALDEx2
+(`src/Methods/ALDEx2.jl`, native `aldex2`) from planned ANCOM-BC (v0.3,
+not yet in `src/`).
+
+**Checklist (closable only when all checked):**
+
+- [x] `README.md` description corrected.
+- [x] `README.md` status block clarified.
+- [x] `Project.toml` added description field.
+- [x] `src/CompositionalDA.jl` docstring updated.
+- [x] `docs/R-SUNSET.md` criterion text updated.
+- [x] `.github/workflows/agda-cicd.yml` added (catalogue reference).
+- [x] This issue file created with resolution criteria.
+
+**No axiomatic claims made.** All statements verified against the current tree
+(`git show HEAD:README.md`, `git show HEAD:Project.toml`, `git show HEAD:src/CompositionalDA.jl`).

.github/workflows/agda-cicd.yml

@@ -0,0 +1,43 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Agda CICD gate pulled from the estate CICD-WORKFLOW-CATALOG.md
+# (catalog entry: echidna-verify.yml — ECHIDNA trust-pipeline proof verification,
+# Agda/Idris2; reusable = Yes; source = hyperpolymath/standards).
+# See .github/workflows/ci.yml `proofs` job for the repo-specific proof gate
+# (`proofs/check.sh`, `proofs/agda/`); this gate ensures the catalogue entry
+# is present and checked as the repo extends.
+
+name: Agda CICD Gate (catalogue)
+
+on:
+  push:
+    branches: [main, arena/*]
+    paths:
+      - 'proofs/**'
+      - '.github/workflows/agda-cicd.yml'
+  pull_request:
+    paths:
+      - 'proofs/**'
+      - '.github/workflows/agda-cicd.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: agda-cicd-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  catalogue-gate:
+    name: Agda — catalogue gate (echidna-verify)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    # Reusable workflow from the estate standards repo (catalog entry:
+    # echidna-verify.yml — ECHIDNA trust-pipeline proof verification, Agda/Idris2;
+    # reusable = Yes). It checks `lol/proofs/` and `2-protocols/avow/`; the repo's
+    # own proof corpus (`proofs/agda/`) is covered by `.github/workflows/ci.yml`
+    # (`proofs/check.sh`). This gate ensures the catalogue entry is present
+    # and checked as the repo extends.
+    uses: hyperpolymath/standards/.github/workflows/echidna-verify.yml@main

Project.toml

@@ -1,6 +1,7 @@
 name = "CompositionalDA"
 uuid = "a77efed1-127c-5b9d-bf19-e0eccfa50304"
 version = "0.2.0"
+description = "Native Julia compositional differential abundance: implemented ALDEx2 (v0.2); planned ANCOM-BC (v0.3). No Python, no TensorFlow; optional R bridge (temporary)."
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 
 [deps]

README.md

@@ -4,17 +4,20 @@
 # CompositionalDA.jl
 
 Native-Julia compositional differential abundance for microbiome count tables.
-Methods: ALDEx2 and ANCOM-BC. Multinomial and Dirichlet-multinomial regression
+Methods (implemented / planned): ALDEx2 is implemented natively (`src/Methods/ALDEx2.jl`);
+ANCOM-BC is planned for v0.3 (not yet in `src/`). Multinomial and Dirichlet-multinomial regression
 live in a separate package,
 [`CompositionalCounts.jl`](https://github.com/hyperpolymath/CompositionalCounts.jl).
 It needs no Python and no TensorFlow. R is needed only for the optional reference
 backend.
 
-> **Status: v0.2.0.** The core layer (closure, the centred log-ratio, zero
-> policies, Benjamini–Hochberg, result/provenance types) and two-group ALDEx2
-> (`aldex2`) are implemented. ALDEx2 is defined by `docs/ALDEx2-SPEC.md` and
-> agrees with Bioconductor ALDEx2 1.42.0 within Monte-Carlo noise on the mock,
-> gut and soil datasets. ANCOM-BC lands in v0.3.
+> **Status: v0.2.0.** Implemented: the core layer (closure, centred log-ratio,
+> zero policies, Benjamini–Hochberg, result/provenance types) and two-group
+> ALDEx2 (`aldex2`). ALDEx2 is defined by `docs/ALDEx2-SPEC.md` and agrees
+> with Bioconductor ALDEx2 1.42.0 within Monte-Carlo noise on the mock, gut
+> and soil datasets. Planned: ANCOM-BC lands in v0.3; the optional R reference
+> backend (`ext/CompositionalDARCallExt.jl`) will call Bioconductor ALDEx2/
+> ANCOMBC through RCall, shipped as a Julia package extension.
 > Nothing here claims a method that is not yet in `src/`.
 
 ## Input contract

docs/R-SUNSET.md

@@ -12,8 +12,9 @@ present) is a bridge, not a product. It never owns R state. Every R call runs in
 caller-supplied `runner` function, so a host application keeps its own R session
 and lock (MetaManifold passes its `with_r_lock`).
 
-**Criterion.** For each method, once the native implementation agrees with the R
-reference within the tolerances stated in `test/oracle/runoracle.jl` on all three
+**Criterion.** For each implemented method (currently ALDEx2; ANCOM-BC is
+planned for v0.3), once the native implementation agrees with the R reference
+within the tolerances stated in `test/oracle/runoracle.jl` on all three
 reference datasets (mock, gut, soil) for **two consecutive releases**, that
 method's R path is marked deprecated in the next release and receives no
 further maintenance. When no method still needs it, the extension is deleted.

src/CompositionalDA.jl

@@ -5,8 +5,9 @@
     CompositionalDA
 
 Compositional differential-abundance methods for count tables, implemented
-natively in Julia. Input is always a table of raw integer counts with samples as
-rows and features (taxa) as columns.
+natively in Julia. Implemented: ALDEx2 (native `aldex2`). Planned: ANCOM-BC
+(v0.3, not yet in `src/`). Input is always a table of raw integer counts with
+samples as rows and features (taxa) as columns.
 
 The core layer is exported: closure, the centred log-ratio, zero policies,
 Benjamini–Hochberg and the result/provenance types. Its algebraic properties are