census: partial refresh with provenance; reconciliation targets

.github/workflows/proven-tests.yml

@@ -49,6 +49,10 @@ jobs:
         run: |
           bun scripts/atlas/census-atlas.mjs check
           bun test tests/atlas/census-atlas.test.mjs
+      - name: Mathesis census merge tests and catalogue freshness
+        run: |
+          bash tests/census/merge-rows.test.sh
+          bash scripts/census/render-catalogue.sh docs/catalogue/census | diff -u docs/catalogue/catalogue.adoc -
       - name: Install verified Nickel 1.18.0 (K9 L2 semantics)
         run: |
           set -euo pipefail

CHANGELOG.adoc

@@ -8,6 +8,31 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== Added
+
+* Partial census refresh. `run-census.sh --merge FILE` (`just census-merge`)
+  censuses only the listed repositories and merges them into the committed
+  data with the new `scripts/census/merge-rows.sh`. Records outside the list
+  are kept byte for byte. `tests/census/merge-rows.test.sh` (`just
+  census-test`) covers replacement, removal, addition, scope filtering, order
+  preservation and seven fail-closed cases. A planted defect fails 6 of its 13
+  tests.
+* Census provenance. `census-repo.sh` records the commit it read, and every
+  run writes `docs/catalogue/census/provenance.json` (repository, commit,
+  UTC date).
+* CI runs the merge tests and the catalogue freshness check
+  (`proven-tests.yml`).
+
+==== Changed
+
+* Refreshed the census rows for 17 repositories named in AffineScript's
+  completion plan (2026-11-09, recorded in `provenance.json`). Eight rows
+  changed: choreographic-types, echo-types, epistemic-types, januskey,
+  occupancy-types, residual-evidence-types, secret-types and typed-wasm.
+  januskey's class moved from engineering to theory by the file-count
+  heuristic, not by review. aggregate-library, jtv-halting-islands-ct and
+  affinescript-libraries still have no row: they have no own proof files.
+
 ==== Fixed
 
 * `repo-init` minting a repository created with GitHub's "Use this

Justfile

@@ -720,6 +720,15 @@ uncloak:
 census:
     bash scripts/census/run-census.sh
 
+# Census only the repos listed in FILE (one OWNER/REPO per line) and merge the
+# result into the committed census; rows for every other repo are kept as is
+census-merge file:
+    bash scripts/census/run-census.sh --merge "{{file}}"
+
+# Test the census merge (positive and fail-closed cases)
+census-test:
+    bash tests/census/merge-rows.test.sh
+
 # Re-render docs/catalogue/catalogue.adoc from the committed census rows
 catalogue:
     bash scripts/census/render-catalogue.sh docs/catalogue/census > docs/catalogue/catalogue.adoc

README.adoc

@@ -56,6 +56,8 @@ organisation-specific working material belongs in separate protected repositorie
   (`docs/catalogue/census/template-paths.txt`) are boilerplate wherever they appear. The
   catalogue counts only a repo's *own* files.
 . *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.
+. *Refresh named repositories.* `just census-merge FILE` (`run-census.sh --merge FILE`) censuses only the repositories listed in FILE and merges the result with `merge-rows.sh`. Rows, unreachable entries and provenance change for those repositories only; every other record is kept byte for byte. `just census-test` runs its positive and fail-closed tests, which CI runs too.
+. *Record provenance.* `docs/catalogue/census/provenance.json` records, for each repository a run read, the exact commit and the UTC date. Rows from the 2026-10-26 first pass have no entry.
 
 == Reading the catalogue (first pass, 2026-10-26)
 
@@ -89,7 +91,7 @@ The first census covered 476 repositories:
   obligations with the status vocabulary of PROOF-POLICY §5.
 * Theorem-level rows for the theory repos: statement, Agda source, Rocq
   leg, Lean leg, route.
-* A scheduled CI job that reruns the census and fails on catalogue drift.
+* A scheduled CI job that reruns the census. (Catalogue drift against the committed rows already fails in CI.)
 * Reconcile the existing `mathesis_chora.deed` with the current estate conventions; it is already present, not a future placeholder.
 
 == Licence

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/generated/az.adoc

@@ -52,7 +52,7 @@
 * `metadatastician/cerro-torre` — engineering; 85 own proof files, 91 detected declarations; provers: idris2 8, spark 75, other 2
 * `hyperpolymath/chapeliser` — engineering; 9 own proof files, 136 detected declarations; provers: idris2 9
 * `hyperpolymath/checky-monkey` — engineering; 3 own proof files, 33 detected declarations; provers: idris2 3
-* `hyperpolymath/choreographic-types` — theory; 25 own proof files, 178 detected declarations; provers: agda 25
+* `hyperpolymath/choreographic-types` — theory; 34 own proof files, 214 detected declarations; provers: agda 34
 * `hyperpolymath/cicd-squabbler` — engineering; 3 own proof files, 0 detected declarations; provers: spark 2, other 1
 * `hyperpolymath/civic-connect` — engineering; 13 own proof files, 46 detected declarations; provers: idris2 4, spark 8, other 1
 * `metadatastician/cleave` — engineering; 12 own proof files, 38 detected declarations; provers: idris2 12
@@ -86,14 +86,14 @@
 
 * `hyperpolymath/echidna` — engineering; 167 own proof files, 1885 detected declarations; provers: agda 24, lean 17, rocq 9, isabelle 6, idris2 49, spark 18, smt-atp 31, why3 1, fstar 6, dafny 1, alloy 1, other 4
 * `hyperpolymath/echidnabot` — theory; 7 own proof files, 63 detected declarations; provers: lean 2, rocq 2, idris2 3
-* `hyperpolymath/echo-types` — theory; 148 own proof files, 1467 detected declarations; provers: agda 148
+* `hyperpolymath/echo-types` — theory; 161 own proof files, 1676 detected declarations; provers: agda 161
 * `hyperpolymath/eclexia` — theory; 11 own proof files, 218 detected declarations; provers: agda 1, rocq 6, idris2 4
 * `hyperpolymath/eclexiaiser` — engineering; 9 own proof files, 121 detected declarations; provers: idris2 9
 * `catachresis-colloquium/enaction-engine` — engineering; 6 own proof files, 95 detected declarations; provers: idris2 6
 * `catachresis-colloquium/enterglide-ncc-137-k` — engineering; 1 own proof files, 13 detected declarations; provers: idris2 1
 * `hyperpolymath/ephapax` — engineering; 43 own proof files, 635 detected declarations; provers: rocq 19, idris2 24
 * `hyperpolymath/ephapaxiser` — engineering; 9 own proof files, 133 detected declarations; provers: idris2 9
-* `hyperpolymath/epistemic-types` — theory; 37 own proof files, 320 detected declarations; provers: agda 37
+* `hyperpolymath/epistemic-types` — theory; 60 own proof files, 513 detected declarations; provers: agda 60
 * `hyperpolymath/error-lang` — engineering; 5 own proof files, 57 detected declarations; provers: idris2 5
 * `catachresis-colloquium/evil-weevil` — engineering; 4 own proof files, 124 detected declarations; provers: idris2 4
 * `hyperpolymath/ExactCounts.jl` — theory; 15 own proof files, 236 detected declarations; provers: agda 15
@@ -149,7 +149,7 @@
 
 == J
 
-* `hyperpolymath/januskey` — engineering; 11 own proof files, 142 detected declarations; provers: agda 3, idris2 8
+* `hyperpolymath/januskey` — theory; 17 own proof files, 193 detected declarations; provers: agda 9, idris2 8
 * `hyperpolymath/jtv-lang` — theory; 10 own proof files, 225 detected declarations; provers: lean 9, idris2 1
 * `hyperpolymath/julia-ecosystem` — engineering; 25 own proof files, 399 detected declarations; provers: idris2 25
 * `hyperpolymath/julia-professional-registry` — engineering; 4 own proof files, 18 detected declarations; provers: idris2 4
@@ -199,7 +199,7 @@
 
 * `hyperpolymath/oblibeniser` — engineering; 9 own proof files, 156 detected declarations; provers: idris2 9
 * `hyperpolymath/oblibeny` — engineering; 9 own proof files, 99 detected declarations; provers: idris2 9
-* `hyperpolymath/occupancy-types` — theory; 19 own proof files, 76 detected declarations; provers: agda 8, lean 5, idris2 6
+* `hyperpolymath/occupancy-types` — theory; 20 own proof files, 90 detected declarations; provers: agda 8, lean 6, idris2 6
 * `hyperpolymath/ochrance` — engineering; 48 own proof files, 404 detected declarations; provers: idris2 48
 * `hyperpolymath/ochrance-framework` — engineering; 14 own proof files, 123 detected declarations; provers: idris2 14
 * `hyperpolymath/odds-and-sods-package-manager` — engineering; 4 own proof files, 41 detected declarations; provers: idris2 4
@@ -243,7 +243,7 @@
 
 * `hyperpolymath/raze-tui` — engineering; 22 own proof files, 59 detected declarations; provers: idris2 3, spark 18, other 1
 * `hyperpolymath/reposystem` — engineering; 16 own proof files, 7 detected declarations; provers: idris2 1, spark 13, other 2
-* `hyperpolymath/residual-evidence-types` — theory; 27 own proof files, 328 detected declarations; provers: agda 27
+* `hyperpolymath/residual-evidence-types` — theory; 37 own proof files, 391 detected declarations; provers: agda 37
 * `hyperpolymath/ResidualEvidenceTypes.jl` — theory; 1 own proof files, 1 detected declarations; provers: agda 1
 * `hyperpolymath/resource-algebra` — theory; 22 own proof files, 271 detected declarations; provers: agda 22
 * `hyperpolymath/resource-record-fluctuator` — engineering; 32 own proof files, 0 detected declarations; provers: spark 31, other 1
@@ -252,7 +252,7 @@
 
 == S
 
-* `hyperpolymath/secret-types` — theory; 16 own proof files, 67 detected declarations; provers: agda 16
+* `hyperpolymath/secret-types` — theory; 21 own proof files, 91 detected declarations; provers: agda 21
 * `metadatastician/selur` — engineering; 2 own proof files, 23 detected declarations; provers: idris2 2
 * `hyperpolymath/session-sentinel` — engineering; 6 own proof files, 117 detected declarations; provers: idris2 6
 * `metadatastician/sim-public-relations` — engineering; 1 own proof files, 0 detected declarations; provers: idris2 1
@@ -281,7 +281,7 @@
 * `hyperpolymath/trigger` — engineering; 64 own proof files, 165 detected declarations; provers: agda 2, idris2 5, spark 56, other 1
 * `hyperpolymath/trope-checker` — theory; 37 own proof files, 492 detected declarations; provers: agda 10, lean 11, idris2 16
 * `hyperpolymath/tropical-types` — theory; 28 own proof files, 540 detected declarations; provers: lean 19, isabelle 9
-* `hyperpolymath/typed-wasm` — engineering; 46 own proof files, 850 detected declarations; provers: idris2 46
+* `hyperpolymath/typed-wasm` — engineering; 48 own proof files, 870 detected declarations; provers: idris2 48
 * `hyperpolymath/typedqliser` — engineering; 11 own proof files, 155 detected declarations; provers: idris2 11
 * `hyperpolymath/typell` — engineering; 6 own proof files, 159 detected declarations; provers: idris2 6
 

docs/atlas/generated/classes.adoc

@@ -11,19 +11,20 @@
 * `hyperpolymath/atoma` — theory; 21 own proof files, 127 detected declarations; provers: agda 4, idris2 3, smt-atp 14
 * `hyperpolymath/autoformal-fidelity` — theory; 4 own proof files, 7 detected declarations; provers: agda 4
 * `hyperpolymath/boinc-boinc` — theory; 8 own proof files, 46 detected declarations; provers: lean 8
-* `hyperpolymath/choreographic-types` — theory; 25 own proof files, 178 detected declarations; provers: agda 25
+* `hyperpolymath/choreographic-types` — theory; 34 own proof files, 214 detected declarations; provers: agda 34
 * `hyperpolymath/CompositionalCounts.jl` — theory; 10 own proof files, 184 detected declarations; provers: agda 10
 * `hyperpolymath/CompositionalDA.jl` — theory; 11 own proof files, 51 detected declarations; provers: agda 11
 * `hyperpolymath/echidnabot` — theory; 7 own proof files, 63 detected declarations; provers: lean 2, rocq 2, idris2 3
-* `hyperpolymath/echo-types` — theory; 148 own proof files, 1467 detected declarations; provers: agda 148
+* `hyperpolymath/echo-types` — theory; 161 own proof files, 1676 detected declarations; provers: agda 161
 * `hyperpolymath/eclexia` — theory; 11 own proof files, 218 detected declarations; provers: agda 1, rocq 6, idris2 4
-* `hyperpolymath/epistemic-types` — theory; 37 own proof files, 320 detected declarations; provers: agda 37
+* `hyperpolymath/epistemic-types` — theory; 60 own proof files, 513 detected declarations; provers: agda 60
 * `hyperpolymath/ExactCounts.jl` — theory; 15 own proof files, 236 detected declarations; provers: agda 15
 * `hyperpolymath/ExactTests.jl` — theory; 9 own proof files, 44 detected declarations; provers: agda 9
 * `hyperpolymath/firmboot` — theory; 38 own proof files, 409 detected declarations; provers: agda 19, lean 19
 * `hyperpolymath/gitbot-fleet` — theory; 7 own proof files, 63 detected declarations; provers: lean 2, rocq 2, idris2 3
 * `hyperpolymath/gnpl` — theory; 53 own proof files, 737 detected declarations; provers: lean 49, idris2 4
 * `hyperpolymath/invariant-path` — theory; 1 own proof files, 8 detected declarations; provers: agda 1
+* `hyperpolymath/januskey` — theory; 17 own proof files, 193 detected declarations; provers: agda 9, idris2 8
 * `hyperpolymath/jtv-lang` — theory; 10 own proof files, 225 detected declarations; provers: lean 9, idris2 1
 * `hyperpolymath/JuliaPackageSpitter.jl` — theory; 17 own proof files, 83 detected declarations; provers: agda 17
 * `hyperpolymath/kitchenspeak` — theory; 6 own proof files, 82 detected declarations; provers: agda 5, idris2 1
@@ -32,14 +33,14 @@
 * `hyperpolymath/my-lang` — theory; 25 own proof files, 617 detected declarations; provers: rocq 16, idris2 9
 * `hyperpolymath/neurophone` — theory; 6 own proof files, 19 detected declarations; provers: lean 3, tla 2, dafny 1
 * `hyperpolymath/nextgen-typing` — theory; 3 own proof files, 16 detected declarations; provers: agda 3
-* `hyperpolymath/occupancy-types` — theory; 19 own proof files, 76 detected declarations; provers: agda 8, lean 5, idris2 6
+* `hyperpolymath/occupancy-types` — theory; 20 own proof files, 90 detected declarations; provers: agda 8, lean 6, idris2 6
 * `hyperpolymath/palimpsest-license` — theory; 5 own proof files, 3 detected declarations; provers: agda 5
 * `hyperpolymath/phronesis` — theory; 12 own proof files, 140 detected declarations; provers: agda 3, lean 3, rocq 1, idris2 2, tla 3
 * `hyperpolymath/protocol-squisher` — theory; 42 own proof files, 365 detected declarations; provers: agda 10, lean 4, rocq 4, isabelle 2, idris2 12, tla 6, smt-atp 4
-* `hyperpolymath/residual-evidence-types` — theory; 27 own proof files, 328 detected declarations; provers: agda 27
+* `hyperpolymath/residual-evidence-types` — theory; 37 own proof files, 391 detected declarations; provers: agda 37
 * `hyperpolymath/ResidualEvidenceTypes.jl` — theory; 1 own proof files, 1 detected declarations; provers: agda 1
 * `hyperpolymath/resource-algebra` — theory; 22 own proof files, 271 detected declarations; provers: agda 22
-* `hyperpolymath/secret-types` — theory; 16 own proof files, 67 detected declarations; provers: agda 16
+* `hyperpolymath/secret-types` — theory; 21 own proof files, 91 detected declarations; provers: agda 21
 * `hyperpolymath/snifs` — theory; 3 own proof files, 43 detected declarations; provers: agda 2, idris2 1
 * `hyperpolymath/statistikles` — theory; 4 own proof files, 22 detected declarations; provers: agda 4
 * `hyperpolymath/system-et` — theory; 21 own proof files, 164 detected declarations; provers: lean 21
@@ -149,7 +150,6 @@
 * `hyperpolymath/intsoc-transactor` — engineering; 3 own proof files, 59 detected declarations; provers: idris2 3
 * `hyperpolymath/ipfs-overlay` — engineering; 5 own proof files, 17 detected declarations; provers: idris2 5
 * `hyperpolymath/iseriser` — engineering; 18 own proof files, 254 detected declarations; provers: idris2 18
-* `hyperpolymath/januskey` — engineering; 11 own proof files, 142 detected declarations; provers: agda 3, idris2 8
 * `hyperpolymath/julia-ecosystem` — engineering; 25 own proof files, 399 detected declarations; provers: idris2 25
 * `hyperpolymath/julia-professional-registry` — engineering; 4 own proof files, 18 detected declarations; provers: idris2 4
 * `hyperpolymath/julianiser` — engineering; 9 own proof files, 140 detected declarations; provers: idris2 9
@@ -208,7 +208,7 @@
 * `hyperpolymath/tlaiser` — engineering; 9 own proof files, 181 detected declarations; provers: idris2 9
 * `hyperpolymath/tree-navigator` — engineering; 16 own proof files, 0 detected declarations; provers: spark 15, other 1
 * `hyperpolymath/trigger` — engineering; 64 own proof files, 165 detected declarations; provers: agda 2, idris2 5, spark 56, other 1
-* `hyperpolymath/typed-wasm` — engineering; 46 own proof files, 850 detected declarations; provers: idris2 46
+* `hyperpolymath/typed-wasm` — engineering; 48 own proof files, 870 detected declarations; provers: idris2 48
 * `hyperpolymath/typedqliser` — engineering; 11 own proof files, 155 detected declarations; provers: idris2 11
 * `hyperpolymath/typell` — engineering; 6 own proof files, 159 detected declarations; provers: idris2 6
 * `hyperpolymath/ubicity` — engineering; 7 own proof files, 76 detected declarations; provers: idris2 7