feat(registry): proposed theorem-level claims registry deriving PWG from home receipts (ADR 0004)

.github/workflows/proven-tests.yml

@@ -49,6 +49,14 @@ jobs:
         run: |
           bun scripts/atlas/census-atlas.mjs check
           bun test tests/atlas/census-atlas.test.mjs
+      # The claims registry (docs/decisions/0004-claims-registry.adoc): re-derive
+      # every grade from the home repositories' receipts at their pinned commits
+      # (fetched, digest-checked) and fail if the committed view is stale or a
+      # receipt asserts a grade its evidence does not support.
+      - name: Mathesis claims registry derivation and tests
+        run: |
+          bun scripts/registry/claims-registry.mjs check
+          bun test tests/registry/claims-registry.test.mjs
       - name: Install verified Nickel 1.18.0 (K9 L2 semantics)
         run: |
           set -euo pipefail

Justfile

@@ -738,3 +738,13 @@ atlas-check:
 
 atlas-find query:
     bun scripts/atlas/census-atlas.mjs find "{{query}}"
+
+# Theorem-level claims registry (ADR 0004): fetch each pinned receipt, derive
+# Proof Witness Grades, and write docs/registry/registry.adoc
+registry:
+    bun scripts/registry/claims-registry.mjs build
+
+# Fail if the committed registry view is stale or a receipt overstates its grade
+registry-check:
+    bun scripts/registry/claims-registry.mjs check
+    bun test tests/registry/claims-registry.test.mjs

README.adoc

@@ -19,6 +19,7 @@ in Rocq and Lean). The working method is the proof-craft skill.
 
 * link:docs/standards/README.adoc[Standards and authority map] — estate proof policy, proof/test evidence ownership, and Mathesis's limits.
 * link:docs/atlas/README.adoc[Discovery atlas] — the current generated, read-only first slice (repository index, not theorem-level certification).
+* link:docs/registry/registry.adoc[Claims registry, pilot slice] — theorem-level, grades *derived* from home-repository receipts at pinned commits; proposed in link:docs/decisions/0004-claims-registry.adoc[ADR 0004], not yet ratified.
 * link:docs/proposals/estate-mathematical-architecture.adoc[Estate mathematical architecture proposal] — the original long-term design brief, preserved but *not ratified*. Its proposed proof grades do not override the standards policy.
 * link:docs/architecture/REPOSITORY-MAP.adoc[Generated repository map] — current path inventory, not the mathematical architecture specification.
 

docs/architecture/REPOSITORY-MAP.adoc

@@ -117,6 +117,10 @@ predecessors did.
 | yes
 | -
 
+| `applied-systems/`
+| yes
+| owner-requested reusable applications area (2026-11-07)
+
 | `benches/`
 | optional
 | Cargo-conventional at package root
@@ -204,6 +208,11 @@ your own repo - but do not read their emptiness as neglect here.
 | `.machine_readable/bot_directives/`
 | `.machine_readable/descriptiles/anchors/`
 | `.machine_readable/scripts/verification/`
+| `applied-systems/decision-science/`
+| `applied-systems/finance/`
+| `applied-systems/finance/cohort-economics/`
+| `applied-systems/finance/liquidity/`
+| `applied-systems/organisational-design/`
 | `docs/governance/audit/`
 | `docs/governance/audit/compliance/`
 | `docs/governance/audit/effects/`

docs/atlas/README.adoc

@@ -18,5 +18,7 @@ Proof declarations, axioms and holes are *counts found by the original census*.
 They are not kernel-check receipts; source files are not included in the
 summarised rows, so this atlas must not invent per-theorem names, evidence,
 proof status, assumptions, equivalence, or independent verification.
-The next slice requires a separately reviewed, source-anchored claims registry.
+The next slice requires a separately reviewed, source-anchored claims registry;
+it is proposed in link:../decisions/0004-claims-registry.adoc[ADR 0004]
+(pilot view: link:../registry/registry.adoc[`docs/registry/registry.adoc`]).
 No private-source records are added or published by this generator.

docs/decisions/0004-claims-registry.adoc

@@ -0,0 +1,149 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Architecture Decision Record: 0004-claims-registry
+
+== 4. A theorem-level claims registry that derives grades and never assigns them
+
+Date: 2026-11-09
+
+=== Status
+
+*Proposed — awaiting owner ratification.* Nothing here is estate policy until
+the owner rules on it. Ratification is the owner's merge of the pull request
+that introduces this file, with this Status changed to `Accepted (ratified by
+owner <date>)` in the same change. Until then the registry view
+(`docs/registry/registry.adoc`) says on its face that the slice is proposed.
+
+=== Context
+
+The atlas (`docs/atlas/README.adoc`) stops at repository-level counts and says
+so: "The next slice requires a separately reviewed, source-anchored claims
+registry." The architecture brief
+(`docs/proposals/estate-mathematical-architecture.adoc`) names that slice as
+Stage 1 (schema decision) and Stage 4 (proof-level indexing), with `registry/`
+and `schemas/` directories; its proof grades were adopted, corrected, as
+`PROOF-POLICY.adoc` §8 (owner ruling 2026-11-04), which binds what a registry
+may say:
+
+* §8.4: grades are *derived*, not asserted; a hand-written grade the receipts
+  do not support is drift; a census, never a percentage.
+* §8.5: each theorem's grade is recorded in its *home repository*; "Mathesis
+  may catalogue grades. It derives them from those receipts and does not assign
+  them."
+* `docs/standards/AUTHORITY.adoc` (this repository): pin claims to source
+  commits, checker versions, assumptions and receipts; never infer a missing
+  field from a green badge; proof receipts stay in their home repositories.
+
+So the registry's job is narrow: point at a claim in its home repository at an
+exact commit, fetch that repository's own machine receipt, recompute the grade
+by §8.2, and report disagreements. It is a checker of home-repository claims,
+not a second ledger.
+
+=== Decision
+
+==== Record (the schema)
+
+`docs/registry/claims.json` is one I-JSON/JCS array. Each record has exactly
+these fields; `scripts/registry/claims-registry.mjs` `validate` enforces them
+and the tests prove each failure.
+
+[cols="1,3",options="header"]
+|===
+|Field |Meaning
+
+|`id` |`<owner>/<repo>#<claim>`; unique.
+|`repo` |The home repository. It must be `public` in
+`docs/catalogue/census/repos.json`: the registry never names a private
+repository, so it cannot leak one (brief §7).
+|`claim` |The claim's id in the home repository's proof-status file (`N-7`, `L-6`).
+|`kind` |`theorem` (graded, §8.1), `demonstration` (a TESTED example) or `assumption`
+(an ASSUMED hypothesis). Only theorems are graded.
+|`statement` |The statement in the home repository's own wording. Mathesis
+does not restate mathematics.
+|`status_doc` |The home repository's proof-status file.
+|`agda` |For a theorem: `{module, names}`, the Agda source of truth (§1). `null`
+otherwise.
+|`source_commit` |The full 40-character commit the record describes.
+|`receipt` |`{path, sha256}` of the home repository's machine receipt at that
+commit, or `null` when it has none.
+|===
+
+A record holds *no grade, token, leg or flag*. Those are read from the receipt.
+
+==== Derivation (PROOF-POLICY §8.1–§8.2)
+
+For each record, the tool fetches the receipt at `source_commit`, refuses it
+if its sha256 differs from the pinned digest, and derives:
+
+. not a theorem → `ungraded` (§8.1);
+. no receipt, or the claim absent from it → `ungraded`;
+. the receipt's flags lack any of `--safe --without-K --cubical-compatible` →
+  `ungraded` (§2.1 is a condition of `PWG-3`);
+. the Agda token is not `proven` or `proven-with-postulates` → `ungraded`;
+. otherwise `PWG-3`, `PWG-2i` or `PWG-2ii` by the number of legs whose §2.2
+  state is `RECONCILED`. A leg's route never counts on its own.
+
+`PWG-1` is never derived in this slice: it needs a current receipt for every
+counted witness, and the slice reads only the Agda-side receipt.
+
+Two kinds of disagreement are reported. A receipt that asserts a `:pwg` its
+evidence does not support is *drift* (§8.4) and fails the check. A receipt that
+still uses the pre-§8 vocabulary (`:grade "grade-3"`) is a visible *finding*,
+not a failure: the vocabulary changed after the receipt was written.
+
+==== View, gate and tooling
+
+* `docs/registry/registry.adoc` is generated (`just registry`) and checked
+  (`just registry-check`, and CI `proven-tests.yml`): stale view, digest
+  mismatch, or drift fails. The view opens with a §8.4.7 census line.
+* The tool is Bun, beside the atlas (`scripts/atlas/census-atlas.mjs`), with
+  hermetic tests (`tests/registry/claims-registry.test.mjs`, `--receipts-dir`
+  fixtures): the ladder, each withheld reason, drift versus legacy finding,
+  digest refusal, validation failures, and "never a percentage".
+* Receipts are fetched from `raw.githubusercontent.com` at the pinned commit,
+  never vendored (AUTHORITY: receipts stay home).
+
+==== Pilot rows
+
+Seventeen claims from the two repositories whose proofs this work audited:
+`hyperpolymath/secret-types` (N-1 to N-9) and `metadatastician/lintel` (L-1 to
+L-7, A-1), each pinned at its `main` of 2026-11-09. At those commits the
+derivation gives *0 of 12 theorems graded*, and says why:
+
+* secret-types `eee4e40`: the receipt records the flag set without
+  `--cubical-compatible` (waiver W-1), and uses the pre-§8 "grade-3" wording.
+  hyperpolymath/secret-types#32 puts the flag in force and writes the §8.5
+  receipt; once it merges, bumping the pin should derive `PWG-3`.
+* Lintel `a0f2bae`: no machine receipt exists in the repository.
+
+That the pilot reports zero is the point: it is what the evidence supports today.
+
+=== Alternatives considered
+
+* *Store grades in the registry.* Rejected: §8.4 and §8.5 forbid assigning
+  them, and a stored grade drifts silently when the home repository moves.
+* *Vendor receipts into Mathesis.* Rejected: AUTHORITY keeps receipts home;
+  a pinned digest gives the same tamper-evidence without a copy.
+* *A JSON Schema file validated by a library.* Deferred: it adds a pinned npm
+  dependency for checks the 40-line `validate` already makes and tests. A
+  schema file can be generated from `validate` later if a consumer needs one.
+* *A ruling in `standards` first.* Possible, slower: the registry's authority
+  would sit beside PROOF-POLICY §8.5. Chosen instead: ratify here, because the
+  registry only *reads* the policy and adds no rule to it.
+
+=== Consequences
+
+* Mathesis can answer "which theorems, at which grade, why not higher" for the
+  piloted repositories, with every answer traceable to a commit and a digest.
+* A home repository whose receipt overstates its grade turns this repository's
+  CI red. That is intended (§8.4.2: "a gate or a bot may recompute it at any
+  time and reports the computed value").
+* The census rows and the atlas are unchanged; the registry sits beside them.
+* After ratification, in order:
+  . Lintel: move its real ledger into `docs/status/PROOF-STATUS.adoc`, retire
+    the template boilerplate, adopt the §2.1 invocation and add a receipt;
+  . `scripts/census/build-rows.sh`: prefer `PROOF-STATUS` over `PROOF-NEEDS`
+    when choosing a repository's status document, then refresh the two rows;
+  . list both repositories as the first §2 reconciliation pilot in
+    `docs/status/CROSS-PROVER-RECONCILIATION.adoc`;
+  . bump the pilot pins as those changes land.

docs/registry/claims.json

@@ -0,0 +1 @@
+[{"agda":{"module":"SecretTypes.Noninterference","names":["tini"]},"claim":"N-1","id":"hyperpolymath/secret-types#N-1","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Noninterference","names":["eval-low"]},"claim":"N-2","id":"hyperpolymath/secret-types#N-2","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Public expressions read the same in low-equivalent stores","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Noninterference","names":["confine"]},"claim":"N-3","id":"hyperpolymath/secret-types#N-3","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Confinement: under a secret program counter the public variable is unchanged, loops included","status_doc":"PROOF-STATUS.adoc"},{"agda":null,"claim":"N-4","id":"hyperpolymath/secret-types#N-4","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"The typing side-condition is load-bearing: an explicit and an implicit flow are each refused and each actually leaks","status_doc":"PROOF-STATUS.adoc"},{"agda":null,"claim":"N-5","id":"hyperpolymath/secret-types#N-5","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another","status_doc":"PROOF-STATUS.adoc"},{"agda":null,"claim":"N-6","id":"hyperpolymath/secret-types#N-6","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Laws census: generic TINI uses exactly the two upper-bound laws and the observer's down-closure (law-ablation certificate)","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Noninterference.Generic","names":["tini"]},"claim":"N-7","id":"hyperpolymath/secret-types#N-7","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"TINI over the Lattice record: for every variable set with decidable equality, lattice, labelling and down-closed observer, two finishing runs of a well-typed command from stores agreeing on what the observer sees end agreeing on it","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Countermodels","names":["NoUpper₁.refutes","NoUpper₂.refutes","NoDownClosure.refutes","NoTrans.refutes"]},"claim":"N-8","id":"hyperpolymath/secret-types#N-8","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Each census law is necessary: dropping an upper-bound law or observer down-closure admits a well-typed leaking program; transitivity is necessary for principal observers","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Noninterference.OutcomeVisibility","names":["termination-sensitive-fails"]},"claim":"N-9","id":"hyperpolymath/secret-types#N-9","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"Lintel.Lattice","names":["⊑-refl","⊑-trans","⊑-antisym","⊔-upper₁","⊔-upper₂","⊔-least","⊓-lower₁","⊓-lower₂","⊓-greatest","anyone-least","no-one-greatest","no-one-⋢-anyone","_⊑?_"]},"claim":"L-1","id":"metadatastician/lintel#L-1","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"A lattice, not just a poset: ⊑ is a decidable partial order, ⊔ and ⊓ are least upper and greatest lower bounds, anyone is least and no-one greatest","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Lattice","names":["⊑-readers","readers-⊑","observes-flow","flow-observes"]},"claim":"L-2","id":"metadatastician/lintel#L-2","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"⊑ is reverse inclusion of reader sets; a role sees a label exactly when the label may flow to that role's observer level","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Instance","names":["reader-sets"]},"claim":"L-3","id":"metadatastician/lintel#L-3","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"The laws secret-types' generic TINI needs hold here, packed as an instance of its Lattice record","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Lattice","names":["address-to-proxy","qname-to-target","link","link-confined"]},"claim":"L-4","id":"metadatastician/lintel#L-4","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"Address and query name each reach their own role; composed, only the client may observe them","status_doc":"README.adoc"},{"agda":null,"claim":"L-5","id":"metadatastician/lintel#L-5","kind":"demonstration","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"The typechecker refuses the self-defeating compositions and accepts the client's","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Instance","names":["tini-per-role","tini-coalition"]},"claim":"L-6","id":"metadatastician/lintel#L-6","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"tini holds at this lattice over the address, the query name and the client's local state, for each role's observer and for any two roles observing together","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Composition","names":["writes-flow","link-written-to-client","link-written-to-local","link-writable"]},"claim":"L-7","id":"metadatastician/lintel#L-7","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"Self-defeating privacy compositions cannot be built as programs: a typed command writes a value depending on both fields only into a variable the client alone may read","status_doc":"README.adoc"},{"agda":null,"claim":"A-1","id":"metadatastician/lintel#A-1","kind":"assumption","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"Non-collusion: no party holds both the proxy and the target role (the gap is proved: collusion-gap)","status_doc":"README.adoc"}]