docs(truth): correct citation abstract; guard description surfaces (issue #15)

CITATION.cff

@@ -2,7 +2,7 @@ cff-version: 1.2.0
 message: "If you use this software, please cite it as below."
 type: software
 title: "Choreographic Types"
-abstract: "Agda formalisation of a graded multiparty-session type theory combining echo loss-grades and epistemic warrants on partial causal orders. The central artefact is K-CUT: the open conjecture that grading and transport commute with endpoint projection across a consistent frontier (antichain), splitting into equality on loss-grades/bound on warrants."
+abstract: "Pre-registration and research notebook for a graded multiparty-session type theory combining echo loss-grades and epistemic warrants on partial causal orders. The central artefact is K-CUT: the open conjecture that grading and transport commute with endpoint projection across a consistent frontier (antichain), splitting into equality on loss-grades/bound on warrants. Agda is the intended prover; no checked formalisation exists yet."
 authors:
   - family-names: "Jewell"
     given-names: "Jonathan D.A."

docs/actions-policy.adoc

@@ -66,11 +66,12 @@ rather than silently rewriting the broader permission settings.
 == Repository description (issue #15)
 
 The local documentation now describes the pre-registration honestly. The
-remote description still needs the following owner-authorised update:
+remote description still needs the following owner-authorised update. The
+canonical text is 345 characters (GitHub's limit is 350):
 
 [source,bash]
 ----
-gh repo edit hyperpolymath/choreographic-types --description 'Pre-registration and research notes for a graded multiparty-session theory combining echo loss-grades and epistemic warrants. K-CUT remains an open conjecture; application targets are not proofs.'
+gh repo edit hyperpolymath/choreographic-types --description 'Pre-registration and research notebook for a graded multiparty-session type theory combining echo loss-grades and epistemic warrants on partial causal orders. Central artefact: K-CUT, the open conjecture that grading and transport commute with endpoint projection across a consistent frontier. Agda is the intended prover; no checked module yet.'
 gh repo view hyperpolymath/choreographic-types --json description
 ----
 
@@ -101,3 +102,24 @@ owner-side check because ordinary Actions tokens cannot read admin settings.
 
 Issues #15 and #16 must remain open until the repository changes are merged
 and the remaining owner-side acceptance checks pass.
+
+== Re-verification (2026-10-03, issue #15 follow-up)
+
+* README acceptance re-measured: `grep -c 'dev-notes/2026-06-16' README.adoc`
+  is 0 and `grep -c 'src/ChoreographicTypes' README.adoc` is 0. No `.a2ml`
+  file exists anywhere in the tree; the pre-registration text lives in
+  link:pre-registration.adoc[].
+* The citation abstract in `CITATION.cff` carried the same "Agda
+  formalisation" claim as the remote description. It was corrected to match
+  the pre-registration status.
+* `scripts/check-repository.mjs` now fails any completed-formalisation claim
+  ("Agda formalisation") on the two description-mirroring surfaces
+  (`README.adoc`, `CITATION.cff`), and requires `CITATION.cff` to disclose
+  pre-registration status. Regression tests cover all four cases (16 tests
+  total, all passing locally with Node 22).
+* Description PATCH re-attempted with the owner-authorised connection:
+  still HTTP 403 (resource not accessible by integration). The owner repair
+  command above therefore remains the only path for criterion 1 of #15.
+* CI state: this repository is public; Documentation Integrity and Secret
+  Scanner runs on `main` are green. The 2026-09-22 billing refusals noted in
+  #15 were private-repo billing state, not a workflow defect.

docs/pre-registration.adoc

@@ -2,14 +2,20 @@
 = Pre-registration, provenance and research obligations
 :toc:
 
-== Current status (2026-09-27)
+== Current status (2026-10-03)
 
 This repository exists and is licensed under MPL-2.0 (see link:../LICENSE[]).
 It is a pre-registration and research notebook, not a checked formalisation.
 K-CUT-LOSS and K-CUT-WARRANT remain OPEN. `SoundWarrant` is an assumed
 receiver-local side-condition, not a result established here.
 The application Agda file contains postulates, not proofs.
 
+The in-repo citation metadata (`CITATION.cff`) no longer claims a completed
+Agda formalisation; the integrity checks now fail such claims on the
+description-mirroring surfaces. The GitHub repository description still needs
+the owner-authorised correction recorded in
+link:actions-policy.adoc#_repository_description_issue_15[Actions policy, "Repository description"].
+
 This document retires the former machine-readable state format. The ledger
 below preserves the 2026-06-16 research intent and later application targets.
 Sibling proof claims are historical provenance, not independently rechecked

scripts/check-repository.mjs

@@ -34,6 +34,20 @@ export function checkRepository(root) {
   for (const [, source] of readme.matchAll(/\bagda\b[^\n]*?([\w./-]+\.agda)/g)) {
     if (!existsSync(resolve(root, source))) errors.push(`Nonexistent Agda build target: ${source}`);
   }
+  // The surfaces that mirror the repository description must not claim a
+  // completed formalisation until a checked module exists (issue #15, D-4).
+  // Relax this in the same change that lands the first checked module.
+  for (const surface of ['README.adoc', 'CITATION.cff']) {
+    const surfacePath = resolve(root, surface);
+    if (!existsSync(surfacePath)) continue;
+    if (/agda\s+formali[sz]ation/i.test(readFileSync(surfacePath, 'utf8'))) {
+      errors.push(`Description claim of a completed Agda formalisation in ${surface}; not true until a checked module exists`);
+    }
+  }
+  const citationPath = resolve(root, 'CITATION.cff');
+  if (existsSync(citationPath) && !/pre-registration/i.test(readFileSync(citationPath, 'utf8'))) {
+    errors.push('CITATION.cff must disclose pre-registration status');
+  }
   return errors;
 }
 

tests/repository.test.mjs

@@ -29,6 +29,23 @@ for (const [name, files, expected] of [
   ['lost project disclosure', { 'README.adoc': 'Nothing in this repo is proven yet.' }, /pre-registration status/],
 ]) test(`regression: ${name}`, t => assert.match(checkRepository(fixture(t, files)).join('\n'), expected));
 
+test('regression: completed-formalisation claim in README', t => {
+  const files = { 'README.adoc': status + 'An Agda formalisation of a graded theory.\n' };
+  assert.match(checkRepository(fixture(t, files)).join('\n'), /completed Agda formalisation/);
+});
+test('regression: completed-formalisation claim in CITATION.cff', t => {
+  const files = { 'CITATION.cff': 'abstract: "Agda formalisation of a graded multiparty-session type theory."\n' };
+  assert.match(checkRepository(fixture(t, files)).join('\n'), /completed Agda formalisation/);
+});
+test('regression: citation without pre-registration disclosure', t => {
+  const files = { 'CITATION.cff': 'title: "Choreographic Types"\nabstract: "A graded theory notebook."\n' };
+  assert.match(checkRepository(fixture(t, files)).join('\n'), /CITATION\.cff must disclose/);
+});
+test('honest citation metadata passes', t => {
+  const files = { 'CITATION.cff': 'abstract: "A pre-registration; Agda is the intended prover, no checked formalisation yet."\n' };
+  assert.deepEqual(checkRepository(fixture(t, files)), []);
+});
+
 const canon = { github_owned_allowed: true, verified_allowed: true, patterns_allowed: ['owner/a@*', 'owner/b@*'] };
 test('payload strips non-API metadata', () => assert.deepEqual(payloadFrom({ ...canon, version: 1 }), canon));
 test('empty, malformed and duplicate patterns fail closed', () => {