diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
index a3ae611..1c97499 100644
--- a/.github/workflows/hypatia-scan.yml
+++ b/.github/workflows/hypatia-scan.yml
@@ -31,7 +31,7 @@ jobs:
       contents: read
       security-events: write
     env:
-      HYPATIA_SHA: '6693f9aed8e4383f78a3d01b600b32663bf7a45c'
+      HYPATIA_SHA: 'b7944d3c6214ac921aa3681db628a765df672a64'
     steps:
       - name: Checkout repository
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
@@ -53,7 +53,7 @@ jobs:
             ~/hypatia
             ~/.hex
             ~/.mix
-          key: hypatia-sarif-${{ runner.os }}-otp28-elx1194-6693f9aed8e4383f78a3d01b600b32663bf7a45c
+          key: hypatia-sarif-${{ runner.os }}-otp28-elx1194-b7944d3c6214ac921aa3681db628a765df672a64
 
       - name: Build pinned Hypatia scanner
         run: |
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
index d3efbf4..84aa471 100644
--- a/EXPLAINME.adoc
+++ b/EXPLAINME.adoc
@@ -77,10 +77,10 @@ from a standards checkout whose file digest it also checks. The view is
 contract clause `no-hand-typed-grade` checks that no pin carries a grade.
 
 Caveat::
-Of 13 theorems, 1 is at `PWG-1` (THY-1) and 12 are `ungraded`. The canon
-reader refuses the current receipts of two home repositories, so their pins
-derive no grade until one side changes (an open finding in
-link:docs/status/ROADMAP.adoc[the roadmap]).
+Of 17 theorems, 11 are at `PWG-1` (THY-1, APP-1 to APP-4, and six of
+secret-types) and 6 are `ungraded` (run on 2026-11-14). The six are Lintel
+claims: their pins, at Lintel `a0f2bae`, name no receipt, so they derive no
+grade. Lintel's main now holds a receipt that no pin names yet.
 
 == Bridge candidates
 
diff --git a/docs/atlas/claims/claims.jsonl b/docs/atlas/claims/claims.jsonl
index adcbd1e..970156b 100644
--- a/docs/atlas/claims/claims.jsonl
+++ b/docs/atlas/claims/claims.jsonl
@@ -15,4 +15,8 @@
 {"agda":{"module":"Lintel.Instance","names":["tini-per-role","tini-coalition"]},"claim":"L-6","id":"metadatastician/lintel#L-6","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"tini holds at this lattice over the address, the query name and the client's local state, for each role's observer and for any two roles observing together","status_doc":"README.adoc"}
 {"agda":{"module":"Lintel.Composition","names":["writes-flow","link-written-to-client","link-written-to-local","link-writable"]},"claim":"L-7","id":"metadatastician/lintel#L-7","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"Self-defeating privacy compositions cannot be built as programs: a typed command writes a value depending on both fields only into a variable the client alone may read","status_doc":"README.adoc"}
 {"agda":null,"claim":"A-1","id":"metadatastician/lintel#A-1","kind":"assumption","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"Non-collusion: no party holds both the proxy and the target role (the gap is proved: collusion-gap)","status_doc":"README.adoc"}
-{"agda":{"module":"FeatureReachability","names":["Cargo.absent-under-all-features","Monotone.reach-mono"]},"claim":"THY-1","id":"hyperpolymath/mathesis#THY-1","kind":"theorem","receipt":{"path":"verification/receipts/theory_praxis.deed","sha256":"001903cb2cf4822aa3a8b4d7ff9bbc8cec99a72d73135df71795529272f95101"},"repo":"hyperpolymath/mathesis","source_commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","statement":"In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone.","status_doc":"docs/status/PROOF-STATUS.adoc"}
+{"agda":{"module":"FeatureReachability","names":["Cargo.absent-under-all-features","Monotone.reach-mono"]},"claim":"THY-1","id":"hyperpolymath/mathesis#THY-1","kind":"theorem","receipt":{"path":"verification/receipts/theory_praxis.deed","sha256":"7e175ec06b47177983d5cd9360043358268fb53ea5a69cd75dde58d196cf1c2c"},"repo":"hyperpolymath/mathesis","shelf":"theory","source_commit":"a1388fcc922ea6d6930fdae78f569139493be975","statement":"In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone.","status_doc":"docs/status/PROOF-STATUS.adoc"}
+{"agda":{"module":"Applied.Missing","names":["Proofs.closing-needs","Proofs.missing-persists","Proofs.closings-missing","Proofs.verdict-yes","Proofs.breach-decides"]},"claim":"APP-1","id":"hyperpolymath/mathesis#APP-1","kind":"theorem","receipt":{"path":"verification/receipts/theory_praxis.deed","sha256":"7e175ec06b47177983d5cd9360043358268fb53ea5a69cd75dde58d196cf1c2c"},"repo":"hyperpolymath/mathesis","shelf":"applied","source_commit":"a1388fcc922ea6d6930fdae78f569139493be975","statement":"Missing propagates: in the cohort model, an output that depends on a missing input is missing, in every period after it too, and never zero. A verdict is \"no\" on a known breach and otherwise missing when any value it depends on is missing; it is never \"yes\" then.","status_doc":"docs/status/PROOF-STATUS.adoc"}
+{"agda":{"module":"Applied.Cash","names":["Proofs.cash-identity"]},"claim":"APP-2","id":"hyperpolymath/mathesis#APP-2","kind":"theorem","receipt":{"path":"verification/receipts/theory_praxis.deed","sha256":"7e175ec06b47177983d5cd9360043358268fb53ea5a69cd75dde58d196cf1c2c"},"repo":"hyperpolymath/mathesis","shelf":"applied","source_commit":"a1388fcc922ea6d6930fdae78f569139493be975","statement":"Cash identity: the closing cash of the last period equals the opening cash plus, summed over the periods, receipts minus payments; when a value is missing, both sides are missing. Proved for any ordered abelian group; `Applied.IntLaws` proves the integers are one.","status_doc":"docs/status/PROOF-STATUS.adoc"}
+{"agda":{"module":"Applied.Cash","names":["Proofs.gap-sound","Proofs.gap-least"]},"claim":"APP-3","id":"hyperpolymath/mathesis#APP-3","kind":"theorem","receipt":{"path":"verification/receipts/theory_praxis.deed","sha256":"7e175ec06b47177983d5cd9360043358268fb53ea5a69cd75dde58d196cf1c2c"},"repo":"hyperpolymath/mathesis","shelf":"applied","source_commit":"a1388fcc922ea6d6930fdae78f569139493be975","statement":"The funding gap is sound and least: adding the gap to the opening cash keeps every closing balance at or above its floor, and no smaller non-negative amount does. Proved for any ordered abelian group; `Applied.IntLaws` proves the integers are one.","status_doc":"docs/status/PROOF-STATUS.adoc"}
+{"agda":{"module":"Applied.Missing","names":["Proofs.members-needs","Proofs.receipts-needs","Proofs.payments-needs","Proofs.closing-needs","Proofs.shortfall-needs","Proofs.cashOk-needs","Proofs.hours-needs","Proofs.capacityOk-needs","Proofs.gap-needs"]},"claim":"APP-4","id":"hyperpolymath/mathesis#APP-4","kind":"theorem","receipt":{"path":"verification/receipts/theory_praxis.deed","sha256":"7e175ec06b47177983d5cd9360043358268fb53ea5a69cd75dde58d196cf1c2c"},"repo":"hyperpolymath/mathesis","shelf":"applied","source_commit":"a1388fcc922ea6d6930fdae78f569139493be975","statement":"Status never upgrades: the evidence status of an output is never stronger than the weakest status of the inputs that it depends on.","status_doc":"docs/status/PROOF-STATUS.adoc"}
diff --git a/docs/atlas/generated/registry.adoc b/docs/atlas/generated/registry.adoc
index 8d796c6..421cdfd 100644
--- a/docs/atlas/generated/registry.adoc
+++ b/docs/atlas/generated/registry.adoc
@@ -10,13 +10,21 @@ assigned (§8.5). A grade is not a discharge (§8.4): `PWG-3` theorems still
 owe their Rocq and Lean legs. Status of this slice: accepted in
 link:../../decisions/0004-claims-registry.adoc[ADR 0004], ratified by the owner.
 
-Census: 6 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 7 `ungraded`, of 13 theorems. 5 demonstrations and assumptions are listed and not graded.
+Census: 11 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 6 `ungraded`, of 17 theorems. 5 demonstrations and assumptions are listed and not graded.
 
 [cols="2,1,1,4,3",options="header"]
 |===
 |Claim |Kind |PWG |Statement (home repository's wording) |Why not higher
 
-|https://github.com/hyperpolymath/mathesis/blob/9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#THY-1] at `9aa1662da5b2` |theorem |`ungraded` |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. (`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`) |the canon reader refuses the receipt: a receipt of the agda leg of claim "THY-1" is current and is missing :inputs-sha256 (§8.5.1)
+|https://github.com/hyperpolymath/mathesis/blob/a1388fcc922ea6d6930fdae78f569139493be975/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#APP-1] at `a1388fcc922e`; the receipt describes `034f215b3b60` |theorem |`PWG-1` |Missing propagates: in the cohort model, an output that depends on a missing input is missing, in every period after it too, and never zero. A verdict is "no" on a known breach and otherwise missing when any value it depends on is missing; it is never "yes" then. (`Applied.Missing`: `Proofs.closing-needs`, `Proofs.missing-persists`, `Proofs.closings-missing`, `Proofs.verdict-yes`, `Proofs.breach-decides`) |—
+
+|https://github.com/hyperpolymath/mathesis/blob/a1388fcc922ea6d6930fdae78f569139493be975/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#APP-2] at `a1388fcc922e`; the receipt describes `034f215b3b60` |theorem |`PWG-1` |Cash identity: the closing cash of the last period equals the opening cash plus, summed over the periods, receipts minus payments; when a value is missing, both sides are missing. Proved for any ordered abelian group; `Applied.IntLaws` proves the integers are one. (`Applied.Cash`: `Proofs.cash-identity`) |—
+
+|https://github.com/hyperpolymath/mathesis/blob/a1388fcc922ea6d6930fdae78f569139493be975/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#APP-3] at `a1388fcc922e`; the receipt describes `034f215b3b60` |theorem |`PWG-1` |The funding gap is sound and least: adding the gap to the opening cash keeps every closing balance at or above its floor, and no smaller non-negative amount does. Proved for any ordered abelian group; `Applied.IntLaws` proves the integers are one. (`Applied.Cash`: `Proofs.gap-sound`, `Proofs.gap-least`) |—
+
+|https://github.com/hyperpolymath/mathesis/blob/a1388fcc922ea6d6930fdae78f569139493be975/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#APP-4] at `a1388fcc922e`; the receipt describes `034f215b3b60` |theorem |`PWG-1` |Status never upgrades: the evidence status of an output is never stronger than the weakest status of the inputs that it depends on. (`Applied.Missing`: `Proofs.members-needs`, `Proofs.receipts-needs`, `Proofs.payments-needs`, `Proofs.closing-needs`, `Proofs.shortfall-needs`, `Proofs.cashOk-needs`, `Proofs.hours-needs`, `Proofs.capacityOk-needs`, `Proofs.gap-needs`) |—
+
+|https://github.com/hyperpolymath/mathesis/blob/a1388fcc922ea6d6930fdae78f569139493be975/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#THY-1] at `a1388fcc922e`; the receipt describes `034f215b3b60` |theorem |`PWG-1` |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. (`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`) |—
 
 |https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-1] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent (`SecretTypes.Noninterference`: `tini`) |—
 
diff --git a/docs/decisions/0004-claims-registry.adoc b/docs/decisions/0004-claims-registry.adoc
index 70614a7..eed4286 100644
--- a/docs/decisions/0004-claims-registry.adoc
+++ b/docs/decisions/0004-claims-registry.adoc
@@ -64,6 +64,10 @@ does not restate mathematics.
 |`status_doc` |The home repository's proof-status file.
 |`agda` |For a theorem: `{module, names}`, the Agda source of truth (§1). `null`
 otherwise.
+|`shelf` |For a theorem whose home is Mathesis only: `theory` or `applied`
+(owner ruling 2026-11-12). A theory-shelf theorem needs an admission record
+in `docs/theory/admissions.jsonl`; an applied-shelf theorem does not. Both are
+graded. A record about another repository has no `shelf`.
 |`source_commit` |The full 40-character commit the record describes.
 |`receipt` |`{path, sha256}` of the home repository's machine receipt at that
 commit, or `null` when it has none.
diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc
index 4e4ade1..74a64da 100644
--- a/docs/status/PROOF-STATUS.adoc
+++ b/docs/status/PROOF-STATUS.adoc
@@ -25,13 +25,14 @@ reader of PROOF-POLICY §8.5.1.
 
 |APP-1 to APP-4, the cohort model of the applied shelf (WO 4.2)
 |Proved in Agda, Rocq and Lean
-|-
-|The record below. The receipt derives `PWG-1` (2026-11-13)
+|`PWG-1`
+|The receipt `verification/receipts/theory_praxis.deed`; the record below.
+Claim pins at main `a1388fc` (2026-11-14)
 |===
 
-*Overall*: 5 of 6 obligations are proved in all three provers; THY-1 alone has
-a receipt and a derived grade. The token-lattice theorems (counted as one) are
-open. These are counts, not a
+*Overall*: 5 of 6 obligations are proved in all three provers, and each of the
+5 has a receipt and a derived grade, `PWG-1`. The token-lattice theorems
+(counted as one) are open. These are counts, not a
 percentage: PROOF-POLICY §8 grades are derived from receipts and are never
 flattened. The template example proofs were removed in WO 4.1.
 
@@ -292,6 +293,12 @@ bash tests/proofs/gate_controls_test.sh agda
 |===
 |Date |Change
 
+|2026-11-14
+|The claim pins of THY-1 and APP-1 to APP-4 name the receipt at main
+`a1388fc`. APP-1 to APP-4 are on the applied shelf. The claims registry
+catalogues `PWG-1` for all five: the reader derives it, and the §8.5.3 git
+checks hold.
+
 |2026-11-13
 |The receipt is written again under PROOF-POLICY §8.5.1 at standards
 `e5a39d7`: each current receipt records its inputs manifest and its axioms.
diff --git a/docs/status/READINESS.adoc b/docs/status/READINESS.adoc
index 9628bc0..b0a0ebe 100644
--- a/docs/status/READINESS.adoc
+++ b/docs/status/READINESS.adoc
@@ -77,8 +77,9 @@ public repository is not reached
 |Claims registry (`scripts/registry/`)
 |D
 |alpha-unstable
-|14 tests pass; ADR 0004; 18 claim pins, 13 theorems, 1 graded `PWG-1`
-|The canon reader refuses the receipts of two homes; a dogfood log
+|26 tests pass; ADR 0004; 22 claim pins, 17 theorems, 11 graded `PWG-1`
+(2026-11-14)
+|Lintel's pins, at `a0f2bae`, name no receipt (its main now has one); a dogfood log
 
 |Proof gate and home theory (`scripts/check-proofs.sh`,
 `verification/`)
diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc
index 39b3fda..41fcbb7 100644
--- a/docs/status/ROADMAP.adoc
+++ b/docs/status/ROADMAP.adoc
@@ -229,16 +229,23 @@ One pull request that changes census rows is open at a time (atlas README,
    43498592499 on main `034f215`. It adds APP-1 to APP-4 and earns THY-1
    again; the reader derives `PWG-1` for all five, and `just receipt-check`
    (the home gate, in `just check`) passes. The registry pins the new reader
-   and catalogues a `PWG-1` only when the git checks hold. Until the next
-   change, the registry shows THY-1 as `ungraded`, because its claim pin names
+   and catalogues a `PWG-1` only when the git checks hold. Until the second
+   change, the registry showed THY-1 as `ungraded`, because its claim pin named
    the old receipt; the theory ledger records this.
 ** The same change pins the nine secret-types claims at its main `4ed0672`
    (re-anchoring plan WO 5.1). Its receipt names `292d566`, with the echo
    `7dfeab2` to `292d566` for the squash merge of its pull request 40. The
    reader derives `PWG-1` for N-1, N-2, N-3, N-7, N-8 and N-9, and the
    registry's git checks hold, so the registry catalogues six `PWG-1`.
-** Next change: the claim pins of THY-1 and APP-1 to APP-4 (applied shelf, a
-   new `shelf` field).
+** Second change: the claim pins of THY-1 and APP-1 to APP-4 name the
+   receipt at main `a1388fc` (the merge of PR 90). A home theorem now names
+   its shelf: THY-1 is on the theory shelf, and APP-1 to APP-4 are on the
+   applied shelf, which needs no admission. The registry catalogues `PWG-1`
+   for all five, and the theory ledger records THY-1's return to `PWG-1`.
+   Census: 11 `PWG-1` and 6 `ungraded` (Lintel: its pins, at `a0f2bae`, name no receipt) of 17
+   theorems. The Hypatia scanner pin moves to `b7944d3` (hypatia#1087, the
+   JavaScript-aware `js_exec_sync` rule), and `scripts/site/site.mjs` drops
+   its `hypatia:ignore` annotation.
 
 [[stages]]
 == Stages
diff --git a/docs/theory/README.adoc b/docs/theory/README.adoc
index 7755cec..10d8e6d 100644
--- a/docs/theory/README.adoc
+++ b/docs/theory/README.adoc
@@ -23,6 +23,10 @@ A theorem enters the shelf only when all three conditions hold:
 
 A theorem that meets the rule is proved in Agda and re-checked in Rocq and
 Lean (PROOF-POLICY §1 and §2), with a receipt in `verification/receipts/`.
+Its claim pin in `docs/atlas/claims/claims.jsonl` carries `"shelf": "theory"`.
+A theorem of the applied shelf (`applied-systems/`) carries
+`"shelf": "applied"`. It is proved and graded in the same way, but it needs no
+admission, because no estate rule depends on it.
 
 == Where the records are
 
diff --git a/docs/theory/generated/index.adoc b/docs/theory/generated/index.adoc
index cb2cd98..b96653d 100644
--- a/docs/theory/generated/index.adoc
+++ b/docs/theory/generated/index.adoc
@@ -13,6 +13,6 @@ Theorems: 1.
 |===
 |Theorem |Statement |PWG |Source and receipt |Dependant
 
-|THY-1 |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. |`ungraded` |`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`; `verification/receipts/theory_praxis.deed` at `9aa1662da5b2` |https://github.com/metadatastician/standards/blob/main/docs/UPSTREAM-DEPENDENCY-WATCH.adoc[metadatastician/standards]: Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build.
+|THY-1 |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. |`PWG-1` |`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`; `verification/receipts/theory_praxis.deed` at `a1388fcc922e` |https://github.com/metadatastician/standards/blob/main/docs/UPSTREAM-DEPENDENCY-WATCH.adoc[metadatastician/standards]: Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build.
 
 |===
diff --git a/docs/theory/ledger.jsonl b/docs/theory/ledger.jsonl
index 1a76a90..f946835 100644
--- a/docs/theory/ledger.jsonl
+++ b/docs/theory/ledger.jsonl
@@ -1,2 +1,3 @@
 {"admission_sha256":"91977ed786bb4a63913234167876096bf6e93491e828dcc3e1e7538862349fc5","date":"2026-11-11","event":"admitted","id":"hyperpolymath/mathesis#THY-1","note":"The ledger starts here, on 2026-11-11. THY-1 was proved in Agda on 2026-11-09 and re-proved in Rocq and Lean; it derived PWG-2ii until the CI receipts of run 42896264290 gave PWG-1 on 2026-11-10. Transport from Agda was blocked, because the Lambdapi exports to Rocq and Lean drop rewrite rules. Earlier history is in git and docs/status/PROOF-STATUS.adoc.","pwg":"PWG-1","receipt":{"commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","path":"verification/receipts/theory_praxis.deed","sha256":"001903cb2cf4822aa3a8b4d7ff9bbc8cec99a72d73135df71795529272f95101"},"seq":1}
 {"admission_sha256":"91977ed786bb4a63913234167876096bf6e93491e828dcc3e1e7538862349fc5","changes":["pwg"],"date":"2026-11-13","event":"changed","id":"hyperpolymath/mathesis#THY-1","note":"The reader pin moved to standards e5a39d7, which requires an inputs manifest, the axioms and the inputs digest on every current receipt. The receipt that THY-1's claim pin names predates them, so the reader refuses it. The Mathesis receipt is regenerated in the same change, and the next change moves THY-1's pin to it.","pwg":"ungraded","receipt":{"commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","path":"verification/receipts/theory_praxis.deed","sha256":"001903cb2cf4822aa3a8b4d7ff9bbc8cec99a72d73135df71795529272f95101"},"seq":2}
+{"admission_sha256":"91977ed786bb4a63913234167876096bf6e93491e828dcc3e1e7538862349fc5","changes":["pwg","receipt"],"date":"2026-11-14","event":"changed","id":"hyperpolymath/mathesis#THY-1","note":"THY-1's claim pin moved to main a1388fc, where the receipt written under PROOF-POLICY 8.5.1 (PR 90) is on main. The canon reader at standards e5a39d7 derives PWG-1 from it, and the 8.5.3 git checks hold, so the registry catalogues PWG-1 again.","pwg":"PWG-1","receipt":{"commit":"a1388fcc922ea6d6930fdae78f569139493be975","path":"verification/receipts/theory_praxis.deed","sha256":"7e175ec06b47177983d5cd9360043358268fb53ea5a69cd75dde58d196cf1c2c"},"seq":3}
diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs
index 78dfd32..ebfce27 100644
--- a/scripts/registry/claims-registry.mjs
+++ b/scripts/registry/claims-registry.mjs
@@ -31,7 +31,7 @@ import {fileURLToPath, pathToFileURL} from 'node:url';
 import path from 'node:path';
 import {readJsonl} from '../atlas/census-atlas.mjs';
 import {validateBridges, renderBridges} from './bridges.mjs';
-import {validateAdmissions, renderTheoryIndex} from './theory.mjs';
+import {validateAdmissions, renderTheoryIndex, HOME} from './theory.mjs';
 import {validateLedger, snapshot, pending, checkAppendOnly, jcs} from './theory-ledger.mjs';
 
 const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../..');
@@ -58,6 +58,7 @@ async function ledgerOnMain() {
 
 const KINDS = new Set(['theorem', 'demonstration', 'assumption']);
 const PWG = new Set(['PWG-1', 'PWG-2ii', 'PWG-2i', 'PWG-3', 'ungraded']);
+const SHELVES = new Set(['theory', 'applied']);
 
 // The canon reader, pinned by commit and by the digest of its file. A reader
 // that is not this file is refused, so a grade never comes from an unpinned rule.
@@ -101,6 +102,9 @@ export function validate(rows, inventory) {
       if (!r.agda || typeof r.agda.module !== 'string' || !Array.isArray(r.agda.names) || r.agda.names.length === 0)
         throw new Error(`A theorem names its Agda module and names: ${r.id}`);
     }
+    if (r.repo === HOME && r.kind === 'theorem') {
+      if (!SHELVES.has(r.shelf)) throw new Error(`A home theorem is on the theory or the applied shelf: ${r.id}`);
+    } else if ('shelf' in r) throw new Error(`Only a home theorem names a shelf: ${r.id}`);
     if (r.receipt !== null) {
       if (!r.receipt || typeof r.receipt.path !== 'string' || !/^[0-9a-f]{64}$/.test(r.receipt.sha256 ?? ''))
         throw new Error(`receipt is null or {path, sha256}: ${r.id}`);
diff --git a/scripts/registry/theory.mjs b/scripts/registry/theory.mjs
index 587ddd4..72f3a14 100644
--- a/scripts/registry/theory.mjs
+++ b/scripts/registry/theory.mjs
@@ -12,6 +12,9 @@
 // receipt and renders docs/theory/generated/index.adoc from both.
 
 export const HOME = 'hyperpolymath/mathesis';
+// A home theorem is on the theory shelf or on the applied shelf (owner ruling
+// 2026-11-12). Only the theory shelf needs an admission.
+export const onTheoryShelf = r => r.repo === HOME && r.kind === 'theorem' && r.shelf === 'theory';
 const FIELDS = new Set(['id', 'admitted', 'theory', 'owner', 'dependant']);
 const DEPENDANT_FIELDS = new Set(['repository', 'path', 'rule']);
 
@@ -23,17 +26,17 @@ const need = (ok, message) => {
 };
 
 // Throw unless every admission is well formed, names a public dependant, and
-// matches one home theorem pin; and unless every home theorem pin has one
+// matches one theory-shelf pin; and unless every theory-shelf pin has one
 // admission. `rows` are the validated claim pins.
 export function validateAdmissions(admissions, rows, inventory) {
   need(Array.isArray(admissions), 'docs/theory/admissions.jsonl must hold one admission record on each line');
   const visibility = new Map(inventory.map(r => [r.full_name, r.visibility]));
-  const home = new Map(rows.filter(r => r.repo === HOME && r.kind === 'theorem').map(r => [r.id, r]));
+  const home = new Map(rows.filter(onTheoryShelf).map(r => [r.id, r]));
   const seen = new Set();
   admissions.forEach((a, i) => {
     const where = `admission ${i + 1}`;
     for (const k of Object.keys(a)) need(FIELDS.has(k), `Unknown field (an admission holds no grade) ${k}: ${where}`);
-    need(home.has(a.id), `No home theorem pin for ${a.id}: ${where}`);
+    need(home.has(a.id), `No theory-shelf pin for ${a.id}: ${where}`);
     need(!seen.has(a.id), `Duplicate admission ${a.id}`);
     seen.add(a.id);
     need(typeof a.admitted === 'string' && /^\d{4}-\d{2}-\d{2}$/.test(a.admitted), `admitted is a date: ${a.id}`);
@@ -45,7 +48,7 @@ export function validateAdmissions(admissions, rows, inventory) {
     need(visibility.get(d.repository) === 'public', `Nonpublic or unlisted dependant repository: ${a.id}`);
     need(text(d.path) && text(d.rule), `The dependant names a path and a rule: ${a.id}`);
   });
-  for (const id of home.keys()) need(seen.has(id), `Home theorem ${id} has no admission record`);
+  for (const id of home.keys()) need(seen.has(id), `Theory-shelf theorem ${id} has no admission record`);
   return admissions;
 }
 
@@ -55,7 +58,7 @@ const cell = s => String(s).replaceAll('|', String.raw`\|`).replaceAll('\n', ' '
 // theorems and their admissions.
 export function renderTheoryIndex(derived, admissions) {
   const byId = new Map(admissions.map(a => [a.id, a]));
-  const home = derived.filter(d => d.row.repo === HOME && d.row.kind === 'theorem')
+  const home = derived.filter(d => onTheoryShelf(d.row))
     .sort((a, b) => a.row.claim.localeCompare(b.row.claim, 'en', {numeric: true}));
   const out = [
     '// SPDX-License-Identifier: CC-BY-SA-4.0',
diff --git a/scripts/site/site.mjs b/scripts/site/site.mjs
index e1bbdb1..da4bc81 100644
--- a/scripts/site/site.mjs
+++ b/scripts/site/site.mjs
@@ -14,7 +14,7 @@
 //     repository fails. A relative link to a repository file that is not in
 //     the site becomes an absolute GitHub link at `main`.
 import {readFileSync, writeFileSync, existsSync, mkdirSync, mkdtempSync, readdirSync, statSync} from 'node:fs';
-import {spawnSync} from 'node:child_process'; // hypatia:ignore js_exec_sync -- argv array, no shell; the program is an absolute path and every argument is a constant or a repository path
+import {spawnSync} from 'node:child_process';
 import {tmpdir} from 'node:os';
 import path from 'node:path';
 
diff --git a/tests/registry/claims-registry.test.mjs b/tests/registry/claims-registry.test.mjs
index 27b12b6..050fddd 100644
--- a/tests/registry/claims-registry.test.mjs
+++ b/tests/registry/claims-registry.test.mjs
@@ -63,6 +63,13 @@ test('validation fails closed', () => {
   expect(() => validate([{...theorem, id: 'o/r#X'}], inv)).toThrow(/repo#claim/);
   expect(() => validate([theorem], [{full_name: 'o/r', visibility: 'private'}])).toThrow(/Nonpublic/);
   expect(() => validate([{...theorem, receipt: {path: 'x', sha256: 'nope'}}], inv)).toThrow(/sha256/);
+  const home = {...theorem, id: 'hyperpolymath/mathesis#T-1', repo: 'hyperpolymath/mathesis', shelf: 'theory'};
+  const homeInv = [{full_name: 'hyperpolymath/mathesis', visibility: 'public'}];
+  expect(validate([home], homeInv)).toHaveLength(1);
+  expect(validate([{...home, shelf: 'applied'}], homeInv)).toHaveLength(1);
+  expect(() => validate([{...home, shelf: undefined}], homeInv)).toThrow(/theory or the applied shelf/);
+  expect(() => validate([{...home, shelf: 'lab'}], homeInv)).toThrow(/theory or the applied shelf/);
+  expect(() => validate([{...theorem, shelf: 'theory'}], inv)).toThrow(/Only a home theorem names a shelf/);
 });
 
 test('only the pinned reader is loaded', async () => {
diff --git a/tests/registry/theory-ledger.test.mjs b/tests/registry/theory-ledger.test.mjs
index e2e8d1a..3030c79 100644
--- a/tests/registry/theory-ledger.test.mjs
+++ b/tests/registry/theory-ledger.test.mjs
@@ -4,7 +4,7 @@
 import {test, expect} from 'bun:test';
 import {readFileSync} from 'node:fs';
 import {validateLedger, snapshot, fold, pending, checkAppendOnly, verifyOffline, jcs, sha256} from '../../scripts/registry/theory-ledger.mjs';
-import {HOME} from '../../scripts/registry/theory.mjs';
+import {onTheoryShelf} from '../../scripts/registry/theory.mjs';
 import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs';
 
 const read = p => readFileSync(new URL(p, import.meta.url), 'utf8');
@@ -12,7 +12,8 @@ const rows = parseJsonl(read('../../docs/atlas/claims/claims.jsonl'));
 const admissions = parseJsonl(read('../../docs/theory/admissions.jsonl'));
 const ledgerText = read('../../docs/theory/ledger.jsonl');
 const ledger = parseJsonl(ledgerText);
-const homeIds = rows.filter(r => r.repo === HOME && r.kind === 'theorem').map(r => r.id);
+// The ledger records the theory shelf only: applied-shelf theorems are not admitted.
+const homeIds = rows.filter(onTheoryShelf).map(r => r.id);
 // The grades the ledger last recorded: grade currency needs the canon reader,
 // so `just registry-check` checks it, not this test.
 const grades = new Map([...fold(ledger)].map(([id, s]) => [id, s.pwg]));
@@ -71,6 +72,6 @@ test('the offline check catches a stale admission, a missing theorem and a lefto
   expect(() => verifyOffline(ledger, rows, [])).toThrow(/has no admission/);
   const state = fold(ledger);
   for (const a of admissions) expect(sha256(jcs(a))).toBe(state.get(a.id).admission_sha256);
-  const unpinned = rows.filter(r => !(r.repo === HOME && r.kind === 'theorem'));
+  const unpinned = rows.filter(r => !onTheoryShelf(r));
   expect(() => verifyOffline(ledger, unpinned, admissions)).toThrow(/no claim pin/);
 });
diff --git a/tests/registry/theory.test.mjs b/tests/registry/theory.test.mjs
index e520e61..a3e9ec6 100644
--- a/tests/registry/theory.test.mjs
+++ b/tests/registry/theory.test.mjs
@@ -4,7 +4,7 @@
 // deterministic.
 import {test, expect} from 'bun:test';
 import {readFileSync} from 'node:fs';
-import {validateAdmissions, renderTheoryIndex, HOME} from '../../scripts/registry/theory.mjs';
+import {validateAdmissions, renderTheoryIndex, onTheoryShelf} from '../../scripts/registry/theory.mjs';
 import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs';
 
 const read = p => parseJsonl(readFileSync(new URL(p, import.meta.url), 'utf8'));
@@ -13,8 +13,8 @@ const inventory = read('../../docs/atlas/census/repos.jsonl');
 const admissions = read('../../docs/theory/admissions.jsonl');
 const [a] = admissions;
 
-test('the committed admissions match the home theorem pins', () => {
-  expect(validateAdmissions(admissions, rows, inventory)).toHaveLength(rows.filter(r => r.repo === HOME && r.kind === 'theorem').length);
+test('the committed admissions match the theory-shelf pins', () => {
+  expect(validateAdmissions(admissions, rows, inventory)).toHaveLength(rows.filter(onTheoryShelf).length);
 });
 
 test('validation fails closed', () => {
@@ -22,21 +22,30 @@ test('validation fails closed', () => {
   bad([], /has no admission record/);
   bad([a, a], /Duplicate admission/);
   bad([{...a, pwg: 'PWG-1'}], /holds no grade/);
-  bad([{...a, id: 'hyperpolymath/mathesis#THY-99'}], /No home theorem pin/);
+  bad([{...a, id: 'hyperpolymath/mathesis#THY-99'}], /No theory-shelf pin/);
   bad([{...a, admitted: 'today'}], /admitted is a date/);
   bad([{...a, theory: ''}], /Missing theory test/);
   bad([{...a, owner: ' '}], /Missing owner test/);
   bad([{...a, dependant: {...a.dependant, repository: 'o/hidden'}}], /Nonpublic or unlisted dependant/);
   bad([{...a, dependant: {...a.dependant, rule: ''}}], /names a path and a rule/);
   bad([{...a, dependant: {...a.dependant, grade: 'x'}}], /Unknown dependant field/);
+  // An applied-shelf theorem needs no admission, and an admission cannot name one.
+  const applied = rows.map(r => (r.id === a.id ? {...r, shelf: 'applied'} : r));
+  expect(validateAdmissions([], applied, inventory)).toEqual([]);
+  expect(() => validateAdmissions([a], applied, inventory)).toThrow(/No theory-shelf pin/);
 });
 
 test('the index is deterministic and takes the grade from the derivation', () => {
-  const home = rows.filter(r => r.repo === HOME && r.kind === 'theorem');
-  const derived = home.map(row => ({row, pwg: 'PWG-1', reasons: [], evidence: row.source_commit}));
+  // Both shelves go in, as in a real derivation; only the theory shelf has
+  // admissions, and only it may reach the index.
+  const home = rows.filter(onTheoryShelf);
+  const applied = rows.filter(r => r.shelf === 'applied');
+  expect(applied.length).toBeGreaterThan(0);
+  const derived = [...home, ...applied].map(row => ({row, pwg: 'PWG-1', reasons: [], evidence: row.source_commit}));
   const view = renderTheoryIndex(derived, admissions);
   expect(renderTheoryIndex([...derived].reverse(), admissions)).toEqual(view);
   expect(view).toContain('`PWG-1`');
   expect(renderTheoryIndex(derived.map(d => ({...d, pwg: 'ungraded'})), admissions)).toContain('`ungraded`');
   expect(view).toContain(`Theorems: ${home.length}.`);
+  for (const r of applied) expect(view).not.toContain(r.id);
 });