theory: an append-only ledger of the theory work

.machine_readable/coaptation/receipts/latest.toml

@@ -10,9 +10,9 @@ band = "amber"
 proposed-action = "advisory — soft drift within bands (posture/intend). Open an advisory issue; no re-anchor."
 
 [coverage]
-clauses-total = 57
+clauses-total = 58
 descriptile-witnessed = 2
-probe-deferred-to-hunt = 32
+probe-deferred-to-hunt = 33
 must-trust-unmeasured-gaps = 0
 note = "Yard sees descriptile evidence only; probe-deferred obligations need a Hunt-tier run for a full hard-gate."
 
@@ -21,7 +21,7 @@ grade = "boolean_gate / boolean_gate_provenance"
 witnessed = 1
 refuted = 0
 unmeasured-gaps = 0
-probe-deferred = 32
+probe-deferred = 33
 gate = "pass"
 
 [reading.adjust]
@@ -71,6 +71,7 @@ must.no-hand-typed-grade = "probe-deferred"
 must.receipts-stay-home = "probe-deferred"
 must.home-theorem-has-receipt = "probe-deferred"
 must.rows-have-provenance = "probe-deferred"
+must.theory-ledger-current = "probe-deferred"
 trust.no-secrets-committed = "probe-deferred"
 trust.no-private-keys = "probe-deferred"
 trust.no-tokens-in-source = "probe-deferred"
@@ -103,5 +104,5 @@ bust.sync-drift-between-repos = "latent"
 bust.contractile-parse-error = "latent"
 
 [provenance]
-contractiles = "intend@89c97164fbff must@b2888ac670fb trust@484d6509ce86 adjust@f7e9bafc614e dust@bdb7dea20424 bust@4de1f1b3bc91"
+contractiles = "intend@89c97164fbff must@1c538d416df3 trust@484d6509ce86 adjust@f7e9bafc614e dust@bdb7dea20424 bust@4de1f1b3bc91"
 descriptiles = "deed@7182c2cc6635 anchor@bba9793279e0"

.machine_readable/contractiles/must/must.k9.ncl

@@ -285,6 +285,14 @@ let base    = import "../_base.ncl" in
         severity = 'critical,
         notes = "Re-anchoring plan WO 2.1. A row without either field makes jq fail, and the probe fails closed.",
       },
+      {
+        id = "theory-ledger-current",
+        section = "Mathesis Invariants",
+        description = "The theory ledger records each home theorem's current admission and receipt pin, and only `just theory-ledger` writes it",
+        probe = "bun scripts/registry/theory-ledger.mjs verify >/dev/null",
+        severity = 'critical,
+        notes = "Owner ruling 2026-11-11. The probe is offline. just registry-check (part of just check) also checks the derived grade, and that the ledger on main is a prefix of this one (append-only).",
+      },
     ],
   },
 

Justfile

@@ -768,4 +768,11 @@ registry:
 # Fail if the committed registry view is stale (needs MATHESIS_STANDARDS, as above)
 registry-check:
     bun scripts/registry/claims-registry.mjs check
+    bun scripts/registry/theory-ledger.mjs verify
     bun test tests/registry/
+
+# Append each change of the theory shelf to docs/theory/ledger.jsonl, the only
+# way the ledger changes (needs MATHESIS_STANDARDS, as above). A note tells the
+# story: just theory-ledger "THY-2 admitted after its Lean leg landed"
+theory-ledger note="":
+    bun scripts/registry/claims-registry.mjs ledger {{ if note == "" { "" } else { "--note " + quote(note) } }}

docs/status/ROADMAP.adoc

@@ -153,9 +153,14 @@ One pull request that changes census rows is open at a time (atlas README,
   generates `docs/theory/generated/index.adoc`. All template example proofs
   and the six template stubs under `docs/theory/` are removed (owner rulings
   2026-11-11).
-* Next, by owner ruling: an append-only ledger of the theory work, written
-  only by a `just theory-ledger` recipe and checked in CI, in its own pull
-  request.
+* WO 4.1 merged (pull request 79).
+* The theory ledger (owner ruling 2026-11-11): `docs/theory/ledger.jsonl`,
+  append-only, written only by `just theory-ledger`. `just registry-check`
+  fails when the ledger is behind or a past entry changed; the `must` clause
+  `theory-ledger-current` states the invariant (approved by the owner).
+* The IANA registration drafts of DEED, K9 and k9-coordination are
+  corrected in a separate session on the standards repository; filing is
+  the owner's act.
 * Finding: the `intend` contract still marks stage 3 `in_progress` and
   stage 4 `declared`; a contract edit needs owner review.
 
@@ -194,7 +199,7 @@ anchors `c81cb84`
 |The three shelves: the theory admission rule and the token-lattice
 theorems, the applied shelf tied to the evidence spine, the published atlas
 (needs a ruling)
-|In progress: WO 4.1 in review
+|In progress: WO 4.1 merged; the theory ledger in review
 
 |5
 |Scale: receipts in the home repositories, the bridge lock pilot, a

docs/theory/README.adoc

@@ -39,6 +39,11 @@ holds no grade.
 |The theorem index, generated by `scripts/registry/claims-registry.mjs` from
 the admission records, the claim pins and the receipt. Never edit it by hand.
 
+|`ledger.jsonl`
+|The story of the theory work: one entry for each admission, withdrawal, or
+change of receipt pin, admission or derived grade, with an optional note.
+Append-only, and written only by `just theory-ledger`.
+
 |`../../verification/proofs/`
 |The Agda, Rocq and Lean sources.
 
@@ -49,15 +54,18 @@ the admission records, the claim pins and the receipt. Never edit it by hand.
 `just registry-check` (part of `just check`) fails when the index is stale,
 when a home theorem has no admission record, or when an admission names no
 dependant, a non-public dependant repository, or a theorem with no claim
-pin.
+pin. It also fails when the ledger is behind the current state, or when the
+ledger on `main` is not a prefix of this one (an altered or lost past entry).
 
 == Admitting a theorem
 
 . State the theorem, prove it in Agda, and re-prove it in Rocq and Lean.
 . Add each leg to the receipt, from observed checker runs.
 . Pin the claim in `docs/atlas/claims/claims.jsonl`.
 . Add its admission record to `admissions.jsonl`.
-. Run `bun scripts/registry/claims-registry.mjs build`, then `just check`.
+. Run `bun scripts/registry/claims-registry.mjs build`.
+. Run `just theory-ledger "a note that tells what happened"`, then
+  `just check`.
 
 The token-lattice theorems are the next candidates (ruling D-10). Their
 statements are in `docs/proposals/mathesis-research-programme.adoc`.

docs/theory/ledger.jsonl

@@ -0,0 +1 @@
+{"admission_sha256":"91977ed786bb4a63913234167876096bf6e93491e828dcc3e1e7538862349fc5","date":"2026-11-11","event":"admitted","id":"hyperpolymath/mathesis#THY-1","note":"The ledger starts here, on 2026-11-11. THY-1 was proved in Agda on 2026-11-09 and re-proved in Rocq and Lean; it derived PWG-2ii until the CI receipts of run 42896264290 gave PWG-1 on 2026-11-10. Transport from Agda was blocked, because the Lambdapi exports to Rocq and Lean drop rewrite rules. Earlier history is in git and docs/status/PROOF-STATUS.adoc.","pwg":"PWG-1","receipt":{"commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","path":"verification/receipts/theory_praxis.deed","sha256":"001903cb2cf4822aa3a8b4d7ff9bbc8cec99a72d73135df71795529272f95101"},"seq":1}

mathesis_chora.deed

@@ -1021,7 +1021,8 @@
               "verification/proofs/agda/FeatureReachability.agda"
               "verification/proofs/coq/FeatureReachability.v"
               "verification/proofs/lean4/FeatureReachability.lean"
-              "EXPLAINME.adoc")
+              "EXPLAINME.adoc"
+              "docs/theory/admissions.jsonl" "docs/theory/ledger.jsonl" "docs/theory/generated/")
       :removed ("archetypes/" "build/docs-seed/" "build/templates/" "rsr-template-repo_chora.deed"
                 "src/interface/" "benches/" "build/container/Containerfile"
                 "tests/ffi_strings_test.sh"

scripts/registry/claims-registry.mjs

@@ -29,6 +29,7 @@ import path from 'node:path';
 import {readJsonl} from '../atlas/census-atlas.mjs';
 import {validateBridges, renderBridges} from './bridges.mjs';
 import {validateAdmissions, renderTheoryIndex} from './theory.mjs';
+import {validateLedger, snapshot, pending, checkAppendOnly, jcs} from './theory-ledger.mjs';
 
 const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../..');
 const claimsFile = path.join(root, 'docs/atlas/claims/claims.jsonl');
@@ -38,6 +39,19 @@ const bridgesFile = path.join(root, 'docs/atlas/claims/bridges.jsonl');
 const bridgesView = path.join(root, 'docs/atlas/generated/bridges.adoc');
 const admissionsFile = path.join(root, 'docs/theory/admissions.jsonl');
 const theoryView = path.join(root, 'docs/theory/generated/index.adoc');
+const ledgerFile = path.join(root, 'docs/theory/ledger.jsonl');
+
+// The theory ledger as it stands on main, for the append-only check, read
+// over HTTPS like the receipts (no subprocess, and the local clone is left
+// as it is). A 404 means main has no ledger yet, so every entry is new; any
+// other failure stops the check: an unchecked ledger is not a passing one.
+const LEDGER_ON_MAIN = 'https://raw.githubusercontent.com/hyperpolymath/mathesis/main/docs/theory/ledger.jsonl';
+async function ledgerOnMain() {
+  const res = await fetch(LEDGER_ON_MAIN);
+  if (res.status === 404) return '';
+  if (!res.ok) throw new Error(`could not fetch ${LEDGER_ON_MAIN}: HTTP ${res.status}`);
+  return res.text();
+}
 
 const KINDS = new Set(['theorem', 'demonstration', 'assumption']);
 const PWG = new Set(['PWG-1', 'PWG-2ii', 'PWG-2i', 'PWG-3', 'ungraded']);
@@ -216,8 +230,8 @@ export function render(derived) {
 
 async function main() {
   const [cmd, ...args] = process.argv.slice(2);
-  if (cmd !== 'build' && cmd !== 'check') {
-    console.error('usage: claims-registry.mjs build|check [--receipts-dir DIR]');
+  if (!['build', 'check', 'ledger'].includes(cmd)) {
+    console.error('usage: claims-registry.mjs build|check|ledger [--receipts-dir DIR] [--note TEXT]');
     process.exit(2);
   }
   const i = args.indexOf('--receipts-dir');
@@ -227,6 +241,16 @@ async function main() {
   const bridges = validateBridges(await readJsonl(bridgesFile), inventory);
   const admissions = validateAdmissions(await readJsonl(admissionsFile), rows, inventory);
   const derived = await deriveAll(rows, receiptsDir, await loadReader());
+  const ledger = validateLedger(await readJsonl(ledgerFile));
+  const current = snapshot(rows, admissions, new Map(derived.map(d => [d.row.id, d.pwg])));
+  if (cmd === 'ledger') {
+    const n = args.indexOf('--note');
+    const note = n >= 0 ? args[n + 1] : undefined;
+    const add = pending(ledger, current, new Date().toISOString().slice(0, 10), note);
+    if (add.length) await writeFile(ledgerFile, [...ledger, ...add].map(e => jcs(e) + '\n').join(''));
+    console.log(`theory ledger: ${add.length} new entries, ${ledger.length + add.length} in all`);
+    return;
+  }
   const views = [[viewFile, render(derived)], [bridgesView, renderBridges(bridges)], [theoryView, renderTheoryIndex(derived, admissions)]];
   if (cmd === 'build') {
     await Promise.all(views.map(([file]) => mkdir(path.dirname(file), {recursive: true})));
@@ -236,7 +260,10 @@ async function main() {
     const committed = await Promise.all(views.map(([file]) => readFile(file, 'utf8').catch(() => '')));
     const stale = views.filter(([, body], i) => committed[i] !== body).map(([file]) => path.relative(root, file));
     if (stale.length) throw new Error(`${stale.join(', ')} stale; run: bun scripts/registry/claims-registry.mjs build`);
-    console.log(`PASS: claims registry derived from ${new Set(rows.map(r => r.repo + '@' + r.source_commit)).size} pinned source(s); views match (${rows.length} claims, ${bridges.length} bridges, ${admissions.length} admissions)`);
+    const due = pending(ledger, current, '0000-00-00');
+    if (due.length) throw new Error(`docs/theory/ledger.jsonl is behind by ${due.length} entries; run: just theory-ledger`);
+    checkAppendOnly(await ledgerOnMain(), await readFile(ledgerFile, 'utf8'));
+    console.log(`PASS: claims registry derived from ${new Set(rows.map(r => r.repo + '@' + r.source_commit)).size} pinned source(s); views match (${rows.length} claims, ${bridges.length} bridges, ${admissions.length} admissions); the theory ledger is current and append-only (${ledger.length} entries)`);
   }
 }