hyperpolymath · Nov 9, 2026 · Nov 9, 2026
@@ -11,7 +11,7 @@ Proofs stay in their home repositories. mathesis points at them. Later it
 will also hold the Agda sources for theory that has no other natural home.
 
 The rules for where a proof *should* live are not here: they are
-https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[the canonical standards/3-practice/PROOF-POLICY.adoc] (Creusot for Rust, SPARK for Ada,
+https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[the canonical standards/3-practice/PROOF-POLICY.adoc] (Creusot with Pearlite contracts, and Verus, for Rust; SPARK for Ada;
 Idris2 for APIs, ABIs and engineering properties, Agda for theory rechecked
 in Rocq and Lean). The working method is the proof-craft skill.
 

@@ -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/`

@@ -84,7 +84,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/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; 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/eclexia` — theory; 11 own proof files, 218 detected declarations; provers: agda 1, rocq 6, idris2 4
@@ -228,6 +228,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

@@ -35,6 +35,7 @@
 * `hyperpolymath/occupancy-types` — theory; 19 own proof files, 76 detected declarations; provers: agda 8, lean 5, 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/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 +120,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

@@ -79,7 +79,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/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/eclexia` — theory; 11 own proof files, 218 detected declarations; provers: agda 1, rocq 6, idris2 4
@@ -169,6 +169,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

@@ -114,6 +114,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/status/PROOF-STATUS.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 +139,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-STATUS.adoc`
 
 |https://github.com/hyperpolymath/ambientops[hyperpolymath/ambientops] |102 |1 |idris2 39, spark 58, other 5 |777 |39 |0 |8 |0 |`PROOF-NEEDS.adoc`
 

@@ -114,7 +114,7 @@ grade field.
 |nextgen-typing / Echo |Agda `Verification.agda` imports Echo; historical modules use `--safe --without-K` |Recheck compatible Echo and stdlib under all three policy flags; record mismatches
 |trope-checker / invariant-path |Graded-loss algebra and evidence/sortal distinctions carry independent open obligations |Compare exact theorem claims, not an assumed type–trope identity or triangulation
 |Mathesis |Manifest-driven per-prover gate and proof inventory; historical Agda manifest only attested `--safe` |Run full-mode check and attach genuine run receipt; only then advance status
-|ECHIDNA |Dogfood Agda corpus and meta-checker CI have separate commands; MetaChecker contains at least one stale 'funext' exception comment |Enforce uniform invocation and audit all imports/assumptions before marking Agda verified
+|ECHIDNA |Audited 2026-11-09. The meta-checker checks 9/9 modules under the policy flags (CI run 42551607796 at `2ab7574`, and a local run with the pinned Agda 2.7.0.1 and stdlib 2.1). The 'funext' exception was a stale line in `meta-checker/README.adoc`, not in a module, and is removed by echidna#479. Under the owner's strict §1 ruling (2026-11-09) only `Receipt.agda` (10 theorems) is theory; the other modules are engineering models of Rust code. The dogfood `proofs/agda/` tree is a §3 fixture, not an obligation |Rocq and Lean legs for the ten `Receipt.agda` theorems, with a §2.2 correspondence record per theorem
 |===
 
 Existing proof statuses in these repos are historical evidence, not
@@ -137,6 +137,11 @@ full-mode runs or cross-prover reconciliations were observed during
 this policy edit**. CI must supply the evidence before any result
 is relabelled.
 
+_Update 2026-11-09._ The ECHIDNA row is relabelled `AGDA-VERIFIED` on a
+recorded receipt (source commit, toolchain digests, flags, import cone and
+postulate scan); its grade, `PWG-3`, is derived (with hyperpolymath/echidna#479) in echidna's own
+`docs/PROOF-STATUS.adoc`, not here (§8.5). No row is reconciled.
+
 == Register format (initially not reconciled)
 
 [cols="2,2,2,2,3",options="header"]
@@ -145,7 +150,8 @@ is relabelled.
 |Mathesis |Properties example |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING
 |VCL-UT |L0–L10 / transition corpus |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING
 |Kategoria |Selected typed mechanism theorem (TBD) |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING
-|ECHIDNA |Meta-checker / dogfood Agda |AGDA-PENDING |Existing separate prover corpora; theorem matches not audited |BRIDGE-PENDING
+|ECHIDNA |`meta-checker/src/Echidna/Receipt.agda` (10 theory theorems) |AGDA-VERIFIED (receipt `docs/reports/2026-11-09-agda-cone-receipt.json`, landing in echidna with hyperpolymath/echidna#479: Agda 2.7.0.1, stdlib 2.1, policy flags, 211-module cone, clean postulate scan) |NOT-INVENTORIED (no Rocq or Lean artefact states these theorems) |BRIDGE-PENDING
+|proof-burrower |`Burrow/Trust.agda`, `Burrow/Ledger.agda` (DOM-1, DOM-2) |AGDA-PENDING (a 2026-11-09 re-check passed under the policy flags; no receipt is committed in that repository and no CI job runs it) |NOT-INVENTORIED |BRIDGE-PENDING
 |nextgen-typing |EchoTyping / Verification |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING
 |===
 

@@ -37,7 +37,13 @@ jq -r '[.repo,.file,.class]|@tsv' "$R/holes.jsonl" \
 jq -r '[.repo,.file]|@tsv' "$R/decls.jsonl" \
 | awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t){print $1}' "$T" - > "$tmp/decls.tsv"
 
-jq -r '.repo+"\t"+.path' "$R/repos-with-status.jsonl" | sort > "$tmp/status.tsv"
+# One status document per repo, preferring the proof-status file (the
+# ledger PROOF-POLICY names) over PROOF-NEEDS and proof-debt registers;
+# the awk below keeps the first row per repo.
+jq -r '(if (.path | test("(^|/)PROOF-STATUS[^/]*$")) then 0
+         elif (.path | test("(^|/)PROOF-NEEDS[^/]*$")) then 1 else 2 end | tostring)
+        + "\t" + .repo + "\t" + .path' "$R/repos-with-status.jsonl" \
+  | sort -t "$(printf '\t')" -k2,2 -k1,1n -k3,3 | cut -f2,3 > "$tmp/status.tsv"
 
 awk -F'\t' '
   FILENAME ~ /holes\.tsv$/  { h[$1" "$2]++; next }

@@ -75,6 +75,10 @@
 isabelle~*.thy~^\s*\(\*~unsafe~quick_and_dirty~quick_and_dirty
 creusot~*.rs~^\s*//~axiom~#[trusted]~#\[\s*(creusot::)?trusted\s*\]
 creusot~*.rs~^\s*//~hole~assume!~\b(proof_)?assume!\s*\(
+verus~*.rs~^\s*//~hole~assume~\bassume\s*\(
+verus~*.rs~^\s*//~hole~admit~\badmit\s*\(\s*\)
+verus~*.rs~^\s*//~axiom~external_body~#\[\s*verifier(::|\s*\(\s*)external_body
+verus~*.rs~^\s*//~axiom~assume_specification~\bassume_specification\b
 spark~*.adb,*.ads~^\s*--~hole~pragma Assume~pragma\s+Assume\b
 spark~*.adb,*.ads~^\s*--~unsafe~SPARK_Mode Off~SPARK_Mode\s*(=>\s*)?\(?\s*Off
 spark~*.adb,*.ads~^\s*--~unsafe~Skip_Proof~Skip_(Flow_And_)?Proof
@@ -99,6 +103,8 @@
     printf '%s\n' "$txt" | grep -qP -- "$comment" && continue
     if [ "$lang" = rocq ] && ! grep -qE '^\s*(Require|From|Theorem|Lemma|Definition|Inductive|Proof\.)' "$f"; then continue; fi
     if [ "$lang" = creusot ] && ! grep -qE 'creusot|pearlite|#\[\s*(requires|ensures)' "$f"; then continue; fi
+    # Verus code lives inside verus! { } blocks and imports vstd.
+    if [ "$lang" = verus ] && ! grep -qE 'verus!|vstd' "$f"; then continue; fi
     emit "$lang" "$class" "$marker" "${f#"$DIR"/}" "$n" "$(printf '%s' "$txt" | sed 's/^\s*//' | cut -c1-200)"
   done >>"$OUT"
 done <<<"$RULES"

@@ -3,14 +3,14 @@ import {test,expect} from 'bun:test';
 import {readFileSync} from 'node:fs';
 import {validate,validateVisibility,find,pack,render} from '../../scripts/atlas/census-atlas.mjs';
 const rows=JSON.parse(readFileSync(new URL('../../docs/catalogue/census/catalogue-rows.json',import.meta.url),'utf8'));
-test('existing corpus validated without modifying provenance',()=>{expect(validate(rows)).toHaveLength(239);expect(rows.some(r=>r.repo==='catachresis-colloquium/IDApTIK')).toBe(true);});
+test('existing corpus validated without modifying provenance',()=>{expect(validate(rows)).toHaveLength(240);expect(rows.some(r=>r.repo==='catachresis-colloquium/IDApTIK')).toBe(true);});
 test('duplicate source identity is rejected',()=>{expect(()=>validate([...rows,rows[0]])).toThrow(/duplicate/);});
 test('invalid class and counts are rejected',()=>{expect(()=>validate([{...rows[0],class:'machine-verified'}])).toThrow(/class/);expect(()=>validate([{...rows[0],own_files:-1}])).toThrow(/counts/);});
 test('case-insensitive source discovery',()=>{const a=find(rows,'IDRIS2');expect(a.length).toBeGreaterThan(0);expect(a.every(r=>r.provers.toLowerCase().includes('idris2'))).toBe(true);});
 test('context is bounded and contains verification caveat',()=>{const x=pack(rows,'idris2',500);expect(JSON.stringify(x,null,2).length+1).toBeLessThanOrEqual(500);expect(x.caveat).toContain('not mathematical proof verification');});
 test('deterministic A-Z and organisation views',()=>{const a=render(rows),b=render([...rows].reverse());expect(a).toEqual(b);expect(a['az.adoc']).toContain('A–Z proof-source directory');expect(JSON.parse(a['index.json']).verification).toBe('not_asserted');});
 
-test('nonpublic and unknown census sources fail closed',()=>{const inventory=JSON.parse(readFileSync(new URL('../../docs/catalogue/census/repos.json',import.meta.url),'utf8'));expect(validateVisibility(rows,inventory)).toHaveLength(239);expect(()=>validateVisibility(rows,[...inventory.filter(r=>r.full_name!==rows[0].repo)])).toThrow(/Nonpublic or unlisted/);});
+test('nonpublic and unknown census sources fail closed',()=>{const inventory=JSON.parse(readFileSync(new URL('../../docs/catalogue/census/repos.json',import.meta.url),'utf8'));expect(validateVisibility(rows,inventory)).toHaveLength(240);expect(()=>validateVisibility(rows,[...inventory.filter(r=>r.full_name!==rows[0].repo)])).toThrow(/Nonpublic or unlisted/);});
 
 test('every census counter is validated',()=>{for(const k of ['holes','axioms','fixture_files','unsafe','policy','own_files','declarations']){expect(()=>validate([{...rows[0],[k]:-1}])).toThrow(/Invalid census counts/);expect(()=>validate([{...rows[0],[k]:'12'}])).toThrow(/Invalid census counts/);}});
 test('A-Z display sorts by repository component, not owner',()=>{const v=render([{...rows[0],repo:'z-owner/beta'},{...rows[1],repo:'a-owner/alpha'}]);expect(v['az.adoc'].indexOf('a-owner/alpha')).toBeLessThan(v['az.adoc'].indexOf('z-owner/beta'));});