registry: pin THY-1 and APP-1 to APP-4 at the receipt on main; shelf field

.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: |

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
 

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"}

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`) |—
 

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.

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.

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

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

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
 

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.
 
 |===