hyperpolymath · Nov 11, 2026 · Nov 11, 2026
@@ -104,4 +104,4 @@ bust.contractile-parse-error = "latent"
 
 [provenance]
 contractiles = "intend@89c97164fbff must@b2888ac670fb trust@484d6509ce86 adjust@f7e9bafc614e dust@bdb7dea20424 bust@4de1f1b3bc91"
-descriptiles = "deed@7182c2cc6635 anchor@11df55a6aaeb"
+descriptiles = "deed@7182c2cc6635 anchor@bba9793279e0"
@@ -6,7 +6,7 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 <!-- The region between the ARRIVAL-PACK markers is generated from this
      repo's deed by `just claude-md` — do not hand-edit it. -->
 
-<!-- ARRIVAL-PACK:BEGIN — estate-common @Manifesto:DRAFT-unratified · repo @deed:DEED@7182c2cc6635 ANCHOR@11df55a6aaeb — generated by `just claude-md`, do not hand-edit -->
+<!-- ARRIVAL-PACK:BEGIN — estate-common @Manifesto:DRAFT-unratified · repo @deed:DEED@7182c2cc6635 ANCHOR@bba9793279e0 — generated by `just claude-md`, do not hand-edit -->
 
 # You are in the hyperpolymath estate — orient before acting
 
@@ -79,7 +79,7 @@ Put every question that needs the owner's decision through the selector (the Ask
 - **Golden path** (ANCHOR) — `just check` → Every generated view matches its data: catalogue, census tests, atlas, claims registry, bridges; Every gated proof checks in the pinned Guix shell, with no axiom, Admitted, sorry or postulate in its cone.
 - **State** — phase incubating; maturity experimental. Milestones and next actions: `docs/status/ROADMAP.adoc`.
 
-<!-- ARRIVAL-PACK:END · provenance: DEED@7182c2cc6635 ANCHOR@11df55a6aaeb · Manifesto@DRAFT-unratified · regenerate: `just claude-md` (k9 drift-detects; do not hand-edit above) -->
+<!-- ARRIVAL-PACK:END · provenance: DEED@7182c2cc6635 ANCHOR@bba9793279e0 · Manifesto@DRAFT-unratified · regenerate: `just claude-md` (k9 drift-detects; do not hand-edit above) -->
 
 <!-- Hand-authored (owner, 2026-10-05): kept below the generated region so `just claude-md` does not overwrite it. -->
 ## Estate-Wide Format Migration Directives

@@ -105,7 +105,8 @@ not exist yet, so no bridge is checked against both homes.
 ____
 THY-1, reachability is monotone under additive features, is
 proved in Agda and re-proved in Rocq and Lean. CI checks all three in a
-pinned Guix shell.
+pinned Guix shell. A theorem enters the theory shelf only under a stated
+admission rule, and a generated index lists each one with its dependant.
 ____
 
 How this is implemented::
@@ -117,7 +118,10 @@ The sources are `link:verification/proofs/agda/FeatureReachability.agda[]`,
 `.github/workflows/agda-proof-policy.yml` runs it in the Guix shell pinned by
 `build/channels.scm` and `build/manifest.scm`, with planted controls
 (`tests/proofs/gate_controls_test.sh`). CI run 43057783538 on `main` at
-`b2cf524` passed. See the <<proof-ledger>>.
+`b2cf524` passed. See the <<proof-ledger>>. The admission rule is in
+`link:docs/theory/README.adoc[]`; `link:scripts/registry/theory.mjs[]` checks
+each record in `docs/theory/admissions.jsonl` against the claim pins and
+renders `docs/theory/generated/index.adoc` with the grade the registry derives.
 
 Caveat::
 The proof is about a graph model. That the model matches Cargo's feature
@@ -193,15 +197,6 @@ badges on a public repository. The README carries none, because no Best
 Practices project identifier is recorded for Mathesis.
 ====
 
-[CAUTION]
-====
-Template example proofs: `verification/proofs/idris2/`,
-`verification/proofs/tlaplus/`, `verification/proofs/agda/Properties.agda`,
-`verification/proofs/coq/TypeSafety.v` and
-`verification/proofs/lean4/ApiTypes.lean` come from the RSR template. They
-are not Mathesis obligations. WO 4.1 of the re-anchoring plan removes them.
-====
-
 [CAUTION]
 ====
 Contract probes: the `must` contract states six Mathesis invariants with
@@ -223,7 +218,7 @@ guard and the public frame (8 test files, all passed on 2026-11-11)
 |View determinism, row validation, the public frame (13 tests)
 
 |`tests/registry/`
-|Registry derivation through fixture receipts (14 tests)
+|Registry derivation through fixture receipts, and the admissions of the theory shelf (17 tests)
 
 |`tests/proofs/gate_controls_test.sh`
 |A planted `postulate`, `Admitted` and `sorry` each fail the proof gate (CI)
@@ -271,7 +266,7 @@ and `_⊔_` as builtins.
 |open
 |-
 |`docs/proposals/mathesis-research-programme.adoc`
-|Not yet stated in a prover (WO 4.1)
+|Not yet stated in a prover (next on the theory shelf)
 |===
 
 Proofs: 3 proven of 5; 1 argued, 1 open. The registry derives `PWG-1` for

@@ -30,7 +30,8 @@ describes what is proved, where, and how strongly.
   repositories, generated into one view.
 * *Home theory.* THY-1, reachability is monotone under additive features, is
   proved in Agda and re-proved in Rocq and Lean. CI checks all three in a
-  pinned Guix shell.
+  pinned Guix shell. A theorem enters the theory shelf only under a stated
+  admission rule, and a generated index lists each one with its dependant.
 * *Applied systems.* Methods that apply mathematics to decisions, starting
   with accounting and finance. Design documents only so far.
 * *Privacy by count.* The frame names public repositories only. The number of
@@ -39,7 +40,7 @@ describes what is proved, where, and how strongly.
 [NOTE]
 .Planned
 ====
-The theory shelf's admission rule and the token-lattice theorems, the applied
+The token-lattice theorems of the theory shelf, the applied
 shelf tied to the evidence rules, a published atlas, receipts in more home
 repositories, and a scheduled census. See
 link:docs/status/ROADMAP.adoc[the roadmap].
@@ -90,6 +91,10 @@ records (`claims/`), and generated views (`generated/`)
 |`verification/receipts/`
 |The proof receipt of Mathesis
 
+|`docs/theory/`
+|The theory shelf: the admission rule, the admission records and the
+generated theorem index
+
 |`applied-systems/`
 |The applied shelf
 

@@ -223,13 +223,6 @@ your own repo - but do not read their emptiness as neglect here.
 | `docs/reports/performance/`
 | `docs/reports/quality/`
 | `docs/reports/security/`
-| `docs/theory/`
-| `docs/theory/computing/`
-| `docs/theory/formalisms/`
-| `docs/theory/mathematics/`
-| `docs/theory/ontologies/`
-| `docs/theory/other/`
-| `docs/theory/socio-technical/`
 | `docs/whitepapers/academic/`
 | `docs/whitepapers/industry/`
 | `examples/`

@@ -33,7 +33,7 @@ watch)
 ladder, starting with the chain of PROOF-POLICY §5. Ruling D-10 puts their
 home in Mathesis.
 |Agda, re-checked in Rocq and Lean
-|Open (WO 4.1)
+|Open (next on the theory shelf)
 |Statements: `docs/proposals/mathesis-research-programme.adoc`
 
 |To be allocated
@@ -46,16 +46,9 @@ home in Mathesis.
 No Mathesis obligation concerns an ABI or an FFI: since WO 3.2 the deed
 declares neither capability.
 
-[NOTE]
-.Template example proofs
-====
-`verification/proofs/idris2/`, `verification/proofs/tlaplus/`,
-`verification/proofs/agda/Properties.agda`,
-`verification/proofs/coq/TypeSafety.v` and
-`verification/proofs/lean4/ApiTypes.lean` come from the RSR template. They
-are examples, not Mathesis obligations. WO 4.1 of the re-anchoring plan
-removes them.
-====
+The template example proofs of the RSR template (Idris2, TLA+, and one
+example each for Agda, Rocq and Lean) were removed in WO 4.1 of the
+re-anchoring plan. They were never Mathesis obligations.
 
 == Banned patterns
 

@@ -18,7 +18,7 @@ reader of PROOF-POLICY §8.5.1.
 |`PWG-1`
 |The receipt `verification/receipts/theory_praxis.deed`; the record below
 
-|The token-lattice theorems (WO 4.1)
+|The token-lattice theorems (next on the theory shelf)
 |Open
 |-
 |Not yet stated in a prover
@@ -31,8 +31,7 @@ reader of PROOF-POLICY §8.5.1.
 
 *Overall*: 1 of 3 obligations discharged; 2 open. These are counts, not a
 percentage: PROOF-POLICY §8 grades are derived from receipts and are never
-flattened. The template example proofs are not obligations (see
-link:PROOF-NEEDS.adoc[PROOF-NEEDS]).
+flattened. The template example proofs were removed in WO 4.1.
 
 == Theory theorems
 

@@ -85,7 +85,7 @@ public repository is not reached
 |D
 |alpha-unstable
 |CI passes with controls; THY-1 at `PWG-1` in three provers
-|A dogfood log; the template example proofs still sit in the gate (WO 4.1)
+|A dogfood log
 |===
 
 The applied shelf (`applied-systems/`) is not graded: it holds design

@@ -145,6 +145,20 @@ One pull request that changes census rows is open at a time (atlas README,
 ** The merge that joined WO 3.2 and WO 3.5 dropped two entries of
    `(variant (paths :diverged))`. WO 3.4 restores them.
 
+=== Re-anchoring: stage 4 (2026-11-11)
+
+* WO 4.1, the theory shelf: `docs/theory/README.adoc` states the admission
+  rule. `docs/theory/admissions.jsonl` holds one authored record for each
+  home theorem; `claims-registry.mjs` checks it against the claim pins and
+  generates `docs/theory/generated/index.adoc`. All template example proofs
+  and the six template stubs under `docs/theory/` are removed (owner rulings
+  2026-11-11).
+* Next, by owner ruling: an append-only ledger of the theory work, written
+  only by a `just theory-ledger` recipe and checked in CI, in its own pull
+  request.
+* Finding: the `intend` contract still marks stage 3 `in_progress` and
+  stage 4 `declared`; a contract edit needs owner review.
+
 [[stages]]
 == Stages
 
@@ -173,14 +187,14 @@ gate gap, Agda, Rocq and Lean in CI, the receipt of Mathesis
 |3
 |Tell the truth: deed, capabilities, contracts, entry documents, no private
 names, affirmation
-|In progress: WO 3.1, 3.2, 3.3 and 3.5 merged; WO 3.4 in review; WO 3.6
-next
+|Done: WO 3.1 to 3.6 merged (pull requests 73 to 78); the affirmation
+anchors `c81cb84`
 
 |4
 |The three shelves: the theory admission rule and the token-lattice
 theorems, the applied shelf tied to the evidence spine, the published atlas
 (needs a ruling)
-|Declared
+|In progress: WO 4.1 in review
 
 |5
 |Scale: receipts in the home repositories, the bridge lock pilot, a

@@ -1,3 +1,63 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= theory Unit
+= The theory shelf
+
+The theory shelf holds the theorems whose home is Mathesis: theory that an
+estate rule, vocabulary or interface depends on, and that no single system
+owns. The other two shelves are the atlas (`docs/atlas/`) and the applied
+systems (`applied-systems/`).
+
+== The admission rule
+
+A theorem enters the shelf only when all three conditions hold:
+
+. *It is theory* by the test of
+  https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[PROOF-POLICY]
+  §1. A statement that names a type, function or wire format of one
+  repository is engineering, and belongs to that repository. A statement
+  that would be true of any implementation is theory.
+. *No single system owns it.* A theorem about one system's own behaviour
+  lives in that system's repository.
+. *An estate rule, vocabulary or interface depends on it,* and the record
+  names that dependant.
+
+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/`.
+
+== Where the records are
+
+[cols="1,3",options="header"]
+|===
+|Path |Contents
+
+|`admissions.jsonl`
+|One authored admission record for each theorem: why it is theory, why no
+single system owns it, and the dependant (repository, path and rule). It
+holds no grade.
+
+|`generated/index.adoc`
+|The theorem index, generated by `scripts/registry/claims-registry.mjs` from
+the admission records, the claim pins and the receipt. Never edit it by hand.
+
+|`../../verification/proofs/`
+|The Agda, Rocq and Lean sources.
+
+|`../../verification/receipts/theory_praxis.deed`
+|The proof receipt of Mathesis (PROOF-POLICY §8.5.1).
+|===
+
+`just registry-check` (part of `just check`) fails when the index is stale,
+when a home theorem has no admission record, or when an admission names no
+dependant, a non-public dependant repository, or a theorem with no claim
+pin.
+
+== Admitting a theorem
+
+. State the theorem, prove it in Agda, and re-prove it in Rocq and Lean.
+. Add each leg to the receipt, from observed checker runs.
+. Pin the claim in `docs/atlas/claims/claims.jsonl`.
+. Add its admission record to `admissions.jsonl`.
+. Run `bun scripts/registry/claims-registry.mjs build`, then `just check`.
+
+The token-lattice theorems are the next candidates (ruling D-10). Their
+statements are in `docs/proposals/mathesis-research-programme.adoc`.
@@ -0,0 +1 @@
+{"admitted":"2026-11-11","dependant":{"path":"docs/UPSTREAM-DEPENDENCY-WATCH.adoc","repository":"metadatastician/standards","rule":"Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build."},"id":"hyperpolymath/mathesis#THY-1","owner":"No single system owns it: it describes the feature resolution that any Cargo workspace exhibits, and Cargo is third-party.","theory":"It names no type, function or wire format of one repository: it holds for any dependency graph whose edges are guarded by features closed under Horn rules (PROOF-POLICY §1)."}
@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// GENERATED by scripts/registry/claims-registry.mjs from docs/theory/admissions.jsonl,
+// docs/atlas/claims/claims.jsonl and the receipt they pin; do not hand-edit.
+= Theorem index of the theory shelf
+
+One row for each theorem whose home is Mathesis. The grade is derived from
+the receipt by the canon reader, never typed. The admission rule is in
+link:../README.adoc[the theory README].
+
+Theorems: 1.
+
+[cols="1,3,1,2,3",options="header"]
+|===
+|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. |`PWG-1` |`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.
+
+|===
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		{"admitted":"2026-11-11","dependant":{"path":"docs/UPSTREAM-DEPENDENCY-WATCH.adoc","repository":"metadatastician/standards","rule":"Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build."},"id":"hyperpolymath/mathesis#THY-1","owner":"No single system owns it: it describes the feature resolution that any Cargo workspace exhibits, and Cargo is third-party.","theory":"It names no type, function or wire format of one repository: it holds for any dependency graph whose edges are guarded by features closed under Horn rules (PROOF-POLICY §1)."}