From 77b49de43ae2b33e6c4a667800de7a0fe4b145a3 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:07:17 +0000 Subject: [PATCH 01/12] docs(mathesis): identify canonical proof policy and separate architecture brief --- docs/standards/README.adoc | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/docs/standards/README.adoc b/docs/standards/README.adoc index b31c112c..e2988588 100644 --- a/docs/standards/README.adoc +++ b/docs/standards/README.adoc @@ -1,3 +1,26 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= Standards Unit += Mathesis standards and architectural authority + +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:../../estate-mathematical-architecture[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. From ee850a13a0efb733360bd22b7d2802de730085a2 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:08:03 +0000 Subject: [PATCH 02/12] docs(mathesis): archive unratified architecture brief under proposals --- .../estate-mathematical-architecture.adoc | 149 ++++++++++++++++++ 1 file changed, 149 insertions(+) create mode 100644 docs/proposals/estate-mathematical-architecture.adoc diff --git a/docs/proposals/estate-mathematical-architecture.adoc b/docs/proposals/estate-mathematical-architecture.adoc new file mode 100644 index 00000000..daf1f882 --- /dev/null +++ b/docs/proposals/estate-mathematical-architecture.adoc @@ -0,0 +1,149 @@ +// 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 +Re-evaluate and substantially improve the architecture of hyperpolymath/mathesis. Mathesis is intended to become the mathematical knowledge commons, proof-discovery atlas, and research-orientation system for a large, heterogeneous, multi-organisation software estate. + +It must serve humans, researchers, mathematicians, developers, coding agents, theorem-proving agents, and automated verification systems. The objective is to map out exact proof states, track translation pipelines across distinct logical foundations, and eliminate dependence on the owner's memory without turning Mathesis into a monolithic proof repository. The original repositories remain the sovereign territory of their own mathematics. + +1. Mandatory Initial Audit +Read the actual Mathesis repository before proposing changes. Start with README.adoc, docs/catalogue/catalogue.adoc, the scripts/census/ tools, the repository deed, and relevant CI workflows. + +Distinguish genuine architectural limits from deliberate simplifications. + +Do not discard the working census or its reproducibility simply to create a more elaborate directory layout. + +2. Estate Discovery, Authority, and Incremental Indexing +Mathesis must discover repositories across relevant owners, forges, and mirrors. Determine which source is authoritative for repository identity, clade/lineage (e.g., gv-clade-index), project membership, and verification receipts. + +The "Cold Start" Protocol: The indexing architecture must support incremental caching. A single repository push must update its own sub-graph and theorem states without forcing a multi-hour rebuild of the entire 400+ repository estate. + +Identity: Do not become a competing canonical registry for identities already owned by gv-clade-index. Use stable identifiers, aliases, and source pointers. + +3. Scope of Mathematical and Engineering Material +A repository need not contain a .agda or .lean file to belong in Mathesis. Discover mathematics appearing in compilers, databases, knot theory, topological simulations, and game engines. + +The estate explicitly divides into a Theory Path and an Engineering Path. Mathesis must track both: + +Theory Path: Pure mathematical formulation, topological proofs, and strict foundational verification (Agda, Rocq/Coq, Lean 4, Isabelle/HOL). + +Engineering Path: Applied invariants and bounded runtime verification. Mathesis must track: + +Idris2: For verified ABIs and strict type-driven design boundaries. + +Rust (Creusot) & Ada (SPARK): For memory-safe, mission-critical systems. (Note: These compile to the Why3 intermediate verification language. If Why3's automated SMT solvers fail, the resulting proof witnesses must be exported to Rocq or Isabelle for manual closure). + +Experimental Engineering Verification: Recognize and track early-stage verification bounds for newer languages. This specifically includes Apodeixi.jl (Julia for data), quintessence (Elixir for web/concurrency/fault tolerance), atoma (Zig for FFIs/APIs), and bactrian (OCaml for compilers and data processing). + +4. Navigation Views +Provide four complementary, generated navigation views: + +A. Alphabetical Mathematical Atlas: A–Z index of concepts, definitions, and aliases linking to their source proofs. + +B. Mathematical Subject Hierarchy: Standardized classifications (e.g., MSC2020) for interdisciplinary work. + +C. Project and Research Clusters: Navigable clusters spanning repositories (e.g., FSinFS, Echo/epistemic research, QuandleDB, eNSAID). + +D. Estate and Provenance View: Browse by organization, proof assistant, verification grade, and maturity status. + +5. The Verification Pipeline: Graded Proof Architecture +Mathesis must rigorously categorize theorems through a strict verification grading system. This tracks a proof from iterative theory down to API-verified cross-system certainty. + +Grade 3 (Iterative & Tentative Formulation): Prototyped and iteratively constructed in Agda. This relies on strict solver flags (e.g., --safe --erasure) or topological geometry (e.g., Full --cubical for knot/Conway problems). A proof is Grade 3 if it type-checks locally in Agda but has not been translated to an independent foundational system. + +Grade 2 (Proof Witness Translation): The Agda proof is translated into a highly rigid, independent foundational proof language. + +Grade 2i (Single Translation): The proof witness is translated to ONE alternative foundational system (e.g., Lean 4 or Rocq). + +Grade 2ii (Dual Translation for High-Assurance): The proof witness is translated into TWO fundamentally distinct logical architectures. Note on Prover Families to avoid foundational blind spots: Agda, Rocq, and Lean 4 all belong to the Dependent Type Theory (DTT) / Calculus of Inductive Constructions family. To achieve true foundational diversity for a Grade 2ii theorem, the second translation must target a non-DTT system like Isabelle/HOL (which relies on Higher-Order Logic/LCF-architecture). + +Grade 1 (Machine-Checked via Verified API): The translated proof witnesses successfully compile in headless, isolated CI environments via verified checker APIs. This requires passing the Axiom Lean Engine (AXLE) API for Lean 4, isabelle server instances for Isabelle/HOL, or internal coq-lsp REST APIs for Rocq. + +6. Epistemic Precision, Versioning, and Deprecation +Do not flatten proof confidence into a percentage. Record exactly whether a result is Open, Claimed, Grade 3, Grade 2i/ii, or Grade 1. + +Axiom Tracking: Track whether a result depends on unverified postulates, #print axioms (Lean), Print Assumptions (Rocq), or pinned library versions. + +Versioning and Regressions: A theorem proven in commit A may break in commit B. Mathesis must track the exact Git commit hash of the verification receipt. Introduce Superseded and Regressed statuses to flag previously Grade 1 proofs that no longer compile against the HEAD of their source repositories. + +7. Search, Access Control, and Knowledge Retrieval +Use the simplest useful working architecture (e.g., Canonical versions → deterministic generated SQLite/FTS5 index). + +Access Boundaries & Row-Level Security: Do not treat a private repository as absent merely because the scanner cannot read it. Conversely, the index query layer must enforce access-control natively (e.g., via clearance tokens or segregated databases) so that a public Mathesis catalog never leaks private repository titles, theorem statements, or WIP mathematical metadata. + +8. Agent Interfaces and Write-Back Correction +Design a stable entry point for coding agents (e.g., "Orient me to the mathematical estate," "Prepare a token-budgeted context pack"). + +LLM Hypothesis Tagging: Any missing mathematical bridge or dependency suggested by an LLM must be strictly tagged as LLM-Hypothesized (Unverified). + +Correction Pipeline: Agents must not have direct write-access to mutate the canonical SQLite index. Provide a strict "write-back" or "nomination" API where agents can submit discovered broken links, missing verification receipts, or false positives for human or CI-gated review. + +9. Dogfooding Investigations +Build and measure at least three substantive experiments to prove the architecture: + +Experiment A (FSinFS): Discover existing theorems, trace them through the pipeline, and output missing proof obligations. + +Experiment B (Quandles & Knots): Connect abstract KnotTheory.jl ideas to Full Cubical Agda topological foundations. + +Experiment C (Cross-Boundary Proof Identity): Verify that Mathesis correctly maps a Grade 3 Agda specification to a Grade 1 Lean/Isabelle proof witness, and connects both to their engineering implementations (e.g., Rust/Creusot). + +10. Directory and Repository Architecture +Develop and evaluate candidate architectures. Consider a structure like: + +registry/ — Canonical records and Grade 1-3 receipts. + +schemas/ — Validated record schemas. + +docs/atlas/ — Generated A-Z, subject, project, and estate views. + +tools/ — Extraction, validation, and incremental indexing logic. +Keep original proofs in their respective home repositories. + +11. Licensing, Reproducibility, and Trust +Use MPL-2.0. Do not copy entire external mathematical libraries or papers merely to index them; prefer source references. Reject silent index drift, duplicate proof inflation, and false positive verification claims. The system should report unresolved or unavailable evidence plainly. + +12. Delivery Stages +Stage 0: Ground-truth audit and CI review. + +Stage 1: Architecture and schema decision. + +Stage 2: Minimal working catalog (small vertical slice with generated views). + +Stage 3: Estate discovery with incremental refresh. + +Stage 4: Proof-level indexing (extracting Grade 1-3 statuses and assumptions). + +Stage 5: Retrieval evaluation (execute Dogfooding experiments). + +Stage 6: Agent interoperability (read APIs and write-back nomination). + +Stage 7: Wider mathematical atlas (external links and unformalized concepts). + +13. What Not To Do +Do not replace the current working census with an unfinished system. + +Do not assume all mathematics is located in .agda or .lean files. + +Do not invent missing repository identities or mathematical relationships to create a tidy taxonomy. + +Do not allow agent-generated evidence to count as independent corroboration. + +Do not treat embedding similarity as mathematical equivalence. + +Do not build a new theorem prover or a custom graph database unless strictly required by performance bottlenecks. + +14. Required Final Handover +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? +.... From a8e5f5872fd74b8d2ed4b02dbe529defa659ca3b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:08:27 +0000 Subject: [PATCH 03/12] docs(mathesis): point authority map to archived proposal --- docs/standards/README.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/standards/README.adoc b/docs/standards/README.adoc index e2988588..3135af75 100644 --- a/docs/standards/README.adoc +++ b/docs/standards/README.adoc @@ -13,7 +13,7 @@ Mathesis is a discovery and proof-orientation system, not a second estate standa == Distinguish proposals from decisions -The root link:../../estate-mathematical-architecture[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 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. From 2f5b59365bf96a4291e775f99fab1e82807f788e Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:08:31 +0000 Subject: [PATCH 04/12] docs(mathesis): make current atlas, policy authority, and proposals discoverable --- README.adoc | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) 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 From d25d2963608bd343d89c1233ca64400b634a06c5 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:09:02 +0000 Subject: [PATCH 05/12] docs(mathesis): remove duplicate root architecture brief after archiving --- estate-mathematical-architecture | 137 ------------------------------- 1 file changed, 137 deletions(-) delete mode 100644 estate-mathematical-architecture diff --git a/estate-mathematical-architecture b/estate-mathematical-architecture deleted file mode 100644 index 65c7f3f3..00000000 --- a/estate-mathematical-architecture +++ /dev/null @@ -1,137 +0,0 @@ -MATHESIS — Estate-wide Mathematical Knowledge Architecture - -Mission -Re-evaluate and substantially improve the architecture of hyperpolymath/mathesis. Mathesis is intended to become the mathematical knowledge commons, proof-discovery atlas, and research-orientation system for a large, heterogeneous, multi-organisation software estate. - -It must serve humans, researchers, mathematicians, developers, coding agents, theorem-proving agents, and automated verification systems. The objective is to map out exact proof states, track translation pipelines across distinct logical foundations, and eliminate dependence on the owner's memory without turning Mathesis into a monolithic proof repository. The original repositories remain the sovereign territory of their own mathematics. - -1. Mandatory Initial Audit -Read the actual Mathesis repository before proposing changes. Start with README.adoc, docs/catalogue/catalogue.adoc, the scripts/census/ tools, the repository deed, and relevant CI workflows. - -Distinguish genuine architectural limits from deliberate simplifications. - -Do not discard the working census or its reproducibility simply to create a more elaborate directory layout. - -2. Estate Discovery, Authority, and Incremental Indexing -Mathesis must discover repositories across relevant owners, forges, and mirrors. Determine which source is authoritative for repository identity, clade/lineage (e.g., gv-clade-index), project membership, and verification receipts. - -The "Cold Start" Protocol: The indexing architecture must support incremental caching. A single repository push must update its own sub-graph and theorem states without forcing a multi-hour rebuild of the entire 400+ repository estate. - -Identity: Do not become a competing canonical registry for identities already owned by gv-clade-index. Use stable identifiers, aliases, and source pointers. - -3. Scope of Mathematical and Engineering Material -A repository need not contain a .agda or .lean file to belong in Mathesis. Discover mathematics appearing in compilers, databases, knot theory, topological simulations, and game engines. - -The estate explicitly divides into a Theory Path and an Engineering Path. Mathesis must track both: - -Theory Path: Pure mathematical formulation, topological proofs, and strict foundational verification (Agda, Rocq/Coq, Lean 4, Isabelle/HOL). - -Engineering Path: Applied invariants and bounded runtime verification. Mathesis must track: - -Idris2: For verified ABIs and strict type-driven design boundaries. - -Rust (Creusot) & Ada (SPARK): For memory-safe, mission-critical systems. (Note: These compile to the Why3 intermediate verification language. If Why3's automated SMT solvers fail, the resulting proof witnesses must be exported to Rocq or Isabelle for manual closure). - -Experimental Engineering Verification: Recognize and track early-stage verification bounds for newer languages. This specifically includes Apodeixi.jl (Julia for data), quintessence (Elixir for web/concurrency/fault tolerance), atoma (Zig for FFIs/APIs), and bactrian (OCaml for compilers and data processing). - -4. Navigation Views -Provide four complementary, generated navigation views: - -A. Alphabetical Mathematical Atlas: A–Z index of concepts, definitions, and aliases linking to their source proofs. - -B. Mathematical Subject Hierarchy: Standardized classifications (e.g., MSC2020) for interdisciplinary work. - -C. Project and Research Clusters: Navigable clusters spanning repositories (e.g., FSinFS, Echo/epistemic research, QuandleDB, eNSAID). - -D. Estate and Provenance View: Browse by organization, proof assistant, verification grade, and maturity status. - -5. The Verification Pipeline: Graded Proof Architecture -Mathesis must rigorously categorize theorems through a strict verification grading system. This tracks a proof from iterative theory down to API-verified cross-system certainty. - -Grade 3 (Iterative & Tentative Formulation): Prototyped and iteratively constructed in Agda. This relies on strict solver flags (e.g., --safe --erasure) or topological geometry (e.g., Full --cubical for knot/Conway problems). A proof is Grade 3 if it type-checks locally in Agda but has not been translated to an independent foundational system. - -Grade 2 (Proof Witness Translation): The Agda proof is translated into a highly rigid, independent foundational proof language. - -Grade 2i (Single Translation): The proof witness is translated to ONE alternative foundational system (e.g., Lean 4 or Rocq). - -Grade 2ii (Dual Translation for High-Assurance): The proof witness is translated into TWO fundamentally distinct logical architectures. Note on Prover Families to avoid foundational blind spots: Agda, Rocq, and Lean 4 all belong to the Dependent Type Theory (DTT) / Calculus of Inductive Constructions family. To achieve true foundational diversity for a Grade 2ii theorem, the second translation must target a non-DTT system like Isabelle/HOL (which relies on Higher-Order Logic/LCF-architecture). - -Grade 1 (Machine-Checked via Verified API): The translated proof witnesses successfully compile in headless, isolated CI environments via verified checker APIs. This requires passing the Axiom Lean Engine (AXLE) API for Lean 4, isabelle server instances for Isabelle/HOL, or internal coq-lsp REST APIs for Rocq. - -6. Epistemic Precision, Versioning, and Deprecation -Do not flatten proof confidence into a percentage. Record exactly whether a result is Open, Claimed, Grade 3, Grade 2i/ii, or Grade 1. - -Axiom Tracking: Track whether a result depends on unverified postulates, #print axioms (Lean), Print Assumptions (Rocq), or pinned library versions. - -Versioning and Regressions: A theorem proven in commit A may break in commit B. Mathesis must track the exact Git commit hash of the verification receipt. Introduce Superseded and Regressed statuses to flag previously Grade 1 proofs that no longer compile against the HEAD of their source repositories. - -7. Search, Access Control, and Knowledge Retrieval -Use the simplest useful working architecture (e.g., Canonical versions → deterministic generated SQLite/FTS5 index). - -Access Boundaries & Row-Level Security: Do not treat a private repository as absent merely because the scanner cannot read it. Conversely, the index query layer must enforce access-control natively (e.g., via clearance tokens or segregated databases) so that a public Mathesis catalog never leaks private repository titles, theorem statements, or WIP mathematical metadata. - -8. Agent Interfaces and Write-Back Correction -Design a stable entry point for coding agents (e.g., "Orient me to the mathematical estate," "Prepare a token-budgeted context pack"). - -LLM Hypothesis Tagging: Any missing mathematical bridge or dependency suggested by an LLM must be strictly tagged as LLM-Hypothesized (Unverified). - -Correction Pipeline: Agents must not have direct write-access to mutate the canonical SQLite index. Provide a strict "write-back" or "nomination" API where agents can submit discovered broken links, missing verification receipts, or false positives for human or CI-gated review. - -9. Dogfooding Investigations -Build and measure at least three substantive experiments to prove the architecture: - -Experiment A (FSinFS): Discover existing theorems, trace them through the pipeline, and output missing proof obligations. - -Experiment B (Quandles & Knots): Connect abstract KnotTheory.jl ideas to Full Cubical Agda topological foundations. - -Experiment C (Cross-Boundary Proof Identity): Verify that Mathesis correctly maps a Grade 3 Agda specification to a Grade 1 Lean/Isabelle proof witness, and connects both to their engineering implementations (e.g., Rust/Creusot). - -10. Directory and Repository Architecture -Develop and evaluate candidate architectures. Consider a structure like: - -registry/ — Canonical records and Grade 1-3 receipts. - -schemas/ — Validated record schemas. - -docs/atlas/ — Generated A-Z, subject, project, and estate views. - -tools/ — Extraction, validation, and incremental indexing logic. -Keep original proofs in their respective home repositories. - -11. Licensing, Reproducibility, and Trust -Use MPL-2.0. Do not copy entire external mathematical libraries or papers merely to index them; prefer source references. Reject silent index drift, duplicate proof inflation, and false positive verification claims. The system should report unresolved or unavailable evidence plainly. - -12. Delivery Stages -Stage 0: Ground-truth audit and CI review. - -Stage 1: Architecture and schema decision. - -Stage 2: Minimal working catalog (small vertical slice with generated views). - -Stage 3: Estate discovery with incremental refresh. - -Stage 4: Proof-level indexing (extracting Grade 1-3 statuses and assumptions). - -Stage 5: Retrieval evaluation (execute Dogfooding experiments). - -Stage 6: Agent interoperability (read APIs and write-back nomination). - -Stage 7: Wider mathematical atlas (external links and unformalized concepts). - -13. What Not To Do -Do not replace the current working census with an unfinished system. - -Do not assume all mathematics is located in .agda or .lean files. - -Do not invent missing repository identities or mathematical relationships to create a tidy taxonomy. - -Do not allow agent-generated evidence to count as independent corroboration. - -Do not treat embedding similarity as mathematical equivalence. - -Do not build a new theorem prover or a custom graph database unless strictly required by performance bottlenecks. - -14. Required Final Handover -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? From 2278b115102b1e44ffee50716c4dcfff1c675746 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:09:16 +0000 Subject: [PATCH 06/12] docs(mathesis): refresh generated map after standards pointer gains content --- docs/architecture/REPOSITORY-MAP.adoc | 1 - 1 file changed, 1 deletion(-) 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/` From ae98d0059ea8855e0ede67f5a7622bbb3860ee83 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:09:57 +0000 Subject: [PATCH 07/12] docs(mathesis): replace template scaffold with evidence-bounded architecture --- docs/architecture.adoc | 99 ++++++++++++++++++------------------------ 1 file changed, 43 insertions(+), 56 deletions(-) diff --git a/docs/architecture.adoc b/docs/architecture.adoc index e99f95ac..62c9726e 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]. From 35d5438f686d814032152c0271c70ccd63a7e23f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:09:59 +0000 Subject: [PATCH 08/12] docs(mathesis): turn duplicate architecture stub into pointer --- docs/ARCHITECTURE.adoc | 50 +++++------------------------------------- 1 file changed, 5 insertions(+), 45 deletions(-) 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. From 2033b6f86940eeb8c2b61907d37c80db3e7f1fc0 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:15:57 +0000 Subject: [PATCH 09/12] docs(mathesis): correct relative links in architecture guide --- docs/architecture.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/architecture.adoc b/docs/architecture.adoc index 62c9726e..af4cb4b6 100644 --- a/docs/architecture.adoc +++ b/docs/architecture.adoc @@ -35,7 +35,7 @@ The census counts and classifies observed files. It does not establish that Agda | Home mathematical repository at a concrete revision, with actual proof-checker outputs and assumptions | Census and derived atlas views -| link:../catalogue/catalogue.adoc[Mathesis census] and link:../atlas/README.adoc[atlas declaration of scope] +| link:catalogue/catalogue.adoc[Mathesis census] and link:atlas/README.adoc[atlas declaration of scope] | General test evidence and fixture requirements | https://github.com/hyperpolymath/proven-tests-and-benches[proven-tests-and-benches] and the canonical estate testing policy From 2bf767b4d6669ec6cfb9884ff35de1b17e06e40f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:21:08 +0000 Subject: [PATCH 10/12] docs(mathesis): give substantive authority routing a dedicated document --- docs/standards/AUTHORITY.adoc | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 docs/standards/AUTHORITY.adoc diff --git a/docs/standards/AUTHORITY.adoc b/docs/standards/AUTHORITY.adoc new file mode 100644 index 00000000..3d5aaeb6 --- /dev/null +++ b/docs/standards/AUTHORITY.adoc @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += 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. From 5523326d7a94535fa1aa73f4e785e69147884021 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:21:10 +0000 Subject: [PATCH 11/12] docs(mathesis): keep standards README as pointer to the authority guide --- docs/standards/README.adoc | 27 +++++---------------------- 1 file changed, 5 insertions(+), 22 deletions(-) diff --git a/docs/standards/README.adoc b/docs/standards/README.adoc index 3135af75..a138714a 100644 --- a/docs/standards/README.adoc +++ b/docs/standards/README.adoc @@ -1,26 +1,9 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= Mathesis standards and architectural authority +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Mathesis standards directory -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. +This directory is *not* a second copy of the estate standards. -== Authority by responsibility +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. -* *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. +Mathematical claims and formal proof receipts remain in the source repositories. The local mathematical census and atlas are indexes, not standards or certificates. From 57ebcd15943a3ff67fdf01d6a76f8bbfc33ca2e0 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 21:21:20 +0000 Subject: [PATCH 12/12] docs(mathesis): attribute authority guide --- docs/standards/AUTHORITY.adoc | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/standards/AUTHORITY.adoc b/docs/standards/AUTHORITY.adoc index 3d5aaeb6..c92e711f 100644 --- a/docs/standards/AUTHORITY.adoc +++ b/docs/standards/AUTHORITY.adoc @@ -1,4 +1,5 @@ // 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.