docs: reconcile Mathesis architecture and standards ownership

README.adoc

@@ -11,10 +11,19 @@ Proofs stay in their home repositories. mathesis points at them. Later it
 will also hold the Agda sources for theory that has no other natural home.
 
 The rules for where a proof *should* live are not here: they are
-`standards/3-practice/PROOF-POLICY.adoc` (Creusot for Rust, SPARK for Ada,
+https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[the canonical standards/3-practice/PROOF-POLICY.adoc] (Creusot for Rust, SPARK for Ada,
 Idris2 for APIs, ABIs and engineering properties, Agda for theory rechecked
 in Rocq and Lean). The working method is the proof-craft skill.
 
+== Where authority lives
+
+* link:docs/standards/README.adoc[Standards and authority map] — estate proof policy, proof/test evidence ownership, and Mathesis's limits.
+* link:docs/atlas/README.adoc[Discovery atlas] — the current generated, read-only first slice (repository index, not theorem-level certification).
+* link:docs/proposals/estate-mathematical-architecture.adoc[Estate mathematical architecture proposal] — the original long-term design brief, preserved but *not ratified*. Its proposed proof grades do not override the standards policy.
+* link:docs/architecture/REPOSITORY-MAP.adoc[Generated repository map] — current path inventory, not the mathematical architecture specification.
+
+Mathesis references proofs in their home repositories. A census row or a green CI badge does not independently verify a theorem. Pin claims to source commits, checker versions, assumptions and verification receipts; report missing or inaccessible evidence explicitly.
+
 == What is here
 
 [cols="1,3"]
@@ -76,8 +85,7 @@ The first census covered 476 repositories:
 * Theorem-level rows for the theory repos: statement, Agda source, Rocq
   leg, Lean leg, route.
 * A scheduled CI job that reruns the census and fails on catalogue drift.
-* A deed (`mathesis_chora.deed`) once the repo is instantiated from the RSR
-  template.
+* Reconcile the existing `mathesis_chora.deed` with the current estate conventions; it is already present, not a future placeholder.
 
 == Licence
 

docs/ARCHITECTURE.adoc

@@ -1,48 +1,8 @@
-= Architecture
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Architecture — Mathesis (compatibility pointer)
 
-== Overview
+This path previously contained a generic RSR scaffold architecture description. The maintained Mathesis-specific description is link:architecture.adoc[docs/architecture.adoc]. It distinguishes the implemented proof census and generated atlas from proposed theorem-level indexing and verification.
 
-This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability.
+For actual paths consult link:architecture/REPOSITORY-MAP.adoc[the generated repository map]. For estate-wide proof policy use link:standards/README.adoc[the canonical standards routing guide]. The original longer design brief is now link:proposals/estate-mathematical-architecture.adoc[an explicitly unratified proposal].
 
-== Directory Structure
-
-[source]
-----
-.
-├── src/           # Source code
-├── tests/        # Test suites
-├── docs/         # Documentation
-├── scripts/      # Utility scripts
-├── config/       # Configuration files
-├── LICENSE       # License file
-├── LICENSES/     # Full license texts
-└── README.adoc   # Project documentation
-----
-
-== Design Principles
-
-* *Separation of Concerns*: Each module has a single responsibility
-* *Testability*: Code is written to be easily testable
-* *Documentation*: All public APIs are documented
-* *Configuration*: Environment-specific settings are externalized
-
-== Dependencies
-
-* External dependencies are minimized and clearly declared
-* Version pinning is used for reproducibility
-
-== Security Considerations
-
-* Sensitive data is never committed to the repository
-* Secrets are managed through environment variables or secure vaults
-* Regular dependency audits are performed
-
-== Maintainability
-
-* Code follows consistent style guidelines
-* Pull requests require review and CI checks
-* Issues and discussions are tracked transparently
-
----
-
-_Last updated: 2026-07-18_
+The path is retained for old references; it is not a second architecture authority.

docs/architecture.adoc

@@ -1,79 +1,66 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
-= Architecture — Mathesis
-:revdate: 2026-MM-DD
+= Mathesis architecture — implemented boundaries
+:revdate: 2026-11-01
 
-== System overview
+== Purpose
 
-One paragraph: what this project does and what it does not do. State the
-*invariant* — the property that, if violated, would make the whole project
-pointless. Future maintainers will read this paragraph first.
+Mathesis is the estate's mathematical source-discovery and proof-orientation index. It is *not* a theorem prover, a universal proof-status authority, or a replacement for the mathematics in individual repositories. The linked source repository, pinned revision and actual proof checker determine the status of a theorem; Mathesis cannot infer that status from a file count or a passing badge.
 
-== Component diagram
+== Implemented data flow
 
-Replace this section with an ASCII or Mermaid diagram. Keep it under 20
-lines — anything bigger belongs in `architecture/`.
-
-[source]
+[source,text]
 ----
-+------------------+      +------------------+
-|   Component A    | ---> |   Component B    |
-+------------------+      +------------------+
-         |
-         v
-+------------------+
-|   Component C    |
-+------------------+
+Repository census input (docs/catalogue/census/repos.json)
+  -> scripts/census/ (source and prover-file discovery)
+  -> corpus counts, holes/unsafe candidates, reachability observations
+  -> docs/catalogue/census/catalogue-rows.json
+  -> generated docs/catalogue/catalogue.adoc
+  -> scripts/atlas/census-atlas.mjs
+  -> docs/atlas/generated/ (A-Z, class, owner; index.json)
+  -> lookup and bounded context-pack commands
 ----
 
-== Data flow
+The census counts and classifies observed files. It does not establish that Agda, Rocq, Lean, Idris2, SPARK or other proofs have passed. The atlas is generated from the census rows; it does not invent theorem identities, independent witnesses or semantic equivalences. Private or unreachable sources must not be treated as having no mathematics, and private metadata must not be published.
 
-For each external input, describe:
+== Sources of authority
 
-* **Source**: where it comes from.
-* **Validation**: what guarantees we enforce on entry.
-* **Transformation**: high-level processing stages.
-* **Sink**: where the result goes.
+[cols="1,3",options="header"]
+|===
+| Question | Owning source
 
-== Key invariants
+| Proof policy and accepted checking discipline
+| https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[canonical standards PROOF-POLICY]
 
-Enumerate the load-bearing invariants of the system. Each should have:
+| Mathematical claims and formal witnesses
+| Home mathematical repository at a concrete revision, with actual proof-checker outputs and assumptions
 
-. A one-line statement.
-. The code location(s) that enforce it.
-. The failure mode if the invariant is violated.
+| Census and derived atlas views
+| link:catalogue/catalogue.adoc[Mathesis census] and link:atlas/README.adoc[atlas declaration of scope]
 
-Example:
+| General test evidence and fixture requirements
+| https://github.com/hyperpolymath/proven-tests-and-benches[proven-tests-and-benches] and the canonical estate testing policy
 
-[cols="1,2,2,2", options="header"]
-|===
-| # | Invariant | Enforced at | Failure mode
+| Repository paths and intended shape
+| link:architecture/REPOSITORY-MAP.adoc[generated repository map]
 
-| 1
-| All HTTP requests carry a valid `X-Request-ID`.
-| `src/request_id.rs`
-| Logs become unjoinable; correlation breaks.
-
-| 2
-| The output buffer is always flushed before exit.
-| `src/main.rs:88-92` (Drop impl)
-| Last ~16KB of log lost on crash.
+| Proposed future architecture
+| link:proposals/estate-mathematical-architecture.adoc[unratified design brief]
 |===
 
-== Dependencies
+See link:standards/README.adoc[the authority map] for migration and conflict rules.
+
+== Explicitly not implemented by this document
 
-* **Internal**: list other hyperpolymath repos this depends on.
-* **External**: SHA-pinned (see `Cargo.lock` / `.lock` / etc.).
-* **Build-time**: tools required to build (just, , cargo, …).
+A theorem-level registry with verified cross-prover translations; automatic proof correspondence; causal/semantic identity of theorems across forks; a mandatory database architecture; full-estate incremental rescanning; or an agent write-back system are *not* established merely by this architecture description. They remain independently reviewable proposals requiring evidence and acceptance tests.
 
-== Out of scope
+== Invariants and failure conditions
 
-Explicit non-goals. Things we deliberately do *not* do, with a one-line
-reason for each. This section saves more time than the rest combined.
+* *No source, no theorem certification.* A file containing a prover language is a discovery result, not a successful verification receipt.
+* *No authority duplication.* A local Mathesis proposal cannot revise `metadatastician/standards` policy.
+* *No invisible drift.* A generated atlas must be reproducible from its indexed census input and named script.
+* *No false negatives from inaccessible sources.* Unreachable and private observations remain marked unknown, not empty.
+* *No source loss through indexing.* Aggregating counts is a declared lossy view; it must never be mistaken for evidence identifying a particular theorem.
 
-== See also
+== Related
 
-* link:./usage.adoc[Usage] — consumer perspective.
-* link:./contributing.adoc[Contributing] — developer setup.
-* link:./decisions/[ADRs] — historical record of why this shape.
+link:../README.adoc[Mathesis README] · link:atlas/README.adoc[Atlas] · link:standards/README.adoc[Standards pointer] · link:architecture/REPOSITORY-MAP.adoc[Repository map].

docs/architecture/REPOSITORY-MAP.adoc

@@ -221,7 +221,6 @@ your own repo - but do not read their emptiness as neglect here.
 | `docs/reports/performance/`
 | `docs/reports/quality/`
 | `docs/reports/security/`
-| `docs/standards/`
 | `docs/theory/`
 | `docs/theory/computing/`
 | `docs/theory/formalisms/`

estate-mathematical-architecture → docs/proposals/estate-mathematical-architecture.adoc

@@ -1,3 +1,14 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Estate-wide Mathematical Knowledge Architecture — working proposal
+
+Status: *unratified architectural brief*. Preserved from the former Mathesis root file `estate-mathematical-architecture` for discoverability and historical provenance. It is not the adopted architecture, a verified implementation plan, or a source of estate-wide proof grades.
+
+The controlling estate proof policy lives at https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[PROOF-POLICY]. Mathesis's live census and first atlas slice are described in link:../../README.adoc[the README] and link:../atlas/README.adoc[the atlas README]. In particular, any conflicting grade definitions, tool flags, integration claims, or proposed storage arrangements below require explicit review, not silent adoption.
+
+== Original working brief (preserved)
+
+[literal]
+....
 MATHESIS — Estate-wide Mathematical Knowledge Architecture
 
 Mission
@@ -135,3 +146,4 @@ Do not build a new theorem prover or a custom graph database unless strictly req
 Produce a substantial report detailing the current limitations, the recommended schema, the exact relationship to tools like gv-clade-index and AXLE, a phased roadmap, and the execution results of the Dogfooding experiments.
 
 Finish with a clear answer to: What can a completely unfamiliar mathematical researcher or coding agent now discover, verify, and understand using Mathesis that they could not reliably discover before?
+....

docs/standards/AUTHORITY.adoc

@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+= Mathesis authority routing: policy, proofs, and evidence
+
+Mathesis is a discovery and proof-orientation system, not a second estate standards authority. This directory is an index of the standards that govern its work, not a copied policy tree.
+
+== Authority by responsibility
+
+* *Estate-wide proof and verification policy*: https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[metadatastician/standards — PROOF-POLICY]. This owns the permitted trust classes, proof languages, and requirements for proof claims. Follow the standards repo's own versioning and pinned revision when verifying a historical result.
+* *Estate-wide test policy*: https://github.com/metadatastician/standards/tree/main/3-practice/testing-and-benchmarking[testing and benchmarking] and https://github.com/metadatastician/standards/blob/main/3-practice/ZIGZAG-TESTING.adoc[Zigzag testing].
+* *Repository-local mathematical architecture*: link:../atlas/README.adoc[Mathesis atlas], link:../catalogue/catalogue.adoc[existing proof census], and link:../../README.adoc[Mathesis README]. Mathesis may propose proof-index schemas and navigation views; a proposed ranking never becomes estate policy by appearing here.
+* *Individual theorem truth and proof obligations*: the theorem's home repository, its exact source revision and its kernel-check receipts. A census row, index, file count, or interpreted dependency is not a proof.
+* *Implementation assurance*: https://github.com/hyperpolymath/proven-tests-and-benches[proven-tests-and-benches] owns reusable test evidence and fixture doctrine; https://github.com/hyperpolymath/cicd-suite[cicd-suite] owns executable assurance gates. The status of a CI job is not automatically a theorem verification result.
+
+== Distinguish proposals from decisions
+
+The root link:../proposals/estate-mathematical-architecture.adoc[estate-mathematical-architecture] is an *unratified architecture brief*, preserved for provenance. In particular, its proposed proof grades, indexing/storage design, and implementation stages are not replacements for the canonical PROOF-POLICY or for the current census implementation.
+
+The generic RSR architecture files under `docs/` reflect template lineage and should not be treated as independent Mathesis standards. If local documentation and estate policy disagree, record the conflict, the source revisions, and the required decision; do not silently make either one authoritative.
+
+== Evidence contract
+
+A discoverable proof record should eventually state: theorem identity and meaning; home repository and commit; checker and version; invocation and safe-mode options; assumptions and trusted base; completed, failed, skipped or unavailable verification status; source receipts; and whether a purported cross-system witness is independently checked or merely proposed. Never infer missing fields from a green badge.
+
+A2ML was retired for new estate-wide declarations in favour of DEED and current canonical formats. Historical .a2ml records may remain as archival evidence, not as an excuse to create new competing canonical files.
+
+This document is a routing guide, not a modification of any upstream rule.

docs/standards/README.adoc

@@ -1,3 +1,9 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= Standards Unit
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+= Mathesis standards directory
+
+This directory is *not* a second copy of the estate standards.
+
+Read link:AUTHORITY.adoc[the authority routing guide] for the boundary between Mathesis proposals and the canonical https://github.com/metadatastician/standards[estate standards], plus the ownership of proof and test evidence.
+
+Mathematical claims and formal proof receipts remain in the source repositories. The local mathematical census and atlas are indexes, not standards or certificates.