fix(census): comment-aware proof-holes.sh, Idris2 undefined-declaration axioms; refresh 13 rows

.github/workflows/estate-rules.yml

@@ -73,6 +73,8 @@ jobs:
         run: bash scripts/check-no-a2ml.sh .
       - name: No-a2ml gate self-test (planted positives must fail)
         run: bash tests/workflows/check_no_a2ml_test.sh
+      - name: Census hole scanner skips comments (planted markers and decoys)
+        run: bash tests/census/proof_holes_comments_test.sh
       - name: Deed clause writer controls
         run: bash tests/workflows/deed_clause_test.sh
       - name: Install verified Nickel 1.17.0

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/ephapax` — engineering; 44 own proof files, 654 detected declarations; provers: rocq 20, 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
@@ -121,7 +122,7 @@
 * `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/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/ephapax` — engineering; 44 own proof files, 654 detected declarations; provers: rocq 20, idris2 24
 * `hyperpolymath/ephapaxiser` — engineering; 9 own proof files, 133 detected declarations; provers: idris2 9
 * `hyperpolymath/error-lang` — engineering; 5 own proof files, 57 detected declarations; provers: idris2 5
 * `hyperpolymath/explicit-trust-plane` — engineering; 3 own proof files, 47 detected declarations; provers: idris2 3
@@ -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