census: prefer PROOF-STATUS ledgers; refresh echidnabot and hypatia; record the echidna proof route

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

@@ -85,7 +85,7 @@
 == 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/echidnabot` — theory; 12 own proof files, 82 detected declarations; provers: agda 2, lean 4, rocq 3, idris2 3
 * `hyperpolymath/echo-types` — theory; 148 own proof files, 1467 detected declarations; provers: agda 148
 * `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
@@ -133,7 +133,7 @@
 * `hyperpolymath/http-capability-gateway` — engineering; 5 own proof files, 59 detected declarations; provers: idris2 5
 * `metadatastician/hvn-dehallucinator` — theory; 9 own proof files, 108 detected declarations; provers: agda 5, idris2 1, tla 3
 * `hyperpolymath/hybrid-automation-router` — engineering; 5 own proof files, 66 detected declarations; provers: idris2 5
-* `hyperpolymath/hypatia` — engineering; 42 own proof files, 448 detected declarations; provers: agda 1, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1
+* `hyperpolymath/hypatia` — engineering; 43 own proof files, 480 detected declarations; provers: agda 2, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1
 
 == I
 

docs/atlas/generated/classes.adoc

@@ -14,7 +14,7 @@
 * `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/echidnabot` — theory; 12 own proof files, 82 detected declarations; provers: agda 2, lean 4, rocq 3, idris2 3
 * `hyperpolymath/echo-types` — theory; 148 own proof files, 1467 detected declarations; provers: agda 148
 * `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
@@ -142,7 +142,7 @@
 * `hyperpolymath/hpm-json-rsr` — engineering; 3 own proof files, 26 detected declarations; provers: idris2 3
 * `hyperpolymath/http-capability-gateway` — engineering; 5 own proof files, 59 detected declarations; provers: idris2 5
 * `hyperpolymath/hybrid-automation-router` — engineering; 5 own proof files, 66 detected declarations; provers: idris2 5
-* `hyperpolymath/hypatia` — engineering; 42 own proof files, 448 detected declarations; provers: agda 1, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1
+* `hyperpolymath/hypatia` — engineering; 43 own proof files, 480 detected declarations; provers: agda 2, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1
 * `hyperpolymath/i-human` — engineering; 3 own proof files, 47 detected declarations; provers: idris2 3
 * `hyperpolymath/ideas-to-alphas` — engineering; 4 own proof files, 77 detected declarations; provers: idris2 4
 * `hyperpolymath/idrisiser` — engineering; 9 own proof files, 122 detected declarations; provers: idris2 9

docs/atlas/generated/organisations.adoc

@@ -80,7 +80,7 @@
 * `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/echidnabot` — theory; 12 own proof files, 82 detected declarations; provers: agda 2, lean 4, rocq 3, idris2 3
 * `hyperpolymath/echo-types` — theory; 148 own proof files, 1467 detected declarations; provers: agda 148
 * `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
@@ -111,7 +111,7 @@
 * `hyperpolymath/hpm-json-rsr` — engineering; 3 own proof files, 26 detected declarations; provers: idris2 3
 * `hyperpolymath/http-capability-gateway` — engineering; 5 own proof files, 59 detected declarations; provers: idris2 5
 * `hyperpolymath/hybrid-automation-router` — engineering; 5 own proof files, 66 detected declarations; provers: idris2 5
-* `hyperpolymath/hypatia` — engineering; 42 own proof files, 448 detected declarations; provers: agda 1, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1
+* `hyperpolymath/hypatia` — engineering; 43 own proof files, 480 detected declarations; provers: agda 2, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1
 * `hyperpolymath/i-human` — engineering; 3 own proof files, 47 detected declarations; provers: idris2 3
 * `hyperpolymath/ideas-to-alphas` — engineering; 4 own proof files, 77 detected declarations; provers: idris2 4
 * `hyperpolymath/idrisiser` — engineering; 9 own proof files, 122 detected declarations; provers: idris2 9

docs/catalogue/catalogue.adoc

@@ -72,6 +72,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 +90,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`
@@ -157,7 +157,7 @@ verdicts.
 
 |https://github.com/hyperpolymath/ephapax[hyperpolymath/ephapax] |43 |0 |rocq 19, idris2 24 |635 |15 |0 |1 |0 |`PROOF-NEEDS.adoc`
 
-|https://github.com/hyperpolymath/hypatia[hyperpolymath/hypatia] |42 |11 |agda 1, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1 |448 |3 |1 |0 |1 |`docs/proof-debt.adoc`
+|https://github.com/hyperpolymath/hypatia[hyperpolymath/hypatia] |43 |11 |agda 2, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1 |480 |3 |1 |0 |1 |`verification/PROOF-STATUS.adoc`
 
 |https://github.com/hyperpolymath/vexometer[hyperpolymath/vexometer] |42 |6 |idris2 10, spark 29, other 3 |104 |3 |0 |0 |0 |`PROOF-NEEDS.adoc`
 

docs/reports/audit/echidna-proof-route-2026-11-09.adoc

@@ -0,0 +1,101 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= The echidna proof route: theorems, receipts and grades (2026-11-09)
+:toc:
+
+This is a dated, source-anchored record of the proofs the echidna proof route
+rests on. It is *not* a claims registry: the atlas README leaves that design
+open. Each theorem lives in its home repository, which owns its statement,
+receipts and status (PROOF-POLICY §2.2, §8.5). This page points at them. The
+Proof Witness Grades (PWG) below are derived from those receipts, not
+assigned here.
+
+An agent drafted this record and the statement comparison it cites. Neither
+has been reviewed by the owner yet, so neither counts as independent
+corroboration.
+
+The plan these rows come from is
+https://github.com/metadatastician/standards/blob/main/docs/ULTRAPLAN-ECHIDNA-PROOF-ROUTE-2026-11-04.adoc[the echidna proof-route ultraplan]
+(ladder rows in brackets; v0.2.4 is metadatastician/standards#1434).
+
+== Theory theorems
+
+Census: 4 theory theorems in this route. `PWG-1`: 0. `PWG-2ii`: 0.
+`PWG-2i`: 0. `PWG-3`: 1. `ungraded`: 3, all planned with no Agda source yet.
+
+[cols="2,2,3,2,3",options="header"]
+|===
+|Theorem |Home |Legs: §5 token, §2.2 state |Derived PWG |Receipts
+
+|Receipt boundary, T-RECEIPT: a warrant token does not give its claim
+without a soundness map; no unconditional reflection exists (feeds rows 4-5)
+|hyperpolymath/echidnabot, `docs/PROOF-STATUS.adoc`
+|Agda `proven`. Lean `proven`, re-proved, `BRIDGE-PENDING`. Rocq `proven`,
+re-proved, `BRIDGE-PENDING`. No axioms in any leg.
+|`PWG-3`. It would become `PWG-2ii` once the drafted statement comparison is
+reviewed and both legs are `RECONCILED`.
+|Agda 2.8.0.2 (§2.1 profile), Lean 4.35.0, Coq 8.18.0, at echidnabot
+`1443adfabb98a9e0daea562bc8dbe764442c14cc`; agent session. The per-commit
+CI job is hyperpolymath/echidnabot#195.
+
+|Token order and weakest-step meet; level monotonicity (row 2)
+|hyperpolymath/mathesis (owner ruling D-10, 2026-11-09); no Agda source yet
+|`open`
+|`ungraded`
+|None
+
+|Retraction never raises a level; name-wise retraction kills exactly its
+dependents (row 7)
+|hyperpolymath/residual-evidence-types (Agda source of `Revision.agda`)
+|`open` for the stated theorem
+|`ungraded`
+|None for this statement. The Idris2 transcription is below.
+
+|Status fold is a join on the token lattice (row 12)
+|hyperpolymath/mathesis (owner ruling D-10, 2026-11-09); no Agda source yet
+|`open`
+|`ungraded`
+|None
+|===
+
+== Engineering proofs (not graded, PROOF-POLICY §8.1)
+
+[cols="2,2,2,3",options="header"]
+|===
+|Proof |Home |Token |Receipt
+
+|`Verdict.idr`: `Sound` only from a confirming prover re-check; level
+"sound" only with a witness
+|hyperpolymath/hypatia, `verification/PROOF-STATUS.adoc`
+|`proven` (Idris2); correspondence with epistemic-types `Warrant.agda` is
+`argued`
+|Idris2 v0.7.0, `verify-proofs.yml` run 42559874988 at
+`c639c465e9bbbd01522f1eae12ac98a071afac13`, with accept and reject fixtures
+
+|`Retraction.idr`: retraction as a thinning; a finding survives through a
+token
+|hyperpolymath/hypatia
+|`proven` (Idris2); correspondence with residual-evidence-types is `argued`.
+It retracts one occurrence by position, while the runtime retracts by name
+(ladder row 7).
+|Same run
+
+|echidnabot GraphQL gate, E-AUTH-SCOPE, E-AUTH-ROLE, E-AUTH-GUARD,
+E-RATE-BOUND (row 15)
+|hyperpolymath/echidnabot, `docs/PROOF-STATUS.adoc`
+|`open` under Creusot/Pearlite and Verus (§1.2)
+|Tests only, which are not proof receipts
+|===
+
+== Census corrections made with this record
+
+* The catalogue rows for echidnabot and hypatia were refreshed from a census
+  of those two repositories on 2026-11-09. echidnabot now shows its Agda,
+  Lean and Rocq theory files.
+* `scripts/census/build-rows.sh` chose whichever status document sorted
+  first, so hypatia was listed under `docs/proof-debt.adoc`. It now prefers
+  a `PROOF-STATUS` file, then `PROOF-NEEDS`, then `proof-debt`, so hypatia's
+  CI-checked `verification/PROOF-STATUS.adoc` is the one shown. Other rows
+  pick up this rule at the next full census.
+* echidnabot's class is still the heuristic `theory`, from its file counts.
+  Most of its proof files are prover fixtures (PROOF-POLICY §3); one
+  theorem is real theory.

scripts/census/build-rows.sh

@@ -42,7 +42,13 @@ jq -r '.repo+"\t"+.path' "$R/repos-with-status.jsonl" | sort > "$tmp/status.tsv"
 awk -F'\t' '
   FILENAME ~ /holes\.tsv$/  { h[$1" "$2]++; next }
   FILENAME ~ /decls\.tsv$/  { d[$1]++; next }
-  FILENAME ~ /status\.tsv$/ { if (!($1 in st)) st[$1]=$2; next }
+  # A repo with several status documents is listed under its proof-status
+  # ledger first, then its needs file, then its debt file; within one kind
+  # the first path in sort order wins.
+  FILENAME ~ /status\.tsv$/ {
+    k = ($2 ~ /(^|\/)PROOF-STATUS[^\/]*$/) ? 1 : ($2 ~ /(^|\/)PROOF-NEEDS[^\/]*$/) ? 2 : 3
+    if (!($1 in st) || k < sk[$1]) { st[$1]=$2; sk[$1]=k }
+    next }
   { n[$1]++; if ($3) fx[$1]++; pc[$1" "$2]++
     if ($2 ~ /agda|lean|rocq|isabelle/) th[$1]++; if ($2 ~ /idris2|spark/) en[$1]++ }
   END {