refactor(atlas): move the census, claims and views under docs/atlas (WO 2.3)

.github/workflows/proven-tests.yml

@@ -69,7 +69,7 @@ jobs:
       - name: Mathesis census tests (offline fixtures) and catalogue currency
         run: |
           for t in tests/census/*.sh; do bash "$t"; done
-          bash scripts/census/render-catalogue.sh docs/catalogue/census | diff -u docs/catalogue/catalogue.adoc -
+          bash scripts/census/render-catalogue.sh docs/atlas/census | diff -u docs/atlas/generated/catalogue.adoc -
       # The claims registry (docs/decisions/0004-claims-registry.adoc): the canon
       # reader re-derives every grade from the home repositories' receipts at
       # their pinned commits (fetched, digest-checked). The check fails if the

.machine_readable/mint-verbatim.txt

@@ -34,4 +34,4 @@ tests/workflows/julia_library_test.sh      # PACKAGE_UUID brace-token fixture
 tests/workflows/resolve_template_pin_test.sh  # template-slug fixtures
 
 # Estate census is evidence, not generated template identity.
-docs/catalogue/census/repos.jsonl
+docs/atlas/census/repos.jsonl

Justfile

@@ -716,7 +716,7 @@ uncloak:
 
 # ── mathesis: estate maths catalogue ──────────────────────────────────────
 
-# Re-run the proof census over docs/catalogue/census/repos.jsonl and regenerate the
+# Re-run the proof census over docs/atlas/census/repos.jsonl and regenerate the
 # catalogue and the atlas built from the same rows (CI checks both, so a census
 # that refreshes one leaves the other stale)
 census:
@@ -730,19 +730,19 @@ update-rows +repos:
 
 # Re-list every blob the RSR template has shipped at its template paths, in any commit
 template-blobs:
-    bash scripts/census/template-blobs.sh docs/catalogue/census/template-paths.txt > docs/catalogue/census/template-blobs.tsv
+    bash scripts/census/template-blobs.sh docs/atlas/census/template-paths.txt > docs/atlas/census/template-blobs.tsv
 
 # Offline census tests: row folding, status documents, template blobs, scanner, Rust proofs
 census-test:
     for t in tests/census/*.sh; do bash "$t" || exit 1; done
 
-# Re-render docs/catalogue/catalogue.adoc from the committed census rows
+# Re-render docs/atlas/generated/catalogue.adoc from the committed census rows
 catalogue:
-    bash scripts/census/render-catalogue.sh docs/catalogue/census > docs/catalogue/catalogue.adoc
+    bash scripts/census/render-catalogue.sh docs/atlas/census > docs/atlas/generated/catalogue.adoc
 
 # Fail if the committed catalogue does not match the committed census rows
 catalogue-check:
-    bash scripts/census/render-catalogue.sh docs/catalogue/census | diff -u docs/catalogue/catalogue.adoc -
+    bash scripts/census/render-catalogue.sh docs/atlas/census | diff -u docs/atlas/generated/catalogue.adoc -
 
 # Mathesis read-only census discovery views and agent retrieval
 atlas-build:
@@ -757,7 +757,7 @@ 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 with the canon reader, and write docs/registry/registry.adoc.
+# Proof Witness Grades with the canon reader, and write docs/atlas/generated/registry.adoc.
 # Needs MATHESIS_STANDARDS: a metadatastician/standards checkout at the reader pin
 # (READER in scripts/registry/claims-registry.mjs).
 registry:

README.adoc

@@ -19,7 +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; accepted in link:docs/decisions/0004-claims-registry.adoc[ADR 0004]; the canon reader of PROOF-POLICY §8.5.1 derives each grade.
+* link:docs/atlas/generated/registry.adoc[Claims registry, pilot slice]: theorem-level, grades *derived* from home-repository receipts at pinned commits; accepted in link:docs/decisions/0004-claims-registry.adoc[ADR 0004]; the canon reader of PROOF-POLICY §8.5.1 derives each grade.
 * 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/proposals/proof-receipts-as-data.adoc[Proof receipts as data] — proposed, not adopted: machine-readable proof ledgers and CI receipts in home repositories, so Mathesis can derive Proof Witness Grades instead of transcribing them.
 * link:docs/architecture/REPOSITORY-MAP.adoc[Generated repository map] — current path inventory, not the mathematical architecture specification.
@@ -35,15 +35,15 @@ organisation-specific working material belongs in separate protected repositorie
 
 [cols="1,3"]
 |===
-|`docs/catalogue/catalogue.adoc` |The catalogue: one row per repository with proof files of its own, split into theory and engineering. Generated; do not edit by hand.
-|`docs/catalogue/census/` |What the catalogue is rendered from: `catalogue-rows.jsonl` (one row of counts per repository, no file paths), `repos.jsonl` (the census input), `unreachable.jsonl`, `template-paths.txt` and `forks-with-own-proofs.txt`. Each `.jsonl` file is JSON Lines: one I-JSON/JCS record on each line, so a change to one row changes one line. Each row also names `commit`, the commit that the census read, and `censused_at`, the UTC time it read it.
+|`docs/atlas/generated/catalogue.adoc` |The catalogue: one row per repository with proof files of its own, split into theory and engineering. Generated; do not edit by hand.
+|`docs/atlas/census/` |What the catalogue is rendered from: `rows.jsonl` (one row of counts per repository, no file paths), `repos.jsonl` (the census input), `unreachable.jsonl`, `template-paths.txt` and `forks-with-own-proofs.txt`. Each `.jsonl` file is JSON Lines: one I-JSON/JCS record on each line, so a change to one row changes one line. Each row also names `commit`, the commit that the census read, and `censused_at`, the UTC time it read it.
 |`scripts/census/` |`run-census.sh` (whole census), `update-rows.sh` (refresh named repositories' rows only), `census-repo.sh` (one repo), `summarise.sh`, `build-rows.sh` (raw census to rows), `render-catalogue.sh` (rows to catalogue), and proof-craft's `proof-holes.sh`.
 |`Justfile` |`just census`, `just catalogue`, `just catalogue-check` (the committed catalogue matches the committed data).
 |===
 
 == How the census works
 
-. *List repositories.* `docs/catalogue/census/repos.jsonl` is the input. Agent sessions build
+. *List repositories.* `docs/atlas/census/repos.jsonl` is the input. Agent sessions build
   it with the Claude Code remote `list_repos` tool, because the GitHub API is
   not reachable from them.
 . *List proof files cheaply.* Each repository is cloned blobless with
@@ -55,12 +55,12 @@ organisation-specific working material belongs in separate protected repositorie
   inventories holes, axioms, disabled checkers and policy breaches
   (`holes.jsonl`).
 . *Set the template aside.* Files the RSR template ships
-  (`docs/catalogue/census/template-paths.txt`) are boilerplate wherever they appear. The
+  (`docs/atlas/census/template-paths.txt`) are boilerplate wherever they appear. The
   catalogue counts only a repo's *own* files.
 . *Skip forks, unless their proofs are first-party.* A fork normally carries
   someone else's work, so the census leaves forks out. A fork whose proof
   files are the owner's own is named in
-  `docs/catalogue/census/forks-with-own-proofs.txt`, with its reason, and is
+  `docs/atlas/census/forks-with-own-proofs.txt`, with its reason, and is
   censused like any other repository.
 . *Keep rows, not paths.* The raw, path-level census (clones, every proof file, every declaration, every hole finding, and a `summary.md`) goes to a scratch directory (`MATHESIS_WORK`) and is not committed. `build-rows.sh` folds it into one row of counts per repository, and only those rows are committed, so the data stays small and does not repeat other repositories' file paths.
 
@@ -75,7 +75,7 @@ The first census covered 476 repositories:
   the end of the catalogue, among them `cut-calculus`.
 * *Possibly missing:* the listing returned only repositories pushed since
   2026-09-15, so older, untouched repos may be absent. Add them to
-  `docs/catalogue/census/repos.jsonl` and rerun.
+  `docs/atlas/census/repos.jsonl` and rerun.
 * *Theory or engineering* is a heuristic: more Agda, Lean, Rocq or Isabelle
   files than Idris2 or SPARK files reads as theory. Confirm each row against
   PROOF-POLICY.

docs/architecture.adoc

@@ -10,13 +10,13 @@ Mathesis is the estate's mathematical source-discovery and proof-orientation ind
 
 [source,text]
 ----
-Repository census input (docs/catalogue/census/repos.jsonl)
+Repository census input (docs/atlas/census/repos.jsonl)
   -> scripts/census/ (source and prover-file discovery)
   -> corpus counts, holes/unsafe candidates, reachability observations
-  -> docs/catalogue/census/catalogue-rows.jsonl
-  -> generated docs/catalogue/catalogue.adoc
+  -> docs/atlas/census/rows.jsonl
+  -> generated docs/atlas/generated/catalogue.adoc
   -> scripts/atlas/census-atlas.mjs
-  -> docs/atlas/generated/ (A-Z, class, owner; index.json)
+  -> docs/atlas/generated/ (catalogue, A-Z, owner, registry; index.json)
   -> lookup and bounded context-pack commands
 ----
 
@@ -35,7 +35,7 @@ The census counts and classifies observed files. It does not establish that Agda
 | Home mathematical repository at a concrete revision, with actual proof-checker outputs and assumptions
 
 | Census and derived atlas views
-| link:catalogue/catalogue.adoc[Mathesis census] and link:atlas/README.adoc[atlas declaration of scope]
+| link:atlas/generated/catalogue.adoc[Mathesis census] and link:atlas/README.adoc[atlas declaration of scope]
 
 | General test evidence and fixture requirements
 | https://github.com/hyperpolymath/proven-tests-and-benches[proven-tests-and-benches] and the canonical estate testing policy

docs/atlas/README.adoc

@@ -3,14 +3,13 @@
 
 This is a *generated, read-only directory of proof-source repositories*, not yet a
 complete alphabetic mathematical concept atlas. It derives from
-`docs/catalogue/census/catalogue-rows.jsonl` and never alters
+`docs/atlas/census/rows.jsonl` and never alters
 or reclassifies the source census. Each row names the commit that the census read
 (`commit`) and the time it read it (`censused_at`, UTC), so each count has a
 source. A–Z means repository-name order, not a claim
 that these are all the mathematical concepts relevant to the estate.
 
-The first views are A–Z repositories, theory-versus-engineering census class,
-and owner/organisation grouping. `index.json` is machine-readable. The CLI
+The views are the catalogue (split by census class), A–Z repositories, owner/organisation grouping and the claims registry. The separate class view was removed on 2026-11-10 (WO 2.3): it repeated the catalogue with fewer columns. `index.json` is machine-readable. The CLI
 supports source discovery and a bounded context pack suitable for agents.
 
 Run with Bun: `bun scripts/atlas/census-atlas.mjs build`, `check`,
@@ -22,15 +21,15 @@ summarised rows, so this atlas must not invent per-theorem names, evidence,
 proof status, assumptions, equivalence, or independent verification.
 The next slice is a separately reviewed, source-anchored claims registry,
 accepted in link:../decisions/0004-claims-registry.adoc[ADR 0004]
-(pilot view: link:../registry/registry.adoc[`docs/registry/registry.adoc`]).
+(pilot view: link:generated/registry.adoc[`docs/atlas/generated/registry.adoc`]).
 No private-source records are added or published by this generator.
 
 == One writer for census data
 
 Census rows change in one way only: `just census` (the whole frame) or
 `just update-rows OWNER/REPO...` (named repositories). Both rebuild the
 catalogue and this atlas from the same rows. Nobody edits
-`catalogue-rows.jsonl`, `unreachable.jsonl` or the generated views by hand.
+`rows.jsonl`, `unreachable.jsonl` or the generated views by hand.
 Only one pull request that changes rows is open at a time; record it under
 "Open census work" in link:../status/ROADMAP.adoc[`ROADMAP.adoc`] before it
 opens. The deed states the same rule in `(bot-directives (census-writer))`.