feat(census): refresh named rows, and re-take five stale ones

.gitignore

@@ -144,3 +144,7 @@ verification/proofs/coq/.*.aux
 # Agda compiled proof artifacts
 verification/proofs/agda/*.agdai
 
+
+# Census publication lock and interrupted staging snapshots
+/docs/.catalogue.lock
+/docs/.catalogue-stage.*/

Justfile

@@ -720,13 +720,17 @@ uncloak:
 census:
     bash scripts/census/run-census.sh
 
+# Re-census only the named repositories (OWNER/REPO ...) and splice their rows in
+census-refresh +repos:
+    bash scripts/census/refresh-rows.sh {{repos}}
+
 # 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
+    bash scripts/census/check-catalogue.sh --write
 
 # 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/check-catalogue.sh
 
 # Mathesis read-only census discovery views and agent retrieval
 atlas-build:

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
@@ -193,16 +197,14 @@ predecessors did.
 
 == Declared structure not yet filled
 
-These directories currently hold only a stub `README.adoc` and a level
-manifest. That is deliberate. They declare the shape a repository minted
+These directories currently hold only a stub `README.adoc` or `.gitkeep`.
+That is deliberate. They declare the shape a repository minted
 from this template is expected to grow into; they are *intended
 structure, not abandoned work*. Add content, or delete the directory in
 your own repo - but do not read their emptiness as neglect here.
 
 [cols="1"]
 |===
-| `.machine_readable/bot_directives/`
-| `.machine_readable/descriptiles/anchors/`
 | `.machine_readable/scripts/verification/`
 | `docs/governance/audit/`
 | `docs/governance/audit/compliance/`
@@ -228,14 +230,9 @@ your own repo - but do not read their emptiness as neglect here.
 | `docs/theory/ontologies/`
 | `docs/theory/other/`
 | `docs/theory/socio-technical/`
-| `docs/whitepapers/`
 | `docs/whitepapers/academic/`
 | `docs/whitepapers/industry/`
-| `docs/whitepapers/outreach/`
 | `examples/`
-| `features/boj-server/`
-| `features/panic-attacker/`
-| `src/aspects/`
 | `src/aspects/integrity/`
 | `src/aspects/observability/`
 | `src/aspects/security/`
@@ -246,7 +243,6 @@ your own repo - but do not read their emptiness as neglect here.
 | `src/errors/`
 | `src/interface/generated/`
 | `src/interface/generated/abi/`
-| `tests/fuzz/`
 | `verification/benchmarks/`
 | `verification/coverage/`
 | `verification/fuzzing/`

docs/atlas/generated/az.adoc

@@ -84,9 +84,9 @@
 
 == E
 
-* `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/echidna` — engineering; 170 own proof files, 1945 detected declarations; provers: agda 27, 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; 12 own proof files, 82 detected declarations; provers: agda 2, lean 4, rocq 3, idris2 3
+* `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
@@ -203,6 +203,7 @@
 * `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
+* `hyperpolymath/ordinal-notation` — theory; 78 own proof files, 618 detected declarations; provers: agda 78
 * `hyperpolymath/otpiser` — engineering; 9 own proof files, 157 detected declarations; provers: idris2 9
 
 == P
@@ -228,6 +229,7 @@
 * `hyperpolymath/presswerk` — engineering; 6 own proof files, 76 detected declarations; provers: idris2 6
 * `metadatastician/proglanging-languages` — engineering; 1 own proof files, 1 detected declarations; provers: idris2 1
 * `catachresis-colloquium/project-ovine` — engineering; 1 own proof files, 0 detected declarations; provers: idris2 1
+* `hyperpolymath/proof-burrower` — theory; 2 own proof files, 31 detected declarations; provers: agda 2
 * `catachresis-colloquium/proof-of-work` — engineering; 4 own proof files, 46 detected declarations; provers: idris2 4
 * `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/proven` — engineering; 967 own proof files, 11166 detected declarations; provers: lean 14, idris2 906, spark 42, tla 1, other 4

docs/atlas/generated/classes.adoc

@@ -14,8 +14,8 @@
 * `hyperpolymath/choreographic-types` — theory; 25 own proof files, 178 detected declarations; provers: agda 25
 * `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/echidnabot` — theory; 12 own proof files, 82 detected declarations; provers: agda 2, lean 4, rocq 3, idris2 3
+* `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/ExactCounts.jl` — theory; 15 own proof files, 236 detected declarations; provers: agda 15
@@ -33,8 +33,10 @@
 * `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/ordinal-notation` — theory; 78 own proof files, 618 detected declarations; provers: agda 78
 * `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/proof-burrower` — theory; 2 own proof files, 31 detected declarations; provers: agda 2
 * `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/ResidualEvidenceTypes.jl` — theory; 1 own proof files, 1 detected declarations; provers: agda 1
@@ -119,7 +121,7 @@
 * `hyperpolymath/dictask` — engineering; 1 own proof files, 17 detected declarations; provers: idris2 1
 * `hyperpolymath/docmatrix` — engineering; 11 own proof files, 0 detected declarations; provers: spark 10, other 1
 * `hyperpolymath/docudactyl` — engineering; 13 own proof files, 223 detected declarations; provers: idris2 7, spark 5, other 1
-* `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/echidna` — engineering; 170 own proof files, 1945 detected declarations; provers: agda 27, lean 17, rocq 9, isabelle 6, idris2 49, spark 18, smt-atp 31, why3 1, fstar 6, dafny 1, alloy 1, other 4
 * `hyperpolymath/eclexiaiser` — engineering; 9 own proof files, 121 detected declarations; provers: idris2 9
 * `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

docs/atlas/generated/organisations.adoc

@@ -79,9 +79,9 @@
 * `hyperpolymath/dictask` — engineering; 1 own proof files, 17 detected declarations; provers: idris2 1
 * `hyperpolymath/docmatrix` — engineering; 11 own proof files, 0 detected declarations; provers: spark 10, other 1
 * `hyperpolymath/docudactyl` — engineering; 13 own proof files, 223 detected declarations; provers: idris2 7, spark 5, other 1
-* `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/echidna` — engineering; 170 own proof files, 1945 detected declarations; provers: agda 27, 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; 12 own proof files, 82 detected declarations; provers: agda 2, lean 4, rocq 3, idris2 3
+* `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
 * `hyperpolymath/ephapax` — engineering; 43 own proof files, 635 detected declarations; provers: rocq 19, idris2 24
@@ -154,6 +154,7 @@
 * `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
+* `hyperpolymath/ordinal-notation` — theory; 78 own proof files, 618 detected declarations; provers: agda 78
 * `hyperpolymath/otpiser` — engineering; 9 own proof files, 157 detected declarations; provers: idris2 9
 * `hyperpolymath/palimpsest-license` — theory; 5 own proof files, 3 detected declarations; provers: agda 5
 * `hyperpolymath/panic-attack` — engineering; 6 own proof files, 46 detected declarations; provers: idris2 6
@@ -169,6 +170,7 @@
 * `hyperpolymath/polyglot-i18n` — engineering; 11 own proof files, 0 detected declarations; provers: spark 10, other 1
 * `hyperpolymath/ponyiser` — engineering; 9 own proof files, 137 detected declarations; provers: idris2 9
 * `hyperpolymath/presswerk` — engineering; 6 own proof files, 76 detected declarations; provers: idris2 6
+* `hyperpolymath/proof-burrower` — theory; 2 own proof files, 31 detected declarations; provers: agda 2
 * `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/proven` — engineering; 967 own proof files, 11166 detected declarations; provers: lean 14, idris2 906, spark 42, tla 1, other 4
 * `hyperpolymath/proven-servers` — engineering; 1097 own proof files, 6242 detected declarations; provers: idris2 899, spark 197, other 1

docs/catalogue/catalogue.adoc

@@ -20,7 +20,9 @@ verdicts.
 |===
 |Repository |Own files |Fixtures |Provers (files) |Declarations |Holes |Axioms |Unsafe |Policy |Proof-status doc
 
-|https://github.com/hyperpolymath/echo-types[hyperpolymath/echo-types] |148 |0 |agda 148 |1467 |0 |1 |0 |1 |`PROOF-STATUS.adoc`
+|https://github.com/hyperpolymath/echo-types[hyperpolymath/echo-types] |161 |0 |agda 161 |1676 |0 |1 |0 |1 |`PROOF-STATUS.adoc`
+
+|https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation] |78 |0 |agda 78 |618 |0 |2 |0 |1 |`docs/status/PROOF-NEEDS.adoc`
 
 |https://github.com/hyperpolymath/valence-shell[hyperpolymath/valence-shell] |64 |0 |agda 10, lean 16, rocq 12, isabelle 9, idris2 12, smt-atp 5 |960 |5 |1 |0 |9 |`PROOF-NEEDS.adoc`
 
@@ -72,6 +74,8 @@ verdicts.
 
 |https://github.com/metadatastician/MetaManifold-Evidence[metadatastician/MetaManifold-Evidence] |13 |0 |agda 13 |70 |0 |0 |0 |0 |—
 
+|https://github.com/hyperpolymath/echidnabot[hyperpolymath/echidnabot] |12 |0 |agda 2, lean 4, rocq 3, idris2 3 |82 |6 |0 |0 |0 |`docs/PROOF-STATUS.adoc`
+
 |https://github.com/hyperpolymath/phronesis[hyperpolymath/phronesis] |12 |0 |agda 3, lean 3, rocq 1, idris2 2, tla 3 |140 |3 |0 |0 |2 |—
 
 |https://github.com/hyperpolymath/CompositionalDA.jl[hyperpolymath/CompositionalDA.jl] |11 |0 |agda 11 |51 |0 |1 |0 |0 |`proofs/PROOF-STATUS.md`
@@ -88,8 +92,6 @@ verdicts.
 
 |https://github.com/hyperpolymath/boinc-boinc[hyperpolymath/boinc-boinc] |8 |0 |lean 8 |46 |1 |0 |0 |0 |`PROOF-NEEDS.adoc`
 
-|https://github.com/hyperpolymath/echidnabot[hyperpolymath/echidnabot] |7 |0 |lean 2, rocq 2, idris2 3 |63 |6 |0 |0 |0 |`docs/proof-debt.adoc`
-
 |https://github.com/hyperpolymath/gitbot-fleet[hyperpolymath/gitbot-fleet] |7 |0 |lean 2, rocq 2, idris2 3 |63 |6 |0 |0 |0 |`PROOF-NEEDS.adoc`
 
 |https://github.com/hyperpolymath/kitchenspeak[hyperpolymath/kitchenspeak] |6 |0 |agda 5, idris2 1 |82 |0 |4 |0 |1 |`docs/proof-debt.adoc`
@@ -114,6 +116,8 @@ verdicts.
 
 |https://github.com/metadatastician/ZenodoDeposits.jl[metadatastician/ZenodoDeposits.jl] |3 |0 |agda 3 |53 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
 
+|https://github.com/hyperpolymath/proof-burrower[hyperpolymath/proof-burrower] |2 |0 |agda 2 |31 |0 |0 |0 |0 |`docs/proof-debt.adoc`
+
 |https://github.com/hyperpolymath/ResidualEvidenceTypes.jl[hyperpolymath/ResidualEvidenceTypes.jl] |1 |1 |agda 1 |1 |0 |0 |0 |0 |—
 
 |https://github.com/hyperpolymath/invariant-path[hyperpolymath/invariant-path] |1 |0 |agda 1 |8 |0 |0 |0 |0 |—
@@ -137,7 +141,7 @@ verdicts.
 
 |https://github.com/hyperpolymath/boj-server-cartridges[hyperpolymath/boj-server-cartridges] |184 |0 |idris2 184 |1500 |0 |0 |0 |0 |—
 
-|https://github.com/hyperpolymath/echidna[hyperpolymath/echidna] |167 |21 |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 |1885 |4 |1 |4 |23 |`docs/PROOF-NEEDS.adoc`
+|https://github.com/hyperpolymath/echidna[hyperpolymath/echidna] |170 |21 |agda 27, lean 17, rocq 9, isabelle 6, idris2 49, spark 18, smt-atp 31, why3 1, fstar 6, dafny 1, alloy 1, other 4 |1945 |4 |1 |4 |26 |`docs/PROOF-NEEDS.adoc`
 
 |https://github.com/hyperpolymath/ambientops[hyperpolymath/ambientops] |102 |1 |idris2 39, spark 58, other 5 |777 |39 |0 |8 |0 |`PROOF-NEEDS.adoc`
 
@@ -548,3 +552,14 @@ session):
 * hyperpolymath/tools
 * hyperpolymath/typefix-zero
 * hyperpolymath/vex-tools
+
+== Refreshed since the full census
+
+These rows were re-taken by `scripts/census/refresh-rows.sh` after the last
+full census, so they are newer than every other row:
+
+* `hyperpolymath/echidna`, 2026-11-09, commit `2ab7574ae1e5`
+* `hyperpolymath/echidnabot`, 2026-11-09, commit `1443adfabb98`
+* `hyperpolymath/echo-types`, 2026-11-09, commit `ccec4d79866e`
+* `hyperpolymath/ordinal-notation`, 2026-11-09, commit `53ff6255e848`
+* `hyperpolymath/proof-burrower`, 2026-11-09, commit `7a5ab74e0d47`

docs/catalogue/census/refreshed.json

@@ -0,0 +1 @@
+[{"commit":"2ab7574ae1e574b0e881422fde6252bf79dea178","refreshed":"2026-11-09","repo":"hyperpolymath/echidna"},{"commit":"1443adfabb98a9e0daea562bc8dbe764442c14cc","refreshed":"2026-11-09","repo":"hyperpolymath/echidnabot"},{"commit":"ccec4d79866e3e433ae2268d2f8b7899396cb34f","refreshed":"2026-11-09","repo":"hyperpolymath/echo-types"},{"commit":"53ff6255e848a364d50fa6dc4687786e389b4740","refreshed":"2026-11-09","repo":"hyperpolymath/ordinal-notation"},{"commit":"7a5ab74e0d47e3b2131bf4273922b6744779c15e","refreshed":"2026-11-09","repo":"hyperpolymath/proof-burrower"}]

scripts/census/census-repo.sh

@@ -23,6 +23,10 @@ if [ $rc -ne 0 ]; then
 fi
 
 git -C "$D" ls-tree -r --name-only HEAD > "$O.tree" 2>/dev/null || true
+if ! head=$(git -C "$D" rev-parse HEAD 2>/dev/null); then
+  head=unavailable
+fi
+printf '%s\n' "$head" > "$O.head"
 if ! [ -s "$O.tree" ]; then rm -rf "$D" "$O.tree"; exit 0; fi
 
 # proof-status docs

scripts/census/check-catalogue.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+set -euo pipefail
+here=$(cd "$(dirname "$0")" && pwd)
+source "$here/snapshot.sh"
+snapshot_lock
+if [ "${1:-}" = --write ]; then
+  snapshot_stage
+  snapshot_publish
+  exit
+fi
+bash "$here/render-catalogue.sh" --staged "$catalogue/census" | diff -u "$catalogue/catalogue.adoc" -