diff --git a/README.adoc b/README.adoc index 19b238e6..f3a29f50 100644 --- a/README.adoc +++ b/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 diff --git a/docs/ARCHITECTURE.adoc b/docs/ARCHITECTURE.adoc index 44cce316..7c173741 100644 --- a/docs/ARCHITECTURE.adoc +++ b/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. diff --git a/docs/architecture.adoc b/docs/architecture.adoc index e99f95ac..af4cb4b6 100644 --- a/docs/architecture.adoc +++ b/docs/architecture.adoc @@ -1,79 +1,66 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -// 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]. diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index f9a68310..d28ba7e4 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/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/` diff --git a/estate-mathematical-architecture b/docs/proposals/estate-mathematical-architecture.adoc similarity index 91% rename from estate-mathematical-architecture rename to docs/proposals/estate-mathematical-architecture.adoc index 65c7f3f3..daf1f882 100644 --- a/estate-mathematical-architecture +++ b/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? +.... diff --git a/docs/standards/AUTHORITY.adoc b/docs/standards/AUTHORITY.adoc new file mode 100644 index 00000000..c92e711f --- /dev/null +++ b/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. diff --git a/docs/standards/README.adoc b/docs/standards/README.adoc index b31c112c..a138714a 100644 --- a/docs/standards/README.adoc +++ b/docs/standards/README.adoc @@ -1,3 +1,9 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= 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.