hyperpolymath · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026
@@ -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/`

@@ -279,7 +279,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/trope-checker` — theory; 37 own proof files, 492 detected declarations; provers: agda 10, lean 11, idris2 16
+* `hyperpolymath/trope-checker` — theory; 38 own proof files, 514 detected declarations; provers: agda 10, lean 12, 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/typedqliser` — engineering; 11 own proof files, 155 detected declarations; provers: idris2 11

@@ -44,7 +44,7 @@
 * `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
 * `hyperpolymath/tangle` — theory; 3 own proof files, 61 detected declarations; provers: lean 3
-* `hyperpolymath/trope-checker` — theory; 37 own proof files, 492 detected declarations; provers: agda 10, lean 11, idris2 16
+* `hyperpolymath/trope-checker` — theory; 38 own proof files, 514 detected declarations; provers: agda 10, lean 12, idris2 16
 * `hyperpolymath/tropical-types` — theory; 28 own proof files, 540 detected declarations; provers: lean 19, isabelle 9
 * `hyperpolymath/valence-shell` — theory; 64 own proof files, 960 detected declarations; provers: agda 10, lean 16, rocq 12, isabelle 9, idris2 12, smt-atp 5
 * `hyperpolymath/wokelang` — theory; 18 own proof files, 418 detected declarations; provers: lean 7, rocq 3, idris2 8

@@ -198,7 +198,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/trope-checker` — theory; 37 own proof files, 492 detected declarations; provers: agda 10, lean 11, idris2 16
+* `hyperpolymath/trope-checker` — theory; 38 own proof files, 514 detected declarations; provers: agda 10, lean 12, 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/typedqliser` — engineering; 11 own proof files, 155 detected declarations; provers: idris2 11

@@ -34,9 +34,9 @@ verdicts.
 
 |https://github.com/hyperpolymath/firmboot[hyperpolymath/firmboot] |38 |0 |agda 19, lean 19 |409 |0 |1 |0 |0 |—
 
-|https://github.com/hyperpolymath/epistemic-types[hyperpolymath/epistemic-types] |37 |14 |agda 37 |320 |0 |0 |0 |0 |`PROOF-STATUS.adoc`
+|https://github.com/hyperpolymath/trope-checker[hyperpolymath/trope-checker] |38 |0 |agda 10, lean 12, idris2 16 |514 |0 |0 |0 |1 |`docs/status/PROOF-STATUS.adoc`
 
-|https://github.com/hyperpolymath/trope-checker[hyperpolymath/trope-checker] |37 |0 |agda 10, lean 11, idris2 16 |492 |10 |0 |0 |1 |`docs/proof-debt.adoc`
+|https://github.com/hyperpolymath/epistemic-types[hyperpolymath/epistemic-types] |37 |14 |agda 37 |320 |0 |0 |0 |0 |`PROOF-STATUS.adoc`
 
 |https://github.com/hyperpolymath/arghda-core[hyperpolymath/arghda-core] |32 |32 |agda 13, lean 2, rocq 4, isabelle 4, idris2 7, smt-atp 2 |15 |0 |0 |0 |0 |—
 
@@ -479,9 +479,9 @@ verdicts.
 
 |https://github.com/hyperpolymath/dictask[hyperpolymath/dictask] |1 |0 |idris2 1 |17 |2 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
 
-|https://github.com/hyperpolymath/haec[hyperpolymath/haec] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+|https://github.com/hyperpolymath/haec[hyperpolymath/haec] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-STATUS.adoc`
 
-|https://github.com/hyperpolymath/hermeneia[hyperpolymath/hermeneia] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+|https://github.com/hyperpolymath/hermeneia[hyperpolymath/hermeneia] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-STATUS.adoc`
 
 |https://github.com/hyperpolymath/laminar[hyperpolymath/laminar] |1 |0 |idris2 1 |6 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
 

@@ -147,8 +147,105 @@ is relabelled.
 |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
 |nextgen-typing |EchoTyping / Verification |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING
+|trope-checker |Theorem B, Targets 1–4 |AGDA-VERIFIED — `proofs.yml` run 42623339243 at `c0eb4f1`, log `PASS: All.agda + Smoke.agda typecheck (--safe --without-K --cubical-compatible)`, Agda 2.7.0.1 + stdlib v2.0 pinned by SHA-256 |Rocq: none exists (ADR 0005 D5 removed the template). Lean: states no part of Theorem B |BRIDGE-PENDING (no leg to bridge to)
+|trope-checker |O1-carrier atom factorisation, tropical factorisations, grade-algebra boundary |No Agda source states them |LEAN-CHECKED (kernel-accepted; `[propext]` for `GradeR.atom_factorization`). Rocq: none. The whole Lean package imports Mathlib, which PROOF-POLICY §2 forbids for a recheck leg |BRIDGE-PENDING
 |===
 
+== Catalogued grades (derived, never assigned here)
+
+PROOF-POLICY §8.5: "Mathesis may catalogue grades. It derives them from those
+receipts and does not assign them. The home repository owns the theorem and its
+evidence." What follows is a catalogue entry only; the authority is
+`hyperpolymath/trope-checker`, `docs/status/PROOF-STATUS.adoc`.
+
+As of 2026-11-09, trope-checker carries the estate's first §8.5 PWG record, and
+it is a *generated* one: `verification/pwg.json` holds evidence only — per
+obligation, each leg's route, its §5 token, its §2.2 state and its receipts — and
+`scripts/pwg-derive.sh` is the only thing that turns that into a grade. A `pwg`
+key in the ledger is a gate failure, which is how §8.4 rule 2 stops being
+aspirational. `scripts/pwg-check.sh` re-derives and fails on drift, and
+`scripts/test-gate-falsifiability.sh` carries canaries proving the gate can fail,
+including two that change only the derived grade.
+
+The derived census, read from that repository (never computed here):
+
+[cols="2,1,4",options="header"]
+|===
+|Rung |Count |What the rung means here
+
+|`PWG-3` |17 |A kernel-checked Agda witness with a complete §8.2 receipt at the
+current commit, and no counting recheck leg. Earned on 2026-11-09 by dispatching
+`proofs.yml` on `main`: run 42623339243 at `c0eb4f1`, log ending `PASS: All.agda +
+Smoke.agda typecheck (--safe --without-K --cubical-compatible)`. The flags in
+force were already §2.1-conformant; what was missing was the *record*, because
+every written-up result said `--safe --without-K` only and §2.1 declassifies
+prior successes under that profile. The mathematics did not change.
+|`PWG-2i` / `PWG-2ii` / `PWG-1` |0 |Unreachable, but not all for the same reason.
+`PWG-2i` needs only *one* counting leg (§8.2), so a reconciled Lean recheck would
+suffice without Rocq — except that trope-checker's Lean leg is target-only
+evidence under §3, hence `BRIDGE-PENDING`, and the owner's 2026-11-09 ruling makes
+Lean a generator rather than a leg, so it will not become one. `PWG-2ii` and
+`PWG-1` additionally require the Rocq leg, and no Rocq development exists in that
+repository at all.
+|`ungraded` |7 |Three ways, and the split is the useful part. Three are Lean-only
+with no Agda source (§8.1): the O1-carrier atom factorisation, tier-2 membership,
+and the (B′) tropical factorisation. Three are Idris2-only, and an engineering
+restatement is not a leg (§8.1): HC-4 coherence, exact-lowering grade soundness,
+T-Sub soundness. One is the retention order, whose Agda leg proves reflexivity but
+not transitivity or decidability, so its Agda token is `OPEN`.
+|===
+
+Denominator 24 theory obligations. Verdict soundness is reclassified engineering
+and is off the ladder entirely (§8.1), so it is not in that count.
+
+`PWG-3` is not a discharge (§8.4 rule 1). All seventeen still owe both recheck
+legs, and so does every other theory result in the stack.
+
+Owner ruling 2026-11-09 on the Mathlib question, recorded here because it decides
+what those seven can become: *Lean is a generator, not a leg.* The Lean
+development keeps Mathlib and keeps its purpose — finding and stress-testing
+theorems — and its results are restated in core Agda, which is what becomes
+gradeable. So the three Lean-only rows do not become legs by any amount of
+bridging work; they become `PWG-3` when their Agda restatement lands, and no
+sooner.
+
+These results cannot reach `PWG-2i`, `PWG-2ii` or `PWG-1` from where the tree
+stands: the current Lean development is not a counting leg, and no Rocq
+development exists. A separate, policy-conformant Lean recheck that is
+`RECONCILED`, together with a qualifying Agda witness, could satisfy `PWG-2i`
+without Rocq; the theorem would still need its second recheck leg. `PWG-2ii` and
+`PWG-1` require Rocq as well. This is the first concrete instance of the pattern
+this document predicted — a successful independent proof is not a verified
+Agda–Lean–Coq bridge. It also separates three failure modes that a prose status
+line had run together:
+
+. a *bookkeeping* gap — the proof was there and the record was not. A dispatch
+  closed it in four minutes and moved seventeen obligations to `PWG-3`.
+. a missing *source* — the theorem exists only in Lean, so there is nothing for
+  the ladder to grade. Only writing the Agda closes it.
+. a missing *rung* — no Rocq development exists, so `PWG-2ii` is unreachable
+  however much Agda or Lean work is done. Only a policy change or a new Rocq
+  development closes it, and the owner has chosen to put the policy question to
+  `standards`.
+
+The first was cheap, the second is proof work, the third is a decision. Reporting
+them as one number would have hidden all three.
+
+NOTE: the census row for trope-checker was refreshed on 2026-11-09 by re-running
+`scripts/census/census-repo.sh` against `main` `c0eb4f1`. It had published 10
+holes; the current count is 0. The 10 were in the never-instantiated Coq, TLA+
+and Agda templates that trope-checker PR #102 deleted, so the catalogue had been
+over-reporting that repository's proof debt. `own_files` 37→38, `lean` 11→12 and
+`declarations` 492→514 also moved, from `EffectAtomsRatified.lean` landing in
+PR #107. Rows carry no commit or census date, so a stale row is indistinguishable
+from a fresh one by inspection; recording per-row provenance is an open
+improvement to the census, not a defect of this entry.
+
+The absences are correct and were checked, not assumed: `vocarium` has eleven
+prover files but every one of them is on `census/template-paths.txt`, so its
+`own_files` is 0; `trope-particularity-workbench` has no prover file at all.
+Neither belongs in the catalogue on the census's own rules.
+
 References:
 https://agda.readthedocs.io/en/v2.7.0.1/language/cubical-compatible.html[Agda cubical-compatible];
 https://github.com/hyperpolymath/vcl-ut[owned VCL-UT gate];

@@ -20,7 +20,16 @@
 | *Total* | *7* | *0* | *0* | *0* | *7*
 |===
 
-*Overall*: 0% proven
+*Census.* Of 7 recorded obligations: 0 done, 0 in progress, 0 blocked, 7
+remaining. No obligation here carries a Proof Witness Grade, because none is a
+theory obligation of this repository under PROOF-POLICY §8.1.
+
+NOTE: this line used to read "*Overall*: 0% proven". PROOF-POLICY §8.4 rule 7 is
+explicit — "Never publish 'X% proved', an average grade, or a single confidence
+score" — and requires a count per category with the denominator instead. The
+figure was accurate; the *form* was the one the policy forbids. The same line
+ships in `rsr-template-repo`'s `PROOF-STATUS.adoc`, so every repository minted
+from it carries it; fixing it there is the solution at source.
 
 == Proofs Done
 

@@ -37,7 +37,27 @@ 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 pointer per repo, chosen by PRECEDENCE, not alphabetically. PROOF-POLICY
+# §8.5 puts a theorem's Proof Witness Grade in "its home repository's
+# proof-status file", so that file is the one the catalogue should point at.
+# Plain `sort` put docs/proof-debt.adoc ahead of docs/status/PROOF-STATUS.adoc
+# and PROOF-NEEDS ahead of PROOF-STATUS, so every repository carrying more than
+# one of them pointed at the wrong file: the debt ledger or the list of what is
+# owed, instead of the record of what is proved.
+jq -r '.repo+"\t"+.path' "$R/repos-with-status.jsonl" \
+| awk -F'\t' 'BEGIN{OFS="\t"} {
+    # Rank the BASENAME, case-insensitively. Matching the whole path would rank a
+    # debt ledger that happens to sit under a PROOF-STATUS/ directory as if it
+    # were the proof-status file, and the catalogue would point at the wrong one.
+    name = tolower($2)
+    sub(/^.*\//, "", name)
+    r = 3
+    if (name ~ /^proof-status/)      r = 0
+    else if (name ~ /^proof-needs/)  r = 1
+    else if (name ~ /^proof-debt/)   r = 2
+    print $1, r, $2 }' \
+| sort -t"$(printf '\t')" -k1,1 -k2,2n \
+| cut -f1,3 > "$tmp/status.tsv"
 
 awk -F'\t' '
   FILENAME ~ /holes\.tsv$/  { h[$1" "$2]++; next }