Description and README describe an Agda formalisation and a build that do not exist (0 source files; cited dev-note absent; STATE.a2ml says 'repo not yet created')

[hyperpolymath]

Measured (2026-09-22, main = 98193be)

• The tree has 0 files matching .agda|.lean|.thy|.idr|.v and 0 paths under dev-notes/.
• Repo description: "Agda formalisation of a graded multiparty-session type theory combining echo loss-grades and epistemic warrant…".
• README.adoc:37 and :158 say "Nothing in this repo is proven yet." (true), but :98–:112 document a src/ChoreographicTypes/ layout and the command agda --no-libraries -i src src/ChoreographicTypes/All.agda, which cannot run, and :84 and :119 cite dev-notes/2026-06-16-choreographic-types-what-it-is.adoc, which exists nowhere in the tree.
• .machine_readable/6a2/STATE.a2ml:22: status = "pre-registration (repo not yet created)" while the repo exists.

Why it matters

A reader, or a sibling repo's CI, that trusts the description or the build table looks for a formalisation that is not there. The only true statement is the pre-registration one.

Ruling

Owner ruling D-4 (2026-09-22, selection UI; booked on hyperpolymath/standards#787, rows D78–D81): correct the description and keep the repo as a pre-registration. Do not scaffold a placeholder src/ tree to make the README true.

Acceptance criteria

1. The repo description says what is true today (a pre-registration / paper-only repo for the graded multiparty-session theory); "Agda formalisation" returns only once a checked module exists.
2. README.adoc either ships the cited dev-note at the cited path, or the two citations (:84, :119) are removed. The src/ChoreographicTypes/ table rows and the agda … command are removed or moved under a heading that says planned, with no command a reader can copy and fail.
3. The .a2ml file is retired, not edited: A2ML is a dead format in this estate (owner doctrine). Its pre-registration text moves into README.adoc or a plain .adoc under docs/.
4. Watched-failing → green: gh api repos/hyperpolymath/choreographic-types/git/trees/main?recursive=1 --jq '.tree[].path' | grep -c 'dev-notes/2026-06-16' is 0 today; after the fix it is 1, or grep -c 'dev-notes/2026-06-16' README.adoc is 0. grep -c 'src/ChoreographicTypes' README.adoc is 0, or every occurrence sits under the "planned" heading.

Note on the red Secret Scanner

The Secret Scanner reds since 2026-09-20 are not a repo defect. This is the only private repo of the family, and every job of run 35478897141 (attempts 1–3; the last two re-run 2026-09-22T19:51Z and 19:52Z) carries the check-run annotation "The job was not started because recent account payments have failed or your spending limit needs to be increased". Private repos bill Actions minutes; the public siblings ran green in the same hour. Owner-side billing, tracked outside this issue.

🤖 Generated with Claude Code