Repository navigation
feat(registry): proposed theorem-level claims registry deriving PWG from home receipts (ADR 0004) - #38
Conversation
…WG from home receipts (ADR 0004)
The atlas stops at repository counts and says the next slice needs a
separately reviewed, source-anchored claims registry. This proposes it, for
the owner to ratify (ADR 0004, Status: Proposed).
- docs/registry/claims.json (I-JSON/JCS): source-anchored facts only. Each
record gives repo, claim id, kind, the statement in the home repository's
wording, Agda module and names, a 40-character commit, and the receipt
{path, sha256}. No grade, token, leg or flag is stored.
- scripts/registry/claims-registry.mjs: fetch each receipt at its pinned
commit, refuse a digest mismatch, and derive the Proof Witness Grade by
PROOF-POLICY §8.2:
* the §2.1 flags are required;
* a proven token is required;
* legs count only when RECONCILED;
* PWG-1 is never derived in this slice.
A receipt asserting a :pwg its evidence does not support is §8.4 drift and
fails; pre-§8 ":grade" wording is a visible finding.
- docs/registry/registry.adoc: the generated view, opening with a §8.4.7
census line (counts with denominator, no percentage).
- tests/registry: 7 hermetic tests, 31 assertions; just registry /
registry-check; CI step in proven-tests.yml beside the atlas.
- Pilot: 17 claims from hyperpolymath/secret-types and
metadatastician/lintel at their 2026-11-09 mains. The result is 0 of 12
theorems graded, and it says why:
* secret-types: --cubical-compatible waived; its receipt uses the pre-§8
wording (fixed by hyperpolymath/secret-types#32).
* Lintel: no receipt.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 32 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
|
|
Canon lockstep fails on The job compares
This PR does not touch the deed, so No fix exists yet. The fix is to bump the deed's Generated by Claude Code |
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
Summary
For owner ratification. ADR 0004 proposes the theorem-level claims registry slice. The atlas says that slice "requires a separately reviewed, source-anchored claims registry". The brief calls it Stage 1 (schema) and Stage 4 (proof-level indexing).
To ratify, merge with the ADR's Status changed to
Accepted (ratified by owner <date>). Until then the view says "proposed" on its face.The design rule comes straight from PROOF-POLICY §8.4–§8.5 and this repo's AUTHORITY.adoc: mathesis never assigns a grade. It pins each claim's home-repository receipt by commit and sha256, re-derives the Proof Witness Grade from what the receipt records, and fails CI if a receipt asserts a grade its evidence does not support.
Changes
docs/decisions/0004-claims-registry.adoc: the decision, the record contract, the derivation rules, alternatives considered, and the work that follows ratification.docs/registry/claims.json(I-JSON/JCS): source-anchored facts only.publicin the census inventory), the claim id, its kind (theorem, demonstration or assumption), the statement in the home repository's wording, the Agda module and names, a 40-character commit, and the receipt{path, sha256}.scripts/registry/claims-registry.mjs(Bun, beside the atlas): fetch, verify the digest, derive, render and check.RECONCILEDstate only, and never derivesPWG-1in this slice.docs/registry/registry.adoc: the generated view. It opens with a §8.4.7 census line: counts with their denominator, never a percentage.tests/registry/claims-registry.test.mjs, 7 tests and 31 assertions, hermetic via--receipts-dir.just registryandjust registry-check, and a CI step inproven-tests.ymlbeside the atlas.Pilot result: 0 of 12 theorems graded, with reasons
eee4e40. The receipt's flags lack--cubical-compatible(waiver W-1), and it uses the pre-§8grade-3wording. hyperpolymath/secret-types#32 fixes both. After it merges, bumping the pin should derivePWG-3.a0f2bae. It has no machine receipt yet. That is the first item after ratification.RSR Quality Checklist
Required
bun test tests/registry/claims-registry.test.mjs: 7 pass.bun scripts/registry/claims-registry.mjs checkpasses against the live receipts.check-ijson-jcs.sh --enforce docs/registry;check-adoc-renders.sh(178 files);check-invisible-characters.sh;check-no-md-in-docs.sh;check-root-shape.sh. I placed the data underdocs/registry/rather than adding a rootregistry/directory.As Applicable
docs/status/ROADMAP.adoc: not touched until ratification.Testing
The tests cover:
3,2iand2iibyRECONCILEDcount;BRIDGE-PENDINGandCOQ-CHECKEDdo not count;PWG-1is never derived;:pwgabove the evidence is drift, while a legacy:gradeis only a finding;%, and rendering is deterministic.Generated by Claude Code