From 988d80e0ca1f79074f7ea625b0b914a12dcf835b Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 15:37:35 +0000 Subject: [PATCH 1/3] docs(proposals): assess mathesis and plan its re-anchoring Measured at main 8ee6354: the golden path tests template stubs only, four checks fail outside CI, the deed and the contracts describe the template, and 17 open pull requests conflict. Propose one identity (atlas, theory, applied, with an evidence spine), a target structure, a bridge centre mechanism and staged work orders. Nothing is changed besides this document. Each change needs a ruling. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- docs/proposals/mathesis-re-anchoring.adoc | 1238 +++++++++++++++++++++ 1 file changed, 1238 insertions(+) create mode 100644 docs/proposals/mathesis-re-anchoring.adoc diff --git a/docs/proposals/mathesis-re-anchoring.adoc b/docs/proposals/mathesis-re-anchoring.adoc new file mode 100644 index 0000000..10ca0f1 --- /dev/null +++ b/docs/proposals/mathesis-re-anchoring.adoc @@ -0,0 +1,1238 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Mathesis re-anchoring: assessment, identity and reorganisation plan +:toc: preamble +:toclevels: 2 +:sectnums: +:icons: font + +Status: *proposed, not ratified* (2026-11-10). This document changes no gate, +schema, deed clause or data file. Each change in it needs the owner's ruling, +and each ruling goes through the selector. The work orders in <> +are written for a later implementation session. + +The companion document is +link:mathesis-research-programme.adoc[the research programme]. This document +says what Mathesis is and how to put it in order. The companion says what +research the ordered repository supports. + +== Verdict in one page + +*Where Mathesis stands.* The facts below were measured on `main` at +`8ee6354` (2026-11-10). <> gives the command or file for each. + +* Mathesis has real, working parts. A census reads 505 repositories, and a + catalogue lists the 248 that have proof files. Three atlas views are + generated from the catalogue rows. A pilot registry pins 17 claims. One + theory theorem is proved in three provers. An applied-systems area exists. +* These parts are a small share of the tree. Of 539 tracked files, 52 exist + only in Mathesis and 23 more were changed after the mint. The other 464 come + from the RSR template unchanged, or changed only by the mint's name pass. +* The declared golden path, `just test && just quality`, checks template + stubs only. It checks no Mathesis part, and no workflow runs it. +* Main CI is green. Four checks fail when a person runs them, and CI runs none + of them. They are the catalogue drift check, the arrival-pack check, the + coaptation check and the AI-install check. +* The deed, the six contractiles and most status documents still describe the + template. The north-star contract lists the template's goals. +* 17 pull requests are open. Each one conflicts with `main`. At least six + repeat a fix that `main` already has. +* The public data names 40 private repositories. The architecture document + says that private metadata must not be published. +* Two programs derive Proof Witness Grades by different rules: the Mathesis + registry tool and the reader that the proof policy names as normative. +* Mathesis records the grade of its own theorem in prose only. It keeps no + machine-readable receipt, and its own registry does not list the theorem. + +*What Mathesis is.* Mathesis is the maths section of the estate. It keeps an +atlas of the mathematics in other repositories, the theory that no single +system owns, and methods that apply mathematics to decisions. One rule binds +the three: each statement carries its evidence, and Mathesis derives status +from that evidence. It does not assert status. + +*How it fits the estate.* The standards repository prescribes. The home +repositories prove. Mathesis describes. + +*What to do.* Six stages, each made of small work orders (<>): + +. Stage 0 stops the conflict between pull requests. +. Stage 1 closes the soundness holes. +. Stage 2 makes one data pipeline with one vocabulary. +. Stage 3 makes the deed, the contracts and the documents tell the truth. +. Stage 4 gives each of the three shelves its rule and its first content. +. Stage 5 scales the derived registry across the home repositories. + +The owner's decisions are in <>. + +*How the plan meets the four aims of the request.* + +[cols="1,4,2",options="header"] +|=== +|Aim |Answer |Where + +|Coherence +|One identity, one record model, one vocabulary and one data pipeline. The +template material is fenced by declared capabilities. +|<>, <>, stages 2 and 3 + +|Value in use +|Rows that show their commit and date. A registry that says what each +theorem still owes. Checks that fail when a view is stale. A published atlas. +|Stages 1, 2 and 5 + +|Clarity of direction +|A deed and contracts that state Mathesis goals. A roadmap with real stages. +Each open decision listed with its arms. +|Stage 3, <> + +|Opportunity +|A theory shelf with an admission rule. A centre for bridges between +systems. An applied shelf tied to the same evidence rules. A research +programme. +|Stages 4 and 5, <>, the companion document +|=== + +[[measured]] +== What was measured, and how + +=== Method + +* Source: `hyperpolymath/mathesis`, `main` at + `8ee635472ca2db6e59579c008233ec9bf747e439`. +* Canon: `metadatastician/standards` at + `be39f900665fb7c042c05d1165da018adc1860f4`. +* Template: `hyperpolymath/rsr-template-repo` at the mint pin + `4e663535bd939a6d9ed840aef2b6849434901b04`, which the deed records. +* Tools: Just 1.56.0, Nickel 1.18.0, Bun 1.4.4 and jq 1.7. The Just and + Nickel binaries passed the checksums that `proven-tests.yml` uses. +* Each check in <> was run from a clean tree. + +Limits of this assessment: + +* The session had no Agda, Rocq, Lean, Idris2 or Zig. No proof was rechecked. + `just test` and `just quality` could not complete. +* The pull request review read commit subjects and file lists. It did not + read each full diff. +* The estate survey read documentation and proof headers in public + repositories. It checked no proof. + +=== Where the files come from + +The template tree at the mint pin was compared with `main`, path by path and +blob by blob. + +[cols="3,1,4",options="header"] +|=== +|Class |Files |Meaning + +|Only in Mathesis +|52 +|The census, atlas and registry tools, their data and tests, the theory +proofs, the proposals, the authority guide, the applied-systems area and one +workflow. Five of the 52 are template files that the mint renamed or seeded: +the deed and four documents. + +|In the template, changed after the mint +|23 +|Mathesis edits, such as `README.adoc`, `Justfile` and `PROOF-STATUS.adoc`, +and later template syncs. + +|In the template, changed by the mint only +|115 +|The name pass changed these files. Nobody changed them later. + +|In the template, byte-identical +|349 +|The template spine and its scaffolds. +|=== + +The 115 and the 349 make 464 files, which is 86% of the tree. This number is a +file count. It is not a measure of value. + +[[gate-results]] +=== Gate results + +[cols="3,4,3,1",options="header"] +|=== +|Check |Command |Result |In CI + +|Catalogue matches its rows +|`just catalogue-check` +|*Fails.* `catalogue.adoc` holds a second row for one repository. +|no + +|Arrival pack matches the deed +|`just validate-claude-md` +|*Fails.* `CLAUDE.md` says the clade is `UNASSIGNED`. The deed says `fv`. +|no + +|Coaptation receipt is current +|`just validate-coapt` +|*Fails.* The committed receipt is stale. +|no + +|AI-install guide +|`just validate-ai-install` +|*Fails.* `README.adoc` has no AI-install section or anchor. +|no + +|Capability profile (canon checker) +|`standards/scripts/check-rsr-profile.sh .` +|*Cannot score.* The deed declares no capability and no preset. +|no + +|Golden path +|`just test`, `just quality` +|Not completed (no Idris2, no Zig). Both recipes read `src/interface` only. +|no + +|Atlas matches its rows +|`bun scripts/atlas/census-atlas.mjs check`, plus 10 tests +|Passes. +|yes + +|Registry derives and matches +|`bun scripts/registry/claims-registry.mjs check`, plus 7 tests +|Passes. 17 claims, 2 pinned sources. +|yes + +|Status-document choice +|`bash tests/census/build_rows_status_test.sh` +|Passes. +|no + +|Repository map +|`just validate-repo-map` +|Passes. +|yes + +|Root shape +|`bash scripts/check-root-shape.sh .` +|Passes. +|yes + +|RSR compliance, deed state +|`just validate-rsr`, `just validate-state` +|Pass. +|no + +|I-JSON and JCS +|`bash scripts/check-ijson-jcs.sh --enforce .` +|Passes. 18 files. +|yes + +|Agda proof gate +|`bash scripts/check-proofs.sh agda` +|Not run here. The workflow `agda-proof-policy.yml` runs it. +|yes +|=== + +=== Findings + +Each finding states a fact, its evidence and its consequence. + +[[f-1]]F-1. The golden path does not test Mathesis:: +`just test` runs `idris2 --typecheck src/interface/abi.ipkg` and +`zig build test` in `src/interface/ffi`. `just quality` adds +`zig fmt --check`. These files are template stubs. The census, atlas, registry +and proof checks are separate recipes. No workflow runs `just test` or +`just quality`. The deed's `(anchor (golden-path))` therefore promises a check +that says nothing about this repository. + +[[f-2]]F-2. Four checks fail and CI does not run them:: +See <>. The duplicate catalogue row came from two merged pull +requests that changed the same generated file. A check that CI does not run +cannot protect `main`. + +[[f-3]]F-3. The descriptive record describes the template:: +* Deed: `(manifest :purpose)` says "Canonical RSR ... template". + `(meta :type)` says `library`. `(anchor (implementation-policy))` allows + Rust, Idris2 and Zig and does not name the JavaScript that the atlas and + registry use. `(anchor (semantic-authority-files))` names four files that do + not exist. `(ecosystem :not)` is empty. `(variant (paths :added))` is empty. +* Contractiles: the `intend` contract lists `repo-initialization` and four + more template goals. No contract states a Mathesis invariant. +* Status: `TEST-NEEDS.adoc` records CRG grade C as "ACHIEVED 2026-04-04", a + date before this repository existed. `READINESS.adoc` is an unfilled form. + `ROADMAP.adoc` keeps the template milestones. `PROOF-NEEDS.adoc` lists the + template's seven ABI and typing obligations. +* Documents: `docs/EXPLAINME.adoc` is titled "RSR Template Repo - Explainme". + `docs/usage.adoc` shows a service that listens on port 8080. + `docs/AFFIRMATION.adoc` is an unsigned form. +* The name pass damaged some sentences. `PROOF-NEEDS.adoc` says "These proofs + come from the mathesis". The `dust` contract forbids "references to mathesis + in generic template files". + +[[f-4]]F-4. The capability profile is empty, and two gates disagree:: +The canon decides which template modules a repository carries by its declared +capabilities. Mathesis declares none. With an honest profile +(<>), the canon checker reports seven vestigial modules: +`src/interface/ffi/`, `src/interface/Abi/`, `src/interface/generated/`, +`benches/`, `build/container/Containerfile`, `rust-ci.yml` and `release.yml`. +The local `just validate-rsr` requires three of these directories in every +repository. The two gates cannot both pass. The cause is in the template. ++ +The canon checker also compares `(manifest :project)` with the deed's +`:canonical-name`, letter for letter. The deed has "Mathesis" in one and +"mathesis" in the other, so the checker reports a missing baseline manifest. + +[[f-5]]F-5. Two derivations of the grade exist:: +PROOF-POLICY §8.5.1 names `readProofReceipt` in the standards repository as +"the normative definition of the profile's fields, vocabularies and +derivation". It says that Mathesis reads receipts through it. The Mathesis +tool `scripts/registry/claims-registry.mjs` has its own parser and its own +rules. The rules differ in three places: ++ +* The canon counts a recheck leg only with a `proven` token, a `transported` + or `re-proved` route, the state `RECONCILED` and a current receipt. The + Mathesis tool counts each leg whose state is `RECONCILED`. +* The canon requires a current Agda receipt and the state `AGDA-VERIFIED`. The + Mathesis tool reads one `:flags` field and the Agda token. +* The canon derives `PWG-1`. The Mathesis tool does not. + +[[f-6]]F-6. Mathesis does not yet keep the rules of a home repository:: +THY-1 has a careful prose record in `docs/status/PROOF-STATUS.adoc`. The +record has gaps that the same file and the roadmap name: ++ +* No receipt deed exists under `verification/receipts/` (PROOF-POLICY §8.5.1). +* The registry does not list `hyperpolymath/mathesis#THY-1`. +* No CI lane runs the Rocq leg or the Lean leg. +* `scripts/check-proofs.sh` passes a Rocq file with `Admitted` and a Lean file + with `sorry`. +* The Agda lane installs Agda from the distribution package. PROOF-POLICY §6 + requires a `deviation` record for that, and none exists. + +[[f-7]]F-7. One register is written by hand:: +`docs/status/CROSS-PROVER-RECONCILIATION.adoc` calls itself a working policy. +PROOF-POLICY §2.2 has since adopted that vocabulary, so the policy text is now +a copy. The same file holds a register of grades that a person typed. The +registry exists so that nobody types a grade. + +[[f-8]]F-8. The data layout causes the pull request conflicts:: +* Each data file is one line of JSON. Two pull requests that change two + different rows conflict on that line. +* A row has no source commit and no census date. A reader cannot tell a fresh + row from an old one. +* The atlas test, the atlas README and the main README state the row count as + a literal number. Each refresh must edit them. +* No rule names one writer for the census data. On 2026-11-09 many sessions + refreshed rows at the same time. +* The deed's `(coverage)` and `(debt)` clauses are empty, so no session could + see the work of another. + +[[f-9]]F-9. Private names are public:: +`repos.json` lists 40 repositories with `"visibility":"private"`. +`unreachable.json` and the "Not reached" section of `catalogue.adoc` repeat +the names. `README.adoc` names one of them. `docs/architecture.adoc` says +"private metadata must not be published". The architecture brief says a +public catalogue must not leak private repository titles. + +[[f-10]]F-10. Three proposals overlap, and the canon settled part of them:: +Issue 28, `proof-receipts-as-data.adoc` and ADR 0004 each propose how +receipts become data. PROOF-POLICY §8.5.1 now fixes the receipt format, its +conventional path and its reader. Each proposal still reads as open. + +[[f-11]]F-11. A ruling about Mathesis is not recorded in Mathesis:: +The owner ruled on 2026-11-09 that the token-lattice theory lives in Mathesis +(decision D-10 of the ECHIDNA proof-route plan in the standards repository). +On `main`, no Mathesis file records the ruling. An open, conflicting pull +request carries it. + +=== What works and must stay + +* The census is reproducible, and it states its own limits in plain words. +* The atlas refuses a row whose repository is not public. Its tests include + negative controls. +* A registry record holds no grade. It pins a commit and a receipt digest. +* The THY-1 record is a model: checker versions, invocations, file digests, + import cone, negative controls, and a statement comparison item by item. + It records the failed Dedukti route as `BLOCKED` and describes a seven-line + reproducer. +* `docs/standards/AUTHORITY.adoc` and `docs/architecture.adoc` state the + limits of Mathesis correctly. +* The applied-systems area has its own evidence vocabulary, and it keeps + "missing" apart from zero. + +== What Mathesis could be + +=== Models from outside the estate + +Each model below solves a part of the same problem. The last column says what +Mathesis takes from it. + +[cols="2,3,3",options="header"] +|=== +|Model |What it is |Lesson for Mathesis + +|Formalizing 100 Theorems +|A list that shows which proof assistant has formalised each theorem. +|A cross-prover scoreboard needs one key per statement. The PWG census is +that scoreboard for the estate. + +|Archive of Formal Proofs +|A refereed collection of Isabelle developments, rechecked on each release. +|Recheck on each change, and show a broken entry as broken. This is the +`regressed` receipt state. + +|Stacks Project tags +|A stable identifier for each result, kept when the text moves. +|A claim identifier must outlive file moves. Use the home's own claim id. + +|Formal Abstracts +|Formal statements of main results, without the proofs. +|A registry of statements has value before all proofs exist. + +|Concept alignments (Math-in-the-Middle) +|Typed links between the same concept in different proof libraries. +|A bridge is a record with a type and a justification. It is not a +matching name. + +|Dedukti and Logipedia +|Proofs written in one logical framework and exported to several provers. +|Transport is the strongest recheck where it works. Record where it fails. + +|Hets and DOL +|Theories in different logics, joined by recorded logic translations. +|A relation between statements in two systems names its translation. + +|Assurance cases +|Claims, arguments, evidence and defeaters in one structure. +|A grade needs its reasons. The registry's "why not higher" column is the +defeater list. + +|Provenance semirings +|An algebra that computes the annotation of a derived fact from its inputs. +|"Only as strong as the weakest step" is one instance. See the research +programme. + +|Attestations (in-toto, SLSA) +|Signed statements about how an artefact was produced. +|A receipt is an attestation. It can use the same transport and checks. + +|Federated software catalogues +|Each repository owns its descriptor. A centre collects them. +|The home repository owns the record. Mathesis collects and recomputes. + +|Official census practice +|A frame, an enumeration, a reference date and a non-response count. +|Each row needs a reference date and a source commit. +|=== + +=== Four candidate identities + +[cols="1,3,3",options="header"] +|=== +|Candidate |Description |Verdict + +|M1. Index only +|Mathesis points at proofs and holds none. +|Rejected. It contradicts two owner rulings: the token-lattice theory lives +here, and the applied-systems area was requested here. + +|M2. Three shelves +|An atlas, a theory shelf and an applied shelf, each with its own rule. +|Adopted as the *shape*. + +|M3. Evidence system +|One record model for claims, evidence and bridges. +|Adopted as the *spine* that the three shelves share. + +|M4. Concept commons +|One identity for each mathematical object across all systems. +|Kept as the *horizon*. It is reached through recorded bridges. It +is not reached through a taxonomy that a person or a model invents. +|=== + +[[identity]] +== The proposed identity + +=== In brief + +Mathesis is the maths section of the estate. It keeps an atlas of the +mathematics in other repositories, the theory that no single system owns, and +methods that apply mathematics to decisions. + +=== Three verbs + +[cols="1,2,4",options="header"] +|=== +|Verb |Who |What + +|Prescribe +|`metadatastician/standards` +|It says what must be proved and how (PROOF-POLICY, the requirements master +list). + +|Prove +|Each home repository +|It holds the proof and the receipt. It owns the theorem and its evidence. + +|Describe +|Mathesis +|It says what is proved, where and how strongly. It derives each answer from +the home's receipts. +|=== + +In the estate's own terms, Mathesis is the mathematical *descriptile* of the +estate and the standards repository holds the *contractile*. A report that +compares the two is the estate-level form of coaptation. + +Mathesis is also a home repository for its own theory. In that role it obeys +each rule that it checks in others. + +=== IS and IS NOT + +Mathesis *is*: + +* the index that answers "where does that proof live, and what supports it?"; +* the home of theory that an estate rule or vocabulary depends on and that no + single system owns; +* the canonical place for bridge records that cross repositories + (<>, proposed); +* a place for reusable methods that apply mathematics to decisions. + +Mathesis *is not*: + +* a prover or a proof kernel. The home repository's checker decides. +* the proof policy. PROOF-POLICY decides. +* the identity registry. `gv-clade-index` decides. +* the map of the type family. `nextgen-typing` coordinates that map and its + glossary. +* a copy of other repositories' proofs or receipts. +* a grade authority. It derives a grade and does not assign one. +* a store for private or organisation-specific case material. +* the RSR template. The template is its lineage only. + +=== The spine: one relation, four record kinds + +The manifesto defines assurance as "a disciplined relationship among a claim, +the evidence offered for it, the model in which that evidence has force, the +residual uncertainty, and an authority accountable for the decision". Mathesis +uses that relation as its record model. + +[cols="2,3,3",options="header"] +|=== +|Manifesto term |Mathesis field |Source of the field + +|Claim +|The claim id and the statement, in the home's wording +|The home's proof-status file + +|Evidence +|Receipts: checker, version, invocation, input digest, result +|The home's receipt deed + +|Model +|Prover, flags, import cone, foundation family +|The receipt + +|Residual uncertainty +|Axioms, assumptions, waivers and the reasons a grade is not higher +|The receipt and the derivation + +|Accountable authority +|The home repository and commit, and the policy pin +|The registry pin +|=== + +Mathesis holds four kinds of record. Each kind has one authority. + +[cols="1,3,2,2",options="header"] +|=== +|Kind |What it is |Authority |Mathesis role + +|Source row +|One measured row for each repository with proof files +|The census run, at a commit and a date +|Measures + +|Claim pin +|A pointer to one claim in its home, at a commit and a receipt digest +|The home repository +|Points and derives + +|Receipt +|The home's machine-readable proof receipt +|The home repository +|Reads through the canon reader. Does not store. + +|Bridge +|A recorded relation between two artefacts, possibly in two repositories. It +names its criterion. +|Mathesis, for bridges that cross repositories (proposed) +|Records, with the evidence in the homes +|=== + +=== Three shelves + +[cols="1,3,2,3",options="header"] +|=== +|Shelf |Holds |Authored or derived |Rule + +|Atlas +|Census rows, the catalogue and views, the claims registry, the +bridge view +|Derived. Only the pins and the bridge records are authored. +|No view states a status that a receipt does not support. + +|Theory +|Theorems that no single system owns: THY-1 and the token-lattice theory +|Authored here +|Mathesis is the home. The admission rule in <> applies. + +|Applied +|Methods and synthetic examples in `applied-systems/` +|Authored here +|Each input carries an evidence status. No private case data. +|=== + +The three shelves match the three pillars of the manifesto: machine-readable +governance, neurosymbolic verification and post-disciplinary praxis. This +match is a reading by the author of this plan. The manifesto does not name +Mathesis. + +=== One meaning for each word + +[cols="1,4",options="header"] +|=== +|Word |Meaning in Mathesis + +|Census +|The measurement run over the frame. It counts files and text markers. + +|Frame +|The list of repositories that the census reads. + +|Row +|The census result for one repository: counts, a source commit and a date. + +|Catalogue +|The generated table of rows, split by census class. It is one atlas view. + +|Atlas +|All generated views together, with their data. + +|Claim +|One theorem, demonstration or assumption in a home repository. + +|Receipt +|The home's record of checker runs for its claims (PROOF-POLICY §8.5.1). + +|Registry +|The generated theorem-level view. Its grades are derived. + +|Bridge +|A recorded, direction-sensitive relation between two artefacts. It names its +criterion, what it preserves and what it forgets. + +|Grade +|A Proof Witness Grade only. It always has the `PWG-` prefix. + +|Home repository +|The repository that owns a claim and its evidence. + +|Shelf +|One of the three parts: atlas, theory, applied. +|=== + +Two words leave the vocabulary. "Register" becomes a generated view of +bridges. "Ledger" stays the home repository's word. + +[[structure]] +== Target structure + +The plan adds no root directory. It keeps the paths that the estate's gates +read: `verification/proofs/`, `verification/receipts/` and `applied-systems/`. + +[source,text] +---- +README.adoc identity, three shelves, quick start +mathesis_chora.deed truthful clauses (stage 3) +docs/ + atlas/ ATLAS shelf + README.adoc pipeline, vocabulary, refresh rule + census/ measured: repos.jsonl, rows.jsonl, + unreachable.jsonl, the two text lists + claims/ authored: claims.jsonl, + bridges.jsonl (stage 5) + generated/ catalogue.adoc, az.adoc, + organisations.adoc, index.json, + registry.adoc, bridges.adoc + theory/ THEORY shelf: admission rule and index + status/ ROADMAP, PROOF-NEEDS, PROOF-STATUS + decisions/ proposals/ standards/ +verification/ + proofs/agda|coq|lean4/ home theory sources and manifests + receipts/ the proof receipt of Mathesis +applied-systems/ APPLIED shelf +scripts/census|atlas|registry/ tools +tests/census|atlas|registry/ tests +---- + +[cols="2,2,3",options="header"] +|=== +|Today |Target |Reason + +|`docs/catalogue/census/*.json` +|`docs/atlas/census/*.jsonl` +|One record on each line ends the single-line conflicts. + +|`docs/catalogue/catalogue.adoc` +|`docs/atlas/generated/catalogue.adoc` +|The catalogue is a generated view of the same rows. + +|`docs/registry/claims.json` +|`docs/atlas/claims/claims.jsonl` +|Pins are authored data. They sit beside the bridge records. + +|`docs/registry/registry.adoc` +|`docs/atlas/generated/registry.adoc` +|The registry is a generated view. + +|`docs/atlas/generated/classes.adoc` +|Removed +|It repeats the catalogue with fewer columns. + +|`docs/status/CROSS-PROVER-RECONCILIATION.adoc` +|A short pointer file at the same path +|The policy text is in PROOF-POLICY §2.2. The rows become generated. +|=== + +Paths that other repositories cite keep a pointer file. Known examples are +`docs/proposals/estate-mathematical-architecture.adoc`, which PROOF-POLICY §8 +cites, and the old catalogue path. The proposal files do not move. + +[[centre]] +== The bridge centre (proposed mechanism) + +The architecture brief records an owner direction of 2026-11-09. Mathesis +becomes the canonical centre for the correspondence record. Each +participating repository keeps an attested local copy, and drift raises an +alert. The brief leaves the mechanism open. This section proposes one. + +The estate already has a word for one such record: a *bridge*. PROOF-POLICY +§2.2 uses it ("a checked bridge or justified statement correspondence"). The +owner's research note on types, tropes and identity +(`hyperpolymath/vcl-ut`, `docs/research/TYPE-TROPE-IDENTITY-SPACES.adoc`) +defines it. This plan uses the word with that meaning. + +=== Principle + +Evidence is local. A bridge has two ends. + +A home repository can check its own proofs, so it owns its evidence. A bridge +relates two artefacts, and the two can be in two repositories. Examples are +an Agda statement and its Lean restatement, or a theorem and the code that +implements it. If one end keeps the record, the other end can change without +notice. So the centre keeps the record, and each end keeps an attested copy. + +This principle keeps the receipt rule intact. Proof status still comes from +the home's receipts. The centre records only the relation and points at the +evidence in each home. + +The centre does not decide how the type disciplines relate. `nextgen-typing` +holds that map (`docs/TYPE-CONNECTIONS.adoc`) and its decisions. A Mathesis +bridge records the evidence for one pair of artefacts. + +=== Rules that each bridge obeys + +The rules come from the research note. A bridge is "a partial and potentially +many-to-many, direction-sensitive relation, not an assumed coercion or +equivalence". + +* It names its *criterion*: what "the same" means for this bridge, and for + which observer. +* It states what it *preserves* and what it *forgets*. +* It has a *direction*. +* It claims no universal identity. Two artefacts are the same under a named + criterion, or they are not related by this record. +* Equal names prove nothing. The estate has an example: an Agda record and a + Lean structure are both named `ResourceAlgebra`, and their laws differ. + +=== The record + +One record for each bridge, in `docs/atlas/claims/bridges.jsonl`: + +* an identifier; +* two endpoints, each with repository, commit, path, name, system and the + blob digest of the file; +* the criterion and the direction; +* what the bridge preserves and what it forgets; +* the relation: `same-statement`, `refinement`, `conditional-transport`, + `countermodel` or `unassessed`; +* the §2.2 correspondence state; +* the basis: `read`, `generated`, `transported` or `proved`; +* a pointer to the comparison record in a home repository; +* the residual assumptions; +* who proposed it, a person or an agent, and who reviewed it. + +A record that an agent proposed stays `unassessed` until a person reviews a +comparison that a home repository holds. The record holds no token and no +grade. + +The survey found three practices for that review: + +* `MetaManifold-Evidence` and `hvn-dehallucinator` keep a leg + `BRIDGE-PENDING` until the owner reviews the comparison. +* `lintel` records `RECONCILED` and says that the comparison is provisional + until the owner reviews it. +* `nextgen-typing` (XP-1) and Mathesis (THY-1) record `RECONCILED` with no + such note. + +The bridge record names the reviewer, so the three cases cannot look the +same. + +=== What the centre computes + +* *Classes under one criterion.* The centre composes the bridges that share a + criterion and that the records declare composable. It lists the classes + that result. A class means "the same under this criterion". The concept + view of the architecture brief can list these classes. Nobody writes that + view by hand. +* *Order.* `refinement` bridges give an order between classes. +* *Contradictions.* A `countermodel` between two artefacts that a chain of + bridges joins, under the same criterion, fails the check. +* *Five different absences.* When no bridge exists, the view says which case + holds: refuted, not yet proved, not enough evidence, forbidden, or not + defined. The research note asks for this distinction. + +This is the manifesto's phrase "identity defined by equivalence rather than +asserted", made into a computation that always names its criterion. + +=== The lock + +The estate already has one pattern for a canonical centre with pinned +copies: the canon lockstep in the deed's `(canon)` clause. The proposal uses +the same pattern. + +. Mathesis publishes a lock file. For each participating repository, the lock + gives the digest of the records that name it. This set is the repository's + *slice*. +. Each participating repository keeps its slice as a file and records the + slice digest in its deed. +. A k9 contract in the home compares the local slice with the lock at the + pinned Mathesis commit. A difference fails the home's gate. +. A check in Mathesis compares each endpoint's blob digest with the home's + current tree. A changed file marks the record `stale` and fails the check. +. A pull request that changes a record must name the home commits that hold + the evidence. The check lists each affected repository. + +Blob digests make a record survive commits that do not touch the file. A +commit that changes the statement makes the record stale, which is correct. +A stale record is a question about identity through time. A new comparison +answers it. A digest does not. + +=== Order of work + +. The home lands the proof, the receipt and the statement comparison. +. Mathesis records the bridge and releases the lock. +. The home pins its slice. + +The centre derives the bridges inside one home from that home's receipt: the +legs of one claim are joined there already. It records by hand only the +bridges that cross repositories. + +Two pilots are ready. The first is a squeakwell recovery-ladder row, whose +Agda, Rocq and Lean artefacts are in three repositories. The second is the +open bridge between the Agda `ResourceAlgebra` of `resource-algebra` and the +Lean structure of the same name in `tropical-types`. + +[[work-orders]] +== Work orders + +Each work order is one small pull request. It names its check. A work order +that needs a ruling says so. No work order relaxes a gate. + +=== Stage 0: stop the conflicts + +[[wo-0-1]]WO 0.1 Triage the open pull requests:: +*Goal:* no open pull request repeats or blocks another. + +*Steps:* Read each full diff. Complete the table in <>. Put the +table to the owner. Rebase the kept changes in this order: scanner fixes, +one refresh tool, the frame fix. Close a pull request only on the owner's +word. + +*Check:* each open pull request merges cleanly, one at a time. + +*Needs ruling:* yes (D-6). + +[[wo-0-2]]WO 0.2 Name one writer for census data:: +*Goal:* two sessions cannot refresh rows at the same time. + +*Steps:* State the rule in `docs/atlas/README.adoc` and in the deed's +`(bot-directives)`. Only `just census` and `just update-rows` write rows. +Only one pull request that changes rows is open at a time. Record open work +in `docs/status/ROADMAP.adoc`. + +*Check:* the rule is in both files. + +=== Stage 1: close the holes + +[[wo-1-1]]WO 1.1 Repair and gate the catalogue:: +*Steps:* Run `just catalogue`. Add `just catalogue-check` and +`tests/census/build_rows_status_test.sh` to CI. + +*Check:* a planted duplicate row fails the new step. A clean tree passes. + +[[wo-1-2]]WO 1.2 Gate the arrival pack and the coaptation receipt:: +*Steps:* Run `just claude-md`. Add `just validate-claude-md` to CI. Add +`just validate-coapt` after stage 3 regenerates the receipt. + +*Check:* a hand edit inside the generated region of `CLAUDE.md` fails. + +*Note:* the template does not run these two checks in CI. Report that to the +template repository. + +[[wo-1-3]]WO 1.3 Close the proof gate gap:: +*Steps:* Adopt the reference gate that PROOF-POLICY §8.4 names +(januskey `scripts/check-agda.sh` and `scripts/scan-postulates.sh`) for the +Agda leg. For Rocq, fail when `Print Assumptions` lists an axiom for a gated +theorem. For Lean, fail when `#print axioms` lists one. + +*Check:* a planted `postulate`, `Admitted` and `sorry` each fail. The clean +files pass. + +*Note:* `scripts/check-proofs.sh` is a template file. Send the same fix to +the template. + +[[wo-1-4]]WO 1.4 Add CI lanes for Rocq and Lean:: +*Steps:* Install Rocq 8.18.0 and Lean 4.15.0 at pinned versions with digest +checks. Assert each version in the run. Write a `deviation` record for each +toolchain that does not come from the Guix manifest or the container +(PROOF-POLICY §6). Write the same record for the Agda lane. Run the three +lanes on each commit to `main`, with no path filter. A lane that runs only +when a proof file changes gives no receipt for the other commits. + +*Check:* each lane fails on the planted controls of WO 1.3. A commit that +changes only a document still gets three receipts. + +[[wo-1-5]]WO 1.5 Write the receipt of Mathesis:: +*Steps:* Write `verification/receipts/theory_praxis.deed` with +`:profile proof-receipt`, from the THY-1 record. Record a run only where a +run exists. Validate the file with +`bun 1-formats/deed/tools/deed_lint.js --proof-receipt-json`. Add the claim +`hyperpolymath/mathesis#THY-1` to the registry. + +*Check:* the reader accepts the receipt, and the registry shows the grade +that the reader derives. Change `PROOF-STATUS.adoc` if the two differ. + +=== Stage 2: one pipeline + +[[wo-2-1]]WO 2.1 Move the data to JSON Lines, with provenance:: +*Steps:* Write each record on one line (standards JSON-POLICY rule J-2). +Add `commit` and `censused_at` to each row. Make `census-repo.sh` record the +commit that it read. Run one full census so that each row has both fields. +Derive the row count in tests and documents. Do not write it as a literal. + +*Check:* `jq -cS -s .` over the new rows equals the old array for the old +fields. Two branches that change two different rows merge cleanly. + +[[wo-2-2]]WO 2.2 Use the canon reader in the registry:: +*Steps:* Delete `parseReceipt` and `derive` from `claims-registry.mjs`. Call +`readProofReceipt` from the pinned standards checkout. Show a receipt that +the reader refuses as `ungraded`, with the reader's reason. Keep the pin, the +digest check and the renderer. + +*Check:* the 17 pilot claims still derive `ungraded`. The hermetic tests pass +with fixture receipts in the §8.5.1 shape. + +*Needs ruling:* yes (D-5). + +[[wo-2-3]]WO 2.3 Move the paths:: +*Steps:* Apply the table in <> with `git mv`. Update the tools, +tests, recipes, the workflow step and the README. Leave a pointer file at +each old path that another repository cites. Run `just repo-map`. + +*Check:* each generated view is byte-identical to the view before the move, +apart from its own path strings. + +*Needs ruling:* yes (D-4). + +[[wo-2-4]]WO 2.4 Generate the bridge view:: +*Steps:* For each hand-written row in the reconciliation register, find the +home's receipt. Add a claim pin where a receipt exists. Keep the row as a +candidate bridge where the relation crosses repositories. Replace the +policy text with a pointer to PROOF-POLICY §2.2. + +*Check:* no grade in the repository is typed by hand. + +[[wo-2-5]]WO 2.5 Make the golden path real:: +*Steps:* Add a recipe `check` that runs the catalogue, atlas, registry and +proof checks. Make `test` depend on it. Run the recipe in CI. + +*Check:* `just test` fails on a stale view and on a failing proof. + +=== Stage 3: tell the truth + +[[wo-3-1]]WO 3.1 Correct the deed:: +*Steps:* Use `scripts/deed-clause.sh`, the one writer. Set the `(ecosystem)` +purpose and `:not` list from <>. Correct `(manifest :purpose)`, +set `(manifest :project)` to `mathesis`, and correct `(meta)`, `(anchor)`, +`(variant (paths))` and `(bot-directives)`. Review each +`(integrations)` clause and remove the unused ones. Then run `just claude-md` +and `just coapt`. + +*Check:* the canon deed validator, `just validate-state`, +`just validate-claude-md` and `just validate-coapt` pass. + +*Needs ruling:* yes (D-1). + +[[wo-3-2]]WO 3.2 Declare the capabilities and remove vestigial modules:: +*Steps:* Declare `agda`, `formal-proofs`, `bash`, `docs-site`, +`governance-tier` and `reproducible-build` in `(rsr-profile)`. Run the canon +checker. Remove each module that it reports as vestigial, with the proofs, +tests and obligations that belong to that module only. Open an issue on the +template for the `validate-rsr` conflict of <>. Record each local +divergence in `(variant (paths :diverged))` until the template fix lands. + +*Check:* `check-rsr-profile.sh` passes for the gated modules, and +`just validate-rsr` passes. + +*Needs ruling:* yes (D-3). + +[[wo-3-3]]WO 3.3 State the Mathesis contracts:: +*Steps:* Add Mathesis clauses to the contractiles. Remove a template clause +only where it cannot apply to a minted repository. The `intend` contract +takes the stages of this plan. The `trust` contract says who writes which +record. The `must` contract takes these clauses: ++ +* each generated view is current; +* no private repository is named; +* no grade is typed by hand; +* receipts stay in their homes; +* each home theorem has a receipt; +* each row has a commit and a date. + ++ +*Check:* the k9 validators pass, and `just coapt` reports each new clause as +witnessed. + +*Needs ruling:* yes. The contractiles are a declared sensitive area. + +[[wo-3-4]]WO 3.4 Rewrite the entry documents to the standard:: +*Steps:* Write `README.adoc` and `docs/EXPLAINME.adoc` to the README and +EXPLAINME authoring standard. EXPLAINME carries the proof ledger that the +standard requires. Write the real stages into `ROADMAP.adoc`, and record the +D-10 ruling there. Write the true obligations into `PROOF-NEEDS.adoc`. Fill +`READINESS.adoc` and `TEST-NEEDS.adoc` from observed runs. Fill or shorten +`usage.adoc`, `contributing.adoc` and `troubleshooting.adoc`. + +*Check:* each README claim has an EXPLAINME entry. No status document states a +result that this session did not observe. + +[[wo-3-5]]WO 3.5 Stop the publication of private names:: +*Steps:* Apply the owner's ruling. + +*Needs ruling:* yes (D-2). + +[[wo-3-6]]WO 3.6 Affirm:: +*Steps:* When stages 0 to 3 are done, fill `docs/AFFIRMATION.adoc` at one +commit, from runs in the same session, in a signed commit. + +*Check:* each line of the affirmation names its command. + +=== Stage 4: the three shelves + +[[wo-4-1]]WO 4.1 Give the theory shelf its rule:: +*Steps:* Write `docs/theory/README.adoc`. State the admission rule. A theorem +enters only when three conditions hold: ++ +* it is theory by the test of PROOF-POLICY §1; +* no single system owns it; +* an estate rule, vocabulary or interface depends on it, and the record names + that dependant. + ++ +Generate the theorem index from the receipt. Remove the three template +example proofs. Each one says that the project must replace it. + +*Next content:* the token-lattice theorems (rows 2 and 12 of the ECHIDNA +proof-route ladder). The research programme gives their statements. + +[[wo-4-2]]WO 4.2 Tie the applied shelf to the spine:: +*Steps:* Define the minimal data schema that the roadmap already names. Write +one synthetic worked example. Give each input an evidence status. State which +invariants merit a proof, and record them as open obligations. + +*Check:* a missing input stays missing in the output. It does not become zero. + +[[wo-4-3]]WO 4.3 Publish the atlas:: +*Steps:* Enable the Pages workflow for the generated views after stage 1 +holds for two weeks. + +*Needs ruling:* yes. Publication is outward-facing. + +=== Stage 5: scale + +[[wo-5-1]]WO 5.1 Bring receipts to the home repositories:: +Run a campaign, one repository at a time, that writes a §8.5.1 receipt where +a theory repository records grades. Start with the repositories that the +registry and the register already name. Add each one to the registry when its +receipt lands. + +[[wo-5-2]]WO 5.2 Pilot the bridge lock:: +Build the mechanism of <> for one relation that crosses repositories. +*Needs ruling:* yes (D-7). + +[[wo-5-3]]WO 5.3 Schedule the census:: +Run the census in one scheduled workflow that opens one pull request. This +workflow becomes the one writer of WO 0.2. + +[[wo-5-4]]WO 5.4 Report what is owed:: +Generate one view that sets the requirements master list of the standards +repository beside the census and the registry, repository by repository. + +[[decisions]] +== Decisions for the owner + +Each decision lists its arms with the most elegant and correct long-term arm +first. The recommended arm is marked where it differs. The plan above assumes +arm (a) in each case. + +. *D-1 Identity.* (a) The three shelves with the evidence spine, as in + <>. (b) An index only, with the theory and the applied area moved + to other repositories. (c) An evidence system only, with the applied area + moved out. +. *D-2 Private repository names.* (a) Publish counts only, remove the names + from the tracked files, and keep the history as it is. (b) The same, and + also rewrite the history, which breaks each clone and mirror. (c) Rule that + the names are public, and amend the invariant. +. *D-3 Template material.* (a) Declare capabilities, remove the vestigial + modules by the canon route, and fix the gate conflict in the template. + (b) Keep each file, and record the ownership boundary only. (c) Remove all + unused template material at once, which breaks template conformance. +. *D-4 Paths.* (a) Consolidate the pipeline under `docs/atlas/`. (b) Keep the + paths and change the content only. +. *D-5 Overlapping proposals.* (a) Amend ADR 0004 to use the canon reader, + and ratify it. Mark `proof-receipts-as-data.adoc` as settled in part by + PROOF-POLICY §8.5.1, and keep its experiments E1 to E6. Close issue 28 with + a pointer. (b) Keep the three open. +. *D-6 Open pull requests.* (a) The implementation session completes the + triage table and the owner approves each row. (b) The owner triages alone. + (c) Merge all 17 in order and resolve each conflict. +. *D-7 Bridge centre.* (a) The lock with slices, as in <>. + (b) No centre: each relation lives in one named home, and Mathesis derives + the view. (c) Defer until the registry covers ten repositories. +. *D-8 Proof toolchains.* (a) Pin Agda, Rocq and Lean in the Guix manifest. + (b) Install from release archives with `deviation` records now, and move + to Guix later. Recommended: (b), because it closes the hole this week. + +== What this plan does not do + +* It does not move, copy or regrade any proof in another repository. +* It does not change PROOF-POLICY or any other canon text. +* It does not register Mathesis in `gv-clade-index`. Registration is the + owner's act. The index at `539dd61` has no entry for Mathesis. +* It does not replace the working census before a tested replacement exists. +* It does not edit a licence. + +[appendix] +[[reports]] +== Reports for other repositories + +The assessment found these defects outside Mathesis. Each one is a report. +This plan does not repair them. + +[cols="2,5",options="header"] +|=== +|Where |Report + +|`rsr-template-repo` +|`just validate-rsr` requires `src/interface/abi`, `ffi` and `generated` in +each repository. The canon capability model calls them vestigial where the +`abi` and `ffi` capabilities are not declared (<>). + +|`rsr-template-repo` +|No workflow runs `just validate-claude-md`, `just validate-coapt`, +`just test` or `just quality`. + +|`rsr-template-repo` +|The mint's name pass changes the meaning of some sentences (<>). + +|`rsr-template-repo` +|`scripts/check-proofs.sh` passes a Rocq file with `Admitted` and a Lean file +with `sorry`. + +|`standards`, `deed_lint.js` +|`readProofReceipt`, as read at `be39f90`, accepts `--cubical` in place of +`--cubical-compatible`. It has no field for the proof profile that +PROOF-POLICY §8.2 requires for full `--cubical`. + +|`standards`, `deed_lint.js` +|The reader derives `PWG-1` when each counted receipt is at the source +commit. A receipt has no field that separates a headless CI run from a local +run. + +|`standards`, PROOF-POLICY +|§2.2 does not say who may record `RECONCILED`. Home repositories follow +three different practices (<>). + +|The proof-craft scanner +|Four open pull requests change the Mathesis copy of `proof-holes.sh` +(<>). + +|`occupancy-types`, `autoformal-fidelity` +|Each one still carries the template's deed, named +`rsr-template-repo_chora.deed`, with the canonical name +`rsr-template-repo`. +|=== + +[appendix] +[[triage]] +== Provisional triage of the open pull requests + +The table comes from commit subjects and file lists at 2026-11-10. Each row +needs a full read of the diff (<>). Each pull request conflicts with +`main`. + +[cols="1,4,4",options="header"] +|=== +|PR |Content that `main` does not have |Provisional disposition + +|16 +|An audit report of the ECHIDNA proof route. The record of ruling D-10. +|Keep both as documents. Drop the row changes. + +|17 +|Nothing found. The status-document fix and the canon 2.1.5 pin are on +`main`. +|Close as superseded. + +|20 +|Template boilerplate matched by blob, first implementation. +|Choose one of 20 and 26. + +|22 +|Tests for status-document choice. The trope-checker grades, typed into the +register. +|Keep the tests. Move the grades to the registry (<>). + +|24 +|A partial refresh that records provenance. A finding: one occupancy proof +fails under its pinned Lean. +|Keep the provenance design for <>. Keep the finding. + +|25 +|A fix that keeps rows when the template list is empty. +|Check `main` for the same fix. Then close or rebase that part. + +|26 +|Template boilerplate matched by path and blob, second implementation. +|Choose one of 20 and 26. + +|27 +|A scanner that skips comments and strings. Idris2 signatures without +clauses, reported as axiom candidates. +|Keep the scanner changes. Send them to the scanner's source. + +|31 +|The census sees proofs written in Rust (Creusot, Pearlite, Verus). +|Keep. PROOF-POLICY §1.2 makes this necessary. + +|34 +|Verus rules. +|Fold into 31. Close the remainder. + +|36 +|25 repositories that the frame lacks. A derived row count. +|Keep both. Drop the rerun data. + +|39 +|The owner's proofs in one fork, with the fork listed. +|Keep the fork listing. Take the row from the next census. + +|40 +|A census rerun. +|Close as superseded by the next single run. + +|41 +|A row refresh tool with atomic publication and tests. +|Choose one refresh tool among `main`, 24, 41 and 42. + +|42 +|Wording that says the catalogue has no grades. +|Keep the wording. See 41. + +|44 +|Ada counted as SPARK only where the code opts in. +|Keep the scanner change. Drop the row changes. + +|45 +|Nothing found beyond a rerun. +|Close as superseded. +|=== + +`scripts/census/proof-holes.sh` is a copy of the scanner from the proof-craft +skill. Pull requests 27, 31, 34 and 44 change the copy. The same change must +reach the source, or the two will differ. From d112cbbb0a929a41e4afa9a621024d14d2000b56 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 15:51:41 +0000 Subject: [PATCH 2/3] docs(proposals): propose the mathesis research programme Join the owner's written directions into one programme anchored here: the algebra of status, bridges between systems, theorem to code, evidence for decisions, and a propose-and-dispose horizon. Each statement is pre-registered with a falsifier. Each experiment has a pass condition. The survey appendix quotes 52 repositories at fixed commits. Nothing is proved or changed by this document. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- .../mathesis-research-programme.adoc | 1119 +++++++++++++++++ 1 file changed, 1119 insertions(+) create mode 100644 docs/proposals/mathesis-research-programme.adoc diff --git a/docs/proposals/mathesis-research-programme.adoc b/docs/proposals/mathesis-research-programme.adoc new file mode 100644 index 0000000..2ea9285 --- /dev/null +++ b/docs/proposals/mathesis-research-programme.adoc @@ -0,0 +1,1119 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Mathesis research programme: evidence, bridges and loss +:toc: preamble +:toclevels: 2 +:sectnums: +:icons: font + +Status: *proposed, not ratified* (2026-11-10). This document claims no proved +result. A statement marked *pre-registered* is a statement to prove or to +refute. A sentence marked *reading* is the view of the author of this +programme. Each fact about another repository names that repository and its +commit in <>. Each such fact is that repository's own claim. This +session checked no proof. + +The companion document is +link:mathesis-re-anchoring.adoc[the re-anchoring plan]. The plan puts the +repository in order. This programme says what research the ordered repository +supports, and who gains from it. + +== The programme in one page + +*The question.* The owner's research note on types, tropes and identity asks +one question. When may "a proposition or transition cross between those +spaces without conflating distinct identities or inventing authority, +evidence or preserved particularity"? This programme takes one kind of +crossing first: a mathematical claim that crosses between systems. Mathesis +is the anchor for that kind. + +*The crossings.* A claim crosses in five ways: + +. from one prover to another (a recheck leg); +. from a theorem to the code that implements it; +. from a theorem to the estate rule that relies on it; +. from a proof to the ledger row that reports it; +. from many ledger rows to one published view. + +Each crossing can lose something. The programme asks, for each one, what is +preserved, what is forgotten, and what evidence shows it. + +*What the estate has already.* The type family has one algebraic kernel +(`resource-algebra`), three core theories (echo, epistemic and residual +evidence) and several applications. The proof policy has a closed status +vocabulary, a grade ladder and a receipt format. These two bodies of work are +not yet joined. + +*The proposal.* Join them, in four lines of work and one horizon: + +[cols="1,3,3",options="header"] +|=== +|Line |Subject |First result to aim for + +|1 +|The algebra of status +|The ledger tokens are a sub-algebra of the family's bottleneck grade. + +|2 +|Bridges between systems +|A record of what each existing statement comparison preserves and forgets. + +|3 +|From theorem to running code +|One vertical slice, with its composite status computed and not typed. + +|4 +|Evidence for decisions +|A sound three-valued verdict for one synthetic cash forecast. + +|Horizon +|Propose and dispose +|A labelled corpus of bridges that an exact checker has accepted or refused. +|=== + +*The one idea.* Status is a monotone function of evidence. More evidence does +not lower a status. Less evidence does not raise one. A chain of steps is as +strong as its weakest step. Each line of work is this idea in one setting. + +== Where the programme comes from + +The programme adds no new direction. It joins directions that the owner has +already written down in separate places. + +[cols="2,3,3",options="header"] +|=== +|Source |What it fixes |Use in this programme + +|Manifesto, `hyperpolymath/manifesto` +|Assurance is a relation among a claim, its evidence, the model, the residual +uncertainty and an accountable authority. "Probabilistic generation may +propose; only symbolic method may dispose." +|The record model. The horizon. + +|Research note on types, tropes and identity, `hyperpolymath/vcl-ut` +|Identity and equivalence need a named criterion. A bridge is partial and +direction-sensitive. It says what it preserves and what it forgets. No +unified calculus is required. +|The rules for line 2. The limits in <>. + +|PROOF-POLICY, `metadatastician/standards` +|Which prover carries which obligation. The five status tokens. The +correspondence states. The Proof Witness Grades and the receipt. +|The objects that lines 1 to 3 study. + +|ECHIDNA proof-route plan, `metadatastician/standards` +|Ladder rows 2, 7 and 12. Ruling D-10: the token-lattice theory lives in +Mathesis. Experiment X-PF1: is a total order on tokens enough? +|The first theorems of line 1. + +|Kautz-ladder plan, `metadatastician/standards` +|Rungs K0 to K6, each with a falsifier. "K3 and K4 are where the proof and +type repositories pay off." +|The horizon, and the habit of a falsifier for each step. + +|Architecture brief, Mathesis +|The dogfooding experiments A, B and C. The owner direction on the +correspondence record. +|Lines 2 and 3. + +|Applied-systems area, Mathesis +|Evidence status on each input. "Missing" is not zero. +|Line 4. +|=== + +== What exists today + +This section reports the survey of <>. It quotes each repository's +own words. + +=== One kernel + +`resource-algebra` says that it is "a kernel module of the family, not a +family of its own". Its record `ResourceAlgebra` has two operations. +Alternatives (`⊕`) form an idempotent commutative monoid. Sequence (`⊗`) +forms a monoid. The order comes from the alternatives: `a ≼ b` when +`a ⊕ b ≡ b`. The kernel proves that `⊕` is the join of that order. It proves +that each dioid is ordered, so sequence is monotone. + +Four instances exist: `Loss`, `MaxPlus`, `HWM` and `MinMax`. The kernel also +states what is *not* true. No strict morphism leaves `HWM` for an algebra +with `𝟘 ≢ 𝟙`. "An occupancy bound is not a cost bound." + +`choreographic-types` and `occupancy-types` import the kernel. +`autoformal-fidelity` imports its prelude. + +=== Three core theories + +[cols="1,3,3",options="header"] +|=== +|Theory |Its own description |Central object + +|`echo-types` +|"proof-relevant fibers as first-class witnesses for structured information +loss". "This is the standard preimage fiber, not a new construction." +|`Echo f y`: the sources that a map sends to `y`. + +|`residual-evidence-types` +|"the alternative explanations compatible with an observation and its +declared evidence" +|`Candidate`: a fibre refined by evidence. `Revision` and `Retraction`. + +|`epistemic-types` +|"standpoint-indexed epistemic modalities, separating knowledge, belief, and +warrant" +|`Warrant` and `SoundWarrant`. Result L-2: "Warrant evidence does not imply +its claim". +|=== + +`residual-evidence-types` says that its verdicts "are a view on Epistemic +over Echo". `nextgen-typing` coordinates the family map and the glossary. + +=== Applications of the family + +* `autoformal-fidelity` asks: "does a formal artefact F say what its informal + source S says?" It defines `Faithful = RoundTrip × Covered`. Its statement + F-2 says: "Round trip is blind to additions". +* `invariant-path` "traces what a claim _means_ when it crosses from one + domain into another". It says that it is "a claim-path debugger, not a truth + engine". +* `trope-checker` gives "a sufficiency verdict" for a graded Trope IR. Its + calculus names "the bottleneck (max–min) grading of a path by its weakest + link". +* `secret-types` proves noninterference "over any Lattice record". It lists + the laws that the proof uses, and it shows by countermodels that each law + is necessary. `lintel` instantiates the theorem. +* `MetaManifold-Evidence` answers "is the taxon present, absent, or + undecided?" from read counts and a noise bound. Its theorem + `never-strengthens` says that "more noise never strengthens a verdict". +* `EpistemicTypes.jl` attaches a receipt to each row of a taxonomic table. +* `hvn-dehallucinator` keeps agent task state outside the model. "Only an + independent verifier may write COMPLETE." + +=== Systems, proof tools and languages + +* *Systems with theory inside.* `januskey` grades its file operations "in + resource-algebra's Loss instance". `absolute-zero` proves that a program + computes nothing, or reveals nothing. `squeakwell` states a recovery ladder + and says: "No proof lives in this repository." Its proofs are in + `echo-types`, `verisimdb` and `tropical-types`. +* *Languages.* The Echo fibre is mechanised in six language repositories: + `my-lang`, `ephapax`, `eclexia`, `tangle`, `phronesis` and `jtv-lang`. Each + one mirrors or imports the Agda source. `jtv-lang` calls its + correspondence "`argued`, not bridged". Two of them disagree: `my-lang` + says that Echo is "NOT a graded comonad", and `eclexia` keeps "the + graded-comonad-of-loss reading". +* *Quantities.* `affinescript`, `my-lang` and `typell` use the usage + quantities 0, 1 and ω. `ephapax` says that `resource-algebra` "cannot + host" them. `affinescript` records an owner ruling: the laws of that + semiring go in `resource-algebra` "as a non-idempotent tier". +* *Statistics.* Four Julia packages keep Agda proofs of exact identities + about models: the centred log-ratio, the Benjamini-Hochberg step-up, + rounding and Fisher's exact test. They state their limits. On control of + the false discovery rate, `CompositionalDA.jl` says: "Nothing in `proofs/` + bears on it". +* *Knots.* `tangle` is a language in which "program equivalence is defined by + isotopy". `quandledb` separates candidate matches from certified + equivalence. `KnotTheory.jl` has no proof file. +* *Accounts of evidence.* `gnpl` "turns an evidence base into an _account_". + Its theory document credits provenance semirings and AGM revision. +* *Proof tools.* The survey reader for ECHIDNA, echidnabot, Hypatia and + proof-burrower stopped at a usage limit. For these four, the programme + uses only the two ECHIDNA plans in the standards repository. It also uses + the first line of the proof-burrower README: "Find the mathematical home + of a proof goal." + +=== A method that is already in use + +The surveyed repositories share habits that few projects have: + +* *Pre-registration.* `choreographic-types` and `autoformal-fidelity` state + each theorem before the proof exists. +* *Law census.* `secret-types` and `choreographic-types` record exactly which + laws a proof uses. +* *Necessity by countermodel.* `secret-types` shows that the theorem fails + when one law is removed. +* *Negative controls.* `residual-evidence-types` keeps 17 rejection controls. + `firmboot` keeps seven false-claim controls. THY-1 in Mathesis keeps four. +* *Agreement by exhaustion.* `residual-evidence-types` proves by `refl` that + its checker matches a finite explorer on 546 configurations. +* *Recorded retraction.* `echo-types` keeps a retraction log, and it closes + one line of work "negatively". `protocol-squisher` is frozen "as its own + provenance and negative result". +* *Three outcomes.* `proven-tests-and-benches` says: "Three outcomes, not + two". Its third outcome is "NO CHECK WAS PERFORMED". The verdicts of + `residual-evidence-types` and `MetaManifold-Evidence` have the same third + value, and so does the "missing" status of the applied-systems area. + +Nobody has written this method down in one place. <> proposes that +Mathesis does. + +== The question and five fixed points + +The fixed points are commitments that the owner's documents already make. +The programme does not test them. It builds on them. + +[cols="1,3,3",options="header"] +|=== +|Fixed point |Statement |Source + +|FP-1 +|A claim is tied to its evidence, the model in which the evidence has force, +the residual uncertainty and an accountable authority. +|Manifesto, "the assurance turn" + +|FP-2 +|Status is derived from evidence. Nobody asserts it. +|PROOF-POLICY §8.4. Ledger rule 3 of the README and EXPLAINME standard. + +|FP-3 +|Identity and equivalence hold under a named criterion. A crossing says what +it preserves and what it forgets. +|Research note. Manifesto: "identity defined by equivalence rather than +asserted". + +|FP-4 +|A learned component proposes. An exact checker decides. +|Manifesto, pillar 2. Kautz-ladder plan. + +|FP-5 +|Abstraction leaves something behind, and the loss is named. +|Manifesto: "abstraction always leaves something behind". `echo-types`. +|=== + +[[line-0]] +== Line 0: the theorem dossier (method) + +*Question.* What must a report of a machine-checked theorem contain? A +stranger must be able to trust it as far as the evidence goes, and no +further. + +*Proposal.* Describe the method of the previous section as one checklist, the +*theorem dossier*: + +. the statement, registered before the proof; +. the checker, its version, its flags and the import cone; +. the laws and axioms that the proof uses; +. a countermodel for each law that the statement needs; +. the negative controls that the gate rejects; +. the receipts, with their states; +. each bridge, with what it preserves and forgets; +. the retractions. + +The registry can then show which parts of the dossier each claim has. This is +a census of practice. It is not a new grade. + +*First experiment.* Score ten existing theorems against the checklist: THY-1, +five from `januskey`, two from `secret-types` and two from `lintel`. + +*Pass condition:* each item is found, or its absence is stated, without a +question to the author. + +*Who gains.* The owner gains one description of a method that is now spread +over many repositories. Other projects gain a concrete answer to the question +"what does `verified` mean here?". + +[[line-1]] +== Line 1: the algebra of status + +*Question.* The estate has five status tokens, a weakest-step rule, a fold +over attempts and a grade ladder. Are these one algebra, and is it one that +the type family already has? + +=== What exists + +* The tokens: `open`, `argued`, `tested-only`, `proven-with-postulates` and + `proven` (README and EXPLAINME standard, proof ledger). +* Ledger rule 3: "A row's status may only be as strong as the weakest step it + depends on." +* Ladder row 2 of the ECHIDNA proof-route plan: "Token order and weakest-step + meet are lawful". Row 12: the status fold over attempts "is a join on the + token lattice". Row 7: "Retraction never raises a level." +* Ruling D-10: the theory of rows 2 and 12 lives in Mathesis. +* The `MinMax` instance of `resource-algebra`: alternatives take the minimum + ("the better path"), and sequence takes the maximum ("the worst hop"). + +=== Pre-registered statements + +The statements use this order, weakest first: `open`, `argued`, +`tested-only`, `proven-with-postulates`, `proven`. PROOF-POLICY §5 lists the +tokens in the reverse of this order. The owner rules on the order before any +proof starts. + +S-1 (the tokens are a bottleneck grade):: +Take the join of the order as alternatives and the meet as sequence, with +`open` as `𝟘` and `proven` as `𝟙`. Then the tokens are a `ResourceAlgebra` +that is a dioid and in which `𝟘` annihilates. The map below is an injective +strict morphism (`Hom`) into `MinMax`. ++ +[cols="2,1",options="header"] +|=== +|Token |`MinMax` grade +|`proven` |`fin 0` +|`proven-with-postulates` |`fin 1` +|`tested-only` |`fin 2` +|`argued` |`fin 3` +|`open` |`inf` +|=== ++ +*Consequences.* Rows 2 and 12 follow from the kernel's own lemmas. The join +laws give a fold that does not depend on order or on repetition. The dioid +law gives a monotone weakest step. + +*Falsifier.* `meet(proven, argued) = proven` is derivable (row 2), or two +orders of one fold give two statuses (row 12). + +S-2 (positive evaluation is monotone):: +Take an expression built from atoms with `⊕` and `⊗` only. Its value in an +ordered resource algebra is monotone in the grades of the atoms. ++ +*Consequences.* A new attempt does not lower a status. A broken leg does not +raise one. Trust withdrawn from a checker version does not raise one. These +are §8.4 rule 4 of PROOF-POLICY and the status half of row 7. + +*Falsifier.* An expression and two atom gradings, one below the other, whose +values are in the opposite order. + +S-3 (the grade is a function of the receipt):: +Write PROOF-POLICY §8.2 as a total function from the facts of a receipt to a +grade. The function is monotone in the set of counted legs. The canon reader +agrees with it on each combination of route, token, state and receipt state. ++ +*Method.* The domain is finite. Generate the table from the reader, and let +Agda compare it with the function by `refl`. This is the method that +`residual-evidence-types` uses for its 546 configurations. + +*Status aimed for.* The function and its monotonicity are theory. The +agreement of the reader is `tested-only`, by exhaustion. + +*Falsifier.* One row where the reader and the function differ. + +=== Research questions + +Q-1.1 Is a chain enough?:: +Experiment X-PF1 of the ECHIDNA plan asks whether a total order on tokens is +enough for the weakest-step rule. A chain puts `tested-only` above `argued`. +Then a claim that rests on one tested step and one argued step is `argued`, +and the report forgets the tested step. *Reading:* the chain is a lossy view +of a richer value, and the loss can be measured with the fibre of +`echo-types`. The question is which decisions need the richer value. + +Q-1.2 What does a recheck leg buy?:: +*Reading:* a theorem with three legs rests on a disjunction. The claim holds +if the Agda kernel is sound. It also holds if the Rocq kernel is sound and +the Rocq bridge is faithful. The same is true for Lean. More legs weaken the +assumption about kernels. Each leg adds an assumption about a bridge. In the +kernel's +terms, legs are alternatives and the parts of one leg are a sequence. The +question is whether this *trust expression* can be computed from a receipt, +and whether the grade is its monotone image. `epistemic-types` already has +the vocabulary: its result L-3 derives a claim from a proof "only from an +accepted sound checker". + +Q-1.3 Which conversions between grade schemes are sound?:: +PROOF-POLICY §8 lists seven schemes named "grade" or "level" and says: "None +of these converts into another." `resource-algebra` proves statements of this +kind with morphisms and with separations. The question is which maps between +the estate's schemes are morphisms, which are lax, and which a countermodel +refutes. The first map is the one in row 2: token to HYP-01 level. + +=== First experiments + +. *E-1.1* Prove S-1 in Agda against `resource-algebra` at a pinned commit. + Re-prove it in Rocq and Lean. + + *Pass condition:* the receipt of Mathesis derives `PWG-2ii` for S-1 through + the canon reader, with no axiom. +. *E-1.2* Prove S-2 once, for each ordered resource algebra. + + *Pass condition:* the token corollaries need no case analysis of their own. +. *E-1.3* Run the table of S-3 against the canon reader and against the + present Mathesis tool. + + *Pass condition:* the reader agrees on each row. The count of rows where + the Mathesis tool differs is published. The plan expects a count above + zero, because the two programs use different rules today. + +=== Who gains + +* *The owner's theory.* The proof ledger joins the type family. Evidence + status becomes a grade in the exact sense of the family's other grades. +* *The owner's engineering.* Each program that computes a status or a grade + can be tested against one checked specification. +* *Others.* A small, checked algebra for the composition of levels. + *Reading:* many assurance schemes define levels and leave their + composition informal. + +[[line-2]] +== Line 2: bridges between systems + +*Question.* A statement in one system is said to be the same as a statement +in another. What exactly is preserved? What is forgotten? How can a third +party check it? + +=== What exists + +* The correspondence states of PROOF-POLICY §2.2, and the rule that "a + successful compilation in each prover does not establish that all proved + the same proposition". +* Written statement comparisons in at least five repositories: Mathesis + (THY-1), `januskey` (T-1), `lintel`, `MetaManifold-Evidence` and + `hvn-dehallucinator`. +* The theory of `autoformal-fidelity`: a round trip rules out collapses and + is blind to additions. Faithfulness needs coverage too. +* The classification of `invariant-path`: `ValidPath`, `Overextended`, + `Conflation`, `Incomplete` and `Abstain`. +* A blocked transport route. THY-1 records that the Agda to Dedukti + translator fails on one construct, and that the Lambdapi exporters drop + rewrite rules. +* Two structures named `ResourceAlgebra`, one in Agda and one in Lean, with + different laws and an open bridge (`resource-algebra`, item M-2). +* A recorded mismatch. `absolute-zero` says that its OND-5 in Agda and its + OND-5 in Coq and Lean are "different propositions". +* A map inside one home. `verisimdb` says that each of its theorems "is an + instance of a more general Echo-Types theorem". It says that its bridge + from Coq to Agda is "Currently NOT IMPLEMENTED". +* A possible repeat. `januskey`, `valence-shell` and `absolute-zero` each + prove that undo in reverse order restores a state. *Reading* of the survey: + no file compares the three statements. + +=== Research questions + +Q-2.1 What must a statement comparison record?:: +The five existing comparisons are prose. Each lists differences of encoding: +universes, the empty type, equality, implicit arguments. Collect the +differences into a closed list. For each one, state when it preserves the +statement and when it adds a side condition. + +Q-2.2 Is a round trip enough?:: +PROOF-POLICY §2 allows a comparison "by a round trip back through Dedukti". +`autoformal-fidelity` F-2 says that a round trip cannot see an addition. +*Reading:* a bridge that rests on a round trip alone is weaker than a bridge +that also shows coverage. The question is whether the estate's comparisons +show coverage. + +Q-2.3 Can a bridge hold by construction?:: +For statements in a small fragment, write the statement once and generate the +Agda, Rocq and Lean forms. The bridge then rests on the generator. The canon +has a precedent: `ZenodoDeposits.jl` regenerates its proved table, and the +row is `tested-only`. + +Q-2.4 Where does transport fail?:: +Keep each failure of the Agda to Dedukti to Rocq or Lean route as a minimal +reproducer with tool versions. The collection is a map of the frontier, and +each entry is a report for the tool's authors. + +Q-2.5 When are two legs independent?:: +The research note asks when "multiple views count as independent +corroboration, rather than duplicated presentations of one witness". +*Reading:* a transported leg checks the same argument with a second kernel. A +re-proved leg can be a second argument. In a trust expression, two legs are +independent with respect to an assumption when they do not share it. A +comparison that one reader wrote for both legs is a shared assumption. + +=== First experiments + +. *E-2.1* Write the five existing comparisons as bridge records, with the + fields of the re-anchoring plan. + + *Pass condition:* each record states its criterion, what it preserves and + what it forgets, from the home's own text. A field that the text does not + support is recorded as missing. +. *E-2.2* Record the `ResourceAlgebra` pair as a bridge. + + *Pass condition:* the record names each law that differs. Its relation is + not `same-statement`. +. *E-2.3* Generate the three forms of S-1 from one source. + + *Pass condition:* the hand-written proofs of E-1.1 check against the + generated statements with no edit to a statement. +. *E-2.4* File the THY-1 reproducer with the translator's authors, and keep + it in the frontier collection. + + *Pass condition:* the reproducer fails in the same way at the pinned + versions on a clean machine. +. *E-2.5* Write one bridge record for each of the six Echo mirrors. + + *Pass condition:* each record says whether the mirror imports the Agda + source or restates it, and what the restatement forgets. The disagreement + about the graded comonad is recorded as a question. It is not resolved by + the record. + +=== Who gains + +* *The owner's theory.* The identity question gets a body of worked cases, + each with a criterion. Line 2 is the research note's first stage, + "vocabulary and discovery", applied to mathematics. +* *The owner's engineering.* `RECONCILED` becomes a state with a checkable + record. ECHIDNA gets labelled pairs, with refusals among them. +* *Others.* A closed list of encoding differences between provers, drawn from + real cases. *Reading:* projects that keep one theorem in two provers have + no common form for the statement comparison. + +[[line-3]] +== Line 3: from theorem to running code + +*Question.* How much of a theorem's guarantee reaches the running system, and +can the answer be computed? + +=== What exists + +* PROOF-POLICY §1.1: a caller proved against an assumed contract is "proved + _relative to the assumption_". +* The ledger rule that a theorem about a model is proved "for the model", and + that the link from model to code "is its own row". +* The Aeneas rule of §4.1: the theorem about the model and the correspondence + of the model to the code are two rows. + +* `januskey`: theorem T-1 says that "undoing a fully executed transaction's + operations in reverse order restores the state it began in". Its own record + gives T-1 `PWG-2ii`. Row T-10, that the Rust operations "refine the abstract + open, edit and settle transitions", is OPEN. Row G-2, the link from Idris2 + to Agda, is "by transcription" and ASSUMED. +* `valence-shell`: "The Rust CLI refines the proven model" is `argued`. +* `verisimdb`: the Rust contracts enter the Rocq development as axioms + "checkable by a Rust property test". +* `vcl-ut`: `WireConformance` "proves, by `Refl`, that this decoder agrees + byte-for-byte with the trusted Rust encoder". +* `protocol-squisher` keeps a negative result: "Toy-model proofs were + presented as system verification." +* `proven` calls itself "the estate trust root". Its draft affirmation says: + "It is not fully proven today." + +=== Research questions + +Q-3.1 Can the composite status be computed?:: +For one chain from theorem to code, write each rung as a row with its token. +Compute the status of the whole with S-2. Compare it with the status that +the documents state. + +Q-3.2 Can a cited law be generated?:: +Row 2 of the ECHIDNA plan lets the Idris2 ABI state the token laws "for its +own types". The ABI cites the Agda theorem as an `argued` row. If the ABI +laws are generated from the Agda source, the row can rise to `tested-only`. + +=== First experiments + +. *E-3.1* Choose one vertical slice with the owner. The survey suggests + `januskey` T-1 with T-10 and G-2. Write its rungs as claims and bridges. + Compute its composite status. + + *Pass condition:* the computed status is not stronger than the weakest + rung, and each document that states a stronger status is listed. +. *E-3.2* Generate the Idris2 statement of the token laws from the source of + S-1. + + *Pass condition:* a change to the Agda order makes the generated file + differ, and the gate fails until it is regenerated. + +=== Who gains + +* *The owner's engineering.* A dashboard that states a status for a system + can be checked against the weakest rung. +* *Others.* A computed, visible composite status is a small tool against + overclaim. *Reading:* the gap between a proved model and the shipped code + is a common weak point of verified software. + +[[line-4]] +== Line 4: evidence for decisions + +*Question.* Can the evidence discipline of the proof ledger serve a decision +about money, capacity and people? + +=== What exists + +* The applied-systems area: five evidence statuses, from "verified + observation" to "missing", and the rule that a missing input stays blank. +* Its liquidity method: "Missing opening cash makes the cash feasibility + verdict unknown." +* `MetaManifold-Evidence`: a verdict of `entailed`, `refuted` or `unresolved` + from counts and a noise bound, with `verdict-sound` and `never-strengthens`. +* `EpistemicTypes.jl`: a receipt for each row, and a merge test that can + refuse. + +=== Pre-registered statements + +S-4 (a sound cash verdict):: +Give each weekly receipt and payment as an interval. Give a cash floor for +each week. The verdict is `meets the floor`, `breaches the floor` or +`undecided`. The verdict is sound: `meets` holds for each value in the +intervals, and `breaches` holds for each value in the intervals. A missing +input is an unbounded interval. + +S-5 (more uncertainty does not strengthen):: +If each interval grows, a verdict of `undecided` stays `undecided`, and no +verdict changes from `breaches` to `meets` or from `meets` to `breaches`. + +*Reading:* S-4 and S-5 have the shape of `verdict-sound` and +`never-strengthens`. The fibre is the set of cash paths that the inputs +allow. If the reading is correct, the proofs reuse `residual-evidence-types` +at a pin, as `MetaManifold-Evidence` does. + +=== Research questions + +Q-4.1 Is evidence status a grade?:: +The applied statuses and the proof tokens are both ordered vocabularies with +a weakest-input rule. The question is whether the applied statuses form a +resource algebra, and whether a map to the proof tokens is a morphism. The +research note warns against "implicit exchange" between measures, so the +default answer is that no map exists until one is proved. + +Q-4.2 When may two views be added?:: +The accounting method keeps five views and says that they are "not amounts to +add together indiscriminately". `EpistemicTypes.jl` has a merge test with +three results. The question is what the merge test is for cost views. + +=== First experiments + +. *E-4.1* Write one synthetic 13-week forecast as records, each with an + evidence status. Compute the verdict. + + *Pass condition:* with the opening cash removed, the verdict is + `undecided`. It is not a number. +. *E-4.2* Prove S-4 and S-5 in Agda. + + *Pass condition:* the receipt of Mathesis derives `PWG-3` for both, and the + executable check agrees with the proof on a generated table. + +=== Who gains + +* *The owner's theory.* The residual-evidence verdict gets a second applied + domain, far from metagenomics. That tests how general it is. +* *The owner's practice.* The management-accounting research gets a checked + core that refuses to turn a missing input into a number. +* *Others.* A forecast method that says `undecided` when an input is + missing. *Reading:* small organisations often decide on forecasts with + missing inputs. + +[[horizon]] +== Horizon: propose and dispose + +*Question.* Can a learned component propose bridges and proofs while an exact +checker keeps the last word? + +=== What exists + +* Rungs K3 and K4 of the Kautz-ladder plan. At K3, "learned front-ends emit + symbolic IR for exact reasoners". At K4, "provers and executors generate + training data". +* The owner direction of 2026-11-09 in the architecture brief. Translations of + verified Rust are "a corpus for ECHIDNA, not proof evidence". ECHIDNA + "learns from these pairs how statements correspond across systems". +* The ECHIDNA engineering plan. It says that "no trained model weights + exist", and that learned advice may "reorder candidates but never decide a + verdict". +* A large stock of work for a proposer. `echo-types` reports 717 `ungraded` + pins of 722. `marches` reports 211 `ungraded` theorems, each with no Agda + witness. + +* `proof-burrower` searches prover libraries "for the place where that goal + already lives". An index of the estate's own declarations would be one + more library for it. +* `statistikles` calls itself "a _Kautz Type 3 neurosymbolic_ statistical + analysis assistant", with "zero neural inference in the computation path". + +=== Research questions + +Q-H.1 What is the task?:: +Given two artefacts, a proposer writes a bridge record: the relation, the +criterion, and what is preserved and forgotten. An exact checker or a +reviewer accepts or refuses it. The labels come from the records of line 2. +The refusals are as useful as the acceptances: each negative control and +each countermodel is a hard case. + +Q-H.2 How is a proposer measured?:: +The Kautz-ladder plan gives the falsifier for K3: "Every proposal is accepted +(the exact reasoner is not refusing anything) or every proposal is rejected +(the front-end is noise)." A proposer passes only between these two ends. + +Q-H.3 What does a recheck leg cost?:: +A model proposes a Rocq or Lean proof for a generated statement (Q-2.3), and +the kernel checks it. The count of accepted legs for each hour of work is a +number that the estate does not have today. The number decides whether +`PWG-2ii` across the estate is a matter of months or of years. + +=== First experiments + +. *E-H.1* Define the corpus as a view over bridge records and receipts. It + needs no new store. + + *Pass condition:* each corpus row points to a record whose state came from + a checker or from a reviewed comparison. No row has a label that a model + wrote. +. *E-H.2* Take 20 `ungraded` Agda theorems from two repositories. Let a model + propose each Rocq leg and each Lean leg against a generated statement. + + *Pass condition:* the counts are published with their denominator. Each + accepted leg stays `BRIDGE-PENDING` until a person reviews the comparison. + +=== Who gains + +* *The owner's theory.* A measured cost for a recheck leg, and with it a + realistic plan for the 900 and more theorems that are `ungraded` today. +* *The owner's engineering.* A first honest reading for rungs K3 and K4, on + data whose labels are exact. +* *Others.* A corpus of paired statements that records refusals. *Reading:* + most public sets of paired statements hold accepted pairs only. + +== Order of work + +The lines depend on each other in one direction only. + +. Line 0 and E-1.1 start first. They need only this repository and the + kernel. +. E-1.3 follows stage 2 of the re-anchoring plan, which moves the registry to + the canon reader. +. Line 2 starts when the bridge record has a ruling (decision D-7 of the + plan). +. Line 3 needs one home repository that agrees to be the slice. +. Line 4 can run at any time. It shares only S-2 with the other lines. +. The horizon waits for lines 1 and 2 to produce records. + +The Kautz-ladder plan has a standing rule: nothing above its first wave is +committed before the experiments have numbers. This programme keeps the same +rule. Each experiment above has a pass condition that was written first. + +== Benefits in one table + +[cols="1,2,2,2",options="header"] +|=== +|Line |The owner's theory |The owner's engineering |Theory and engineering in general + +|0 +|One written method +|A dossier check in the registry +|A concrete meaning for "verified" + +|1 +|The ledger joins the type family +|One specification for each grade computer +|A checked algebra for level schemes + +|2 +|Worked cases for the identity question +|A checkable `RECONCILED` +|A list of encoding differences between provers + +|3 +|A test of the weakest-step rule on a real chain +|A computed status for a system +|A tool against overclaim for verified software + +|4 +|A second domain for residual evidence +|A forecast that can say `undecided` +|Evidence-typed decision models + +|Horizon +|Data on what a learned proposer can do +|Rungs K3 and K4 of the ladder +|A corpus with exact labels +|=== + +== How to tell if the programme fails + +A programme that cannot fail is not research. Each sign below would show that +a line is not worth its cost. + +* *Line 1.* The proofs of rows 2 and 12 through the kernel are longer than + direct proofs, or no program is ever tested against the specification. +* *Line 2.* The five existing comparisons do not fit one record without + invented fields. Or the closed list of encoding differences keeps growing + after twenty cases. +* *Line 3.* No home repository can state the rungs of one slice. +* *Line 4.* S-4 needs assumptions that no real forecast meets. +* *The whole.* After two quarters, no result of the programme has changed a + rule, a gate or a document in any other repository. + +[[limits]] +== What the programme does not claim + +* It does not claim one calculus for the type family. The research note says + that none is required, and the kernel's own separations show where the + instances differ. +* It does not claim that a status token, a grade and an evidence status are + the same thing. Each map between them is a question until it is proved. +* It does not claim that a bridge gives identity. A bridge holds under its + criterion. +* It does not claim that a recheck leg is an independent witness of truth. + Q-1.2 and Q-2.5 ask what a leg does witness. +* It does not move any theorem out of its home repository. +* It does not treat a proposal of a model as evidence. + +== Decisions for the owner + +Each decision lists the most elegant and correct long-term arm first. The +programme assumes arm (a). + +. *R-1 The order of the tokens.* (a) The chain of S-1, as PROOF-POLICY §5 + lists it. (b) A partial order in which `tested-only` and `argued` are not + comparable. Arm (b) needs a new bottom value for a mixed claim. +. *R-2 The kernel import.* (a) The token theory imports `resource-algebra` at + a pinned commit, as `januskey` and `choreographic-types` do. (b) The token + theory is self-contained, and a bridge record joins it to the kernel. +. *R-3 The home of S-2.* (a) Mathesis, because the expression language is the + ledger's. (b) `resource-algebra`, as a kernel lemma. +. *R-4 The first slice for line 3.* The owner names the repository. +. *R-5 The dossier.* (a) Mathesis describes the method and reports it as a + census. (b) The method goes to the standards repository as policy first. + +[appendix] +[[survey]] +== Survey of the estate + +Read on 2026-11-10 from the default branch of each repository. Each entry +gives the commit that was read. Fenced readers extracted the entries from +documentation and proof headers. The author of this programme checked the +quoted kernel module, the research note and the manifesto first-hand. + +A status in the third column is the repository's own statement. Some +repositories still use the older wording "Grade 3" for what PROOF-POLICY §8 +now calls `PWG-3`. + +=== The type family + +[cols="2,4,3",options="header"] +|=== +|Repository and commit |Its own description |Status that it states + +|`resource-algebra` `aac649c` +|"a kernel module of the family, not a family of its own" +|PROVEN rows are `PWG-3` at a commit with a passing run. "no Rocq or Lean leg +exists" + +|`echo-types` `b6c8b97` +|"proof-relevant fibers as first-class witnesses for structured information +loss" +|Of 722 pins: `PWG-2ii` 5, `ungraded` 717 + +|`epistemic-types` `bfcee6e` +|"standpoint-indexed epistemic modalities, separating knowledge, belief, and +warrant" +|"Every theorem is `ungraded`" + +|`residual-evidence-types` `1807536` +|"evidence-indexed residual types" +|No grade recorded. A hosted Agda run is recorded. + +|`nextgen-typing` `bc91959` +|"the coordination monorepo for the hyperpolymath type theory research and +production pipeline" +|XP-1 at "Grade 2i" (older wording) + +|`tropical-types` `f2e465c` +|"applying max-plus (tropical) algebra to resource-aware type systems" +|Lean, no Mathlib. No grade stated. + +|`occupancy-types` `1ba67f7` +|"live-state occupancy as a graded type discipline" +|R-1 to R-5 are `PWG-3` at a commit with a passing job. + +|`choreographic-types` `edf7b88` +|"A pre-registration and research notebook for a graded multiparty-session +and choreographic type theory" +|No grade stated. + +|`secret-types` `ecf164a` +|"a standalone information-flow typing project" +|"mathesis Grade 3 and no higher" (older wording). A receipt deed exists. + +|`lintel` `89ceac3` +|"A privacy lattice for oblivious DNS" +|Six rows at `PWG-2ii`. The comparison is "provisional until the owner +reviews it". + +|`system-et` `04a8b6e` +|"systemet is the theory, not an implementation" +|Of 15 obligations: 2 done, 2 in progress, 11 open. + +|`ordinal-notation` `f27d292` +|"A constructive Agda development of ordinal notations". "Status: frozen" +|"Every theorem is `ungraded`" + +|`trope-checker` `24d1985` +|"The portable trust boundary of trope-particularity" +|Of 24 theory obligations: `PWG-3` 17, `ungraded` 7 + +|`invariant-path` `3a0a8fc` +|"a claim-path debugger, not a truth engine" +|"Nothing in this repository implements these layers." + +|`autoformal-fidelity` `a235db8` +|"An application of the type family to the autoformalisation fidelity +problem" +|Its pre-registration marks three statements PROVEN. No receipt was found. + +|`marches` `e479ebc` +|Region crossing in a routed network as "a typing judgment on traces" +|"`ungraded` 211". Lean only. + +|`firmboot` `034d50c` +|"A research language for evolving running systems under explicit continuity +guarantees." +|95 Lean lemmas with an axiom audit. No grade stated. +|=== + +=== Applications and executable companions + +[cols="2,4,3",options="header"] +|=== +|Repository and commit |Its own description |Status that it states + +|`MetaManifold-Evidence` `051a426` +|"Evidence Mode for MetaManifold as an independent package" +|"22 of 22 theorems at `PWG-3`". Legs `BRIDGE-PENDING`. + +|`hvn-dehallucinator` `da01ab8` +|"An external state-management orchestration framework for LLM agents" +|Three theorems at `pwg` 3. Legs `BRIDGE-PENDING`. + +|`EchoTypes.jl` `83a2ad8` +|"An executable companion to the Agda library" +|"It is not a proof." + +|`EpistemicTypes.jl` `3f52b6f` +|"Per-row claims with receipts for taxonomic tables" +|"not extracted from the proofs" + +|`ResidualEvidenceTypes.jl` `a92a9e2` +|"the executable side of the Agda development" +|"It is not a proof about either." +|=== + +=== Systems + +[cols="2,4,3",options="header"] +|=== +|Repository and commit |Its own description |Status that it states + +|`januskey` `989a747` +|"A Rust CLI for file operations that carry their own inversion metadata" +|`PWG-3` 4, `PWG-2ii` 1 + +|`squeakwell` `8ad9d12` +|"A database recovery and reconstruction tool" +|"No proof lives in this repository" + +|`absolute-zero` `ffcfed1` +|Programs that "provably compute nothing" and programs that "provably reveal +nothing" +|Agda `proven`. "Grade: `ungraded`" + +|`valence-shell` `48a88ea` +|"Research shell exploring formally specified reversible operations" +|Agda `PWG-3` "once CI is green on the merge head" + +|`verisimdb` `7039618` +|"a federated consonance engine" +|13 Coq axioms, 0 `Admitted`. No grade stated. + +|`vcl-ut` `5b10cb0` +|"the proof-bearing safety pipeline for VCL" +|"No Grade 3 claim is assigned by this plan" + +|`protocol-squisher` `3d50aa0` +|"Terminated as an active project (2026-07-06)" +|Two results are machine-checked, by its own provenance note. + +|`proven` `a7503b2` +|"Mathematically proven safe operations." +|Draft affirmation: "It is not fully proven today." + +|`proven-tests-and-benches` `f90bacb` +|"the testing framework for the hyperpolymath ecosystem" +|"29 spec-suite properties are now Actually-Proven" + +|`kategoria` `948d020` +|"an exploration, not a product" +|Its status files disagree. +|=== + +=== Languages + +[cols="2,4,3",options="header"] +|=== +|Repository and commit |Its own description |Status that it states + +|`affinescript` `a4d02e1` +|"a small, affine-typed core language that compiles to WebAssembly" +|"22 obligations: 7 `proven`, 13 `open`, 2 `argued`" + +|`my-lang` `0ba3b9f` +|"a multi-dialect surface for the hyperpolymath language stack" +|Its README calls the Coq core "axiom-free". + +|`ephapax` `6a422f6` +|A research language for "irreversible boundaries" in WebAssembly +|"446 of 446 named results closed" + +|`jtv-lang` `499038a` +|"A Harvard-architecture programming language" +|"PWG-3 24 · ungraded 10" + +|`eclexia` `48ea0e4` +|"an Economics-as-Code programming language" +|Five axioms, in a file that CI does not build. + +|`wokelang` `1624f41` +|"A human-centered, consent-driven programming language." +|The proofs cover a subset of the surface language. + +|`phronesis` `b06a951` +|A language "designed to formalize ethical reasoning in autonomous systems" +|Proof corpus "Authored, not independently reviewed." + +|`gnpl` `bbed3a0` +|"Lithoglyph's narration/projection language" +|16 Lean `axiom` declarations in inherited code. + +|`typell` `5a6592a` +|"The type-theoretic verification engine" +|"5 / 5 required PASS" + +|`tangle` `6f070d6` +|"A research language for knots and their mathematics" +|No `sorry` and no `axiom`. "`braidEquiv` is TRUSTED, NOT PROVEN" +|=== + +=== Statistics, knots and other + +[cols="2,4,3",options="header"] +|=== +|Repository and commit |Its own description |Status that it states + +|`CompositionalDA.jl` `9903e76` +|"Native-Julia compositional differential abundance for microbiome count +tables." +|Nine Agda modules, "no postulates". "No second Rocq/Lean witness" + +|`ExactCounts.jl` `08c5c64` +|"Exact counts and proportions for count tables" +|Each theorem is "about the Agda model". + +|`ExactTests.jl` `cf0a5e8` +|No README. Its proofs are about Fisher's exact test. +|No status document. + +|`CompositionalCounts.jl` `0c86831` +|"Multinomial (MN) and Dirichlet-Multinomial (DM) regression" +|Its documents disagree about its proofs. + +|`statistikles` `f2de559` +|"a Kautz Type 3 neurosymbolic statistical analysis assistant" +|Ten lemmas over the naturals are proven. Ten statistical targets are +"pending". + +|`KnotTheory.jl` `b84ce1c` +|"A comprehensive Julia toolkit for computational knot theory" +|No proof file. + +|`quandledb` `68c1485` +|"stores and investigates knots using presentations, invariants and semantic +indexes" +|One Agda file. Most rows are "NOT STARTED". + +|`snifs` `720eb82` +|"Safer (sandboxed) NIFs" +|"10/10 gated proof artifacts". The gap from model to code is "NOT proven". + +|`plasma-parser-writer` `17b2096` +|"a deterministic, typed policy engine for the agentic era" +|No proof file. + +|`ensaid-spec` `57412d7` +|"an open specification for neurosymbolic development environments" +|Each section is "Draft". +|=== + +=== Read first-hand, or not surveyed + +* Read first-hand by the author: `manifesto` `5f0b20e`, the research note in + `vcl-ut` `5b10cb0`, `resource-algebra` `aac649c` (`Core.agda`, + `Morphism.agda`, the `MinMax` instance), and `metadatastician/standards` + `be39f90`. +* `gv-clade-index` `539dd61` was searched for the word "mathesis". It has no + entry. +* Cloned and not surveyed, because the reader stopped at a usage limit: + `echidna` `f546ee9`, `echidnabot` `bbbc433`, `hypatia` `b2fc9d4`, + `proof-burrower` `5063985`, `arghda-core` `e793355`, `ijson-jcs` + `cccb538` and `metadatastician/kyq` `ca6f427`. From 430889d62bd1f744b3036a894281232d4a972afb Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 16:22:12 +0000 Subject: [PATCH 3/3] docs(proposals): record owner rulings and the X-PF1 outcomes The owner ruled through the selector on 2026-11-10: identity (three shelves, one spine), private names (counts only, history kept), template material (declare capabilities, remove vestigial modules), paths (consolidate under docs/atlas), open pull requests (session triages, owner approves), bridge centre (lock with slices), and the token theory (chain with the kernel import, provisional on X-PF1). Say why the history is not rewritten. Say what experiment X-PF1 can change: a seven-value candidate, its strict morphism onto the chain, three outcomes, and what stays true in each one. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- docs/proposals/mathesis-re-anchoring.adoc | 70 ++++++-- .../mathesis-research-programme.adoc | 167 ++++++++++++++++-- 2 files changed, 205 insertions(+), 32 deletions(-) diff --git a/docs/proposals/mathesis-re-anchoring.adoc b/docs/proposals/mathesis-re-anchoring.adoc index 10ca0f1..5aac968 100644 --- a/docs/proposals/mathesis-re-anchoring.adoc +++ b/docs/proposals/mathesis-re-anchoring.adoc @@ -6,10 +6,11 @@ :sectnums: :icons: font -Status: *proposed, not ratified* (2026-11-10). This document changes no gate, -schema, deed clause or data file. Each change in it needs the owner's ruling, -and each ruling goes through the selector. The work orders in <> -are written for a later implementation session. +Status: *proposed* (2026-11-10). The owner ruled on six of its eight +decisions on 2026-11-10, through the selector (<>). This document +changes no gate, schema, deed clause or data file. Each change that a ruling +does not cover still needs one. The work orders in <> are +written for a later implementation session. The companion document is link:mathesis-research-programme.adoc[the research programme]. This document @@ -852,7 +853,7 @@ table to the owner. Rebase the kept changes in this order: scanner fixes, one refresh tool, the frame fix. Close a pull request only on the owner's word. + *Check:* each open pull request merges cleanly, one at a time. + -*Needs ruling:* yes (D-6). +*Ruling:* D-6 (a), 2026-11-10. The owner approves each row before the session acts. [[wo-0-2]]WO 0.2 Name one writer for census data:: *Goal:* two sessions cannot refresh rows at the same time. + @@ -930,7 +931,7 @@ tests, recipes, the workflow step and the README. Leave a pointer file at each old path that another repository cites. Run `just repo-map`. + *Check:* each generated view is byte-identical to the view before the move, apart from its own path strings. + -*Needs ruling:* yes (D-4). +*Ruling:* D-4 (a), 2026-11-10. [[wo-2-4]]WO 2.4 Generate the bridge view:: *Steps:* For each hand-written row in the reconciliation register, find the @@ -955,7 +956,7 @@ set `(manifest :project)` to `mathesis`, and correct `(meta)`, `(anchor)`, and `just coapt`. + *Check:* the canon deed validator, `just validate-state`, `just validate-claude-md` and `just validate-coapt` pass. + -*Needs ruling:* yes (D-1). +*Ruling:* D-1 (a), 2026-11-10. The owner still reviews the clause text before it lands. [[wo-3-2]]WO 3.2 Declare the capabilities and remove vestigial modules:: *Steps:* Declare `agda`, `formal-proofs`, `bash`, `docs-site`, @@ -966,7 +967,7 @@ template for the `validate-rsr` conflict of <>. Record each local divergence in `(variant (paths :diverged))` until the template fix lands. + *Check:* `check-rsr-profile.sh` passes for the gated modules, and `just validate-rsr` passes. + -*Needs ruling:* yes (D-3). +*Ruling:* D-3 (a), 2026-11-10. [[wo-3-3]]WO 3.3 State the Mathesis contracts:: *Steps:* Add Mathesis clauses to the contractiles. Remove a template clause @@ -997,8 +998,16 @@ D-10 ruling there. Write the true obligations into `PROOF-NEEDS.adoc`. Fill result that this session did not observe. [[wo-3-5]]WO 3.5 Stop the publication of private names:: -*Steps:* Apply the owner's ruling. + -*Needs ruling:* yes (D-2). +*Ruling:* D-2 (a), 2026-11-10. Counts only. The history stays as it is. + +*Steps:* Keep only public repositories in the frame file. Record the count +of private repositories as one number, with the date of the listing. Remove +the private names from the unreachable list. Print the count in the "Not +reached" section of the catalogue. Remove the private name from +`README.adoc`. Extend the visibility check of the atlas to the frame file. + +*Check:* a frame record or a row whose visibility is not `public` fails the +gate. No tracked file at `HEAD` holds a name from the old private list. + +*Note:* do not rewrite the history (<>). If one name is +sensitive, the owner renames that private repository. [[wo-3-6]]WO 3.6 Affirm:: *Steps:* When stages 0 to 3 are done, fill `docs/AFFIRMATION.adoc` at one @@ -1043,7 +1052,7 @@ receipt lands. [[wo-5-2]]WO 5.2 Pilot the bridge lock:: Build the mechanism of <> for one relation that crosses repositories. -*Needs ruling:* yes (D-7). +*Ruling:* D-7 (a), 2026-11-10. [[wo-5-3]]WO 5.3 Schedule the census:: Run the census in one scheduled workflow that opens one pull request. This @@ -1060,33 +1069,64 @@ Each decision lists its arms with the most elegant and correct long-term arm first. The recommended arm is marked where it differs. The plan above assumes arm (a) in each case. +The owner ruled on six decisions through the selector on 2026-11-10. D-5 and +D-8 are open. + . *D-1 Identity.* (a) The three shelves with the evidence spine, as in <>. (b) An index only, with the theory and the applied area moved to other repositories. (c) An evidence system only, with the applied area - moved out. + moved out. *Ruled 2026-11-10: (a).* . *D-2 Private repository names.* (a) Publish counts only, remove the names from the tracked files, and keep the history as it is. (b) The same, and also rewrite the history, which breaks each clone and mirror. (c) Rule that - the names are public, and amend the invariant. + the names are public, and amend the invariant. *Ruled 2026-11-10: (a).* + <> gives the reason against a rewrite. . *D-3 Template material.* (a) Declare capabilities, remove the vestigial modules by the canon route, and fix the gate conflict in the template. (b) Keep each file, and record the ownership boundary only. (c) Remove all unused template material at once, which breaks template conformance. + *Ruled 2026-11-10: (a).* . *D-4 Paths.* (a) Consolidate the pipeline under `docs/atlas/`. (b) Keep the - paths and change the content only. + paths and change the content only. *Ruled 2026-11-10: (a).* . *D-5 Overlapping proposals.* (a) Amend ADR 0004 to use the canon reader, and ratify it. Mark `proof-receipts-as-data.adoc` as settled in part by PROOF-POLICY §8.5.1, and keep its experiments E1 to E6. Close issue 28 with - a pointer. (b) Keep the three open. + a pointer. (b) Keep the three open. *Open.* . *D-6 Open pull requests.* (a) The implementation session completes the triage table and the owner approves each row. (b) The owner triages alone. (c) Merge all 17 in order and resolve each conflict. + *Ruled 2026-11-10: (a).* . *D-7 Bridge centre.* (a) The lock with slices, as in <>. (b) No centre: each relation lives in one named home, and Mathesis derives the view. (c) Defer until the registry covers ten repositories. + *Ruled 2026-11-10: (a).* . *D-8 Proof toolchains.* (a) Pin Agda, Rocq and Lean in the Guix manifest. (b) Install from release archives with `deviation` records now, and move to Guix later. Recommended: (b), because it closes the hole this week. + *Open.* + +The companion programme records two more rulings of the same day: the token +theory starts with the chain of PROOF-POLICY §5 and imports the +`resource-algebra` kernel. The order is provisional until experiment X-PF1 +has a result. + +[[no-rewrite]] +=== Why the history is not rewritten + +A rewrite of the history would add little and cost much. + +* It cannot remove the names from public view. They have been public since + 2026-10-26. They are in each mirror, in each clone and in the pull request + refs, which a force-push does not remove. +* The public standards repository names at least one of the same private + repositories. +* It changes each commit identifier. Other repositories cite Mathesis by + commit, and the THY-1 record in `PROOF-STATUS.adoc` cites two source + commits. Those citations would point at nothing. +* It breaks each clone, each mirror and each open pull request. + +If one name is sensitive, the effective remedy is to rename that private +repository. The published name then points at nothing. == What this plan does not do diff --git a/docs/proposals/mathesis-research-programme.adoc b/docs/proposals/mathesis-research-programme.adoc index 2ea9285..2a076f8 100644 --- a/docs/proposals/mathesis-research-programme.adoc +++ b/docs/proposals/mathesis-research-programme.adoc @@ -6,9 +6,10 @@ :sectnums: :icons: font -Status: *proposed, not ratified* (2026-11-10). This document claims no proved -result. A statement marked *pre-registered* is a statement to prove or to -refute. A sentence marked *reading* is the view of the author of this +Status: *proposed* (2026-11-10). The owner ruled on two of its five decisions +on 2026-11-10 (<>). The rest is not ratified. This +document claims no proved result. A statement marked *pre-registered* is a +statement to prove or to refute. A sentence marked *reading* is the view of the author of this programme. Each fact about another repository names that repository and its commit in <>. Each such fact is that repository's own claim. This session checked no proof. @@ -335,8 +336,12 @@ the type family already has? The statements use this order, weakest first: `open`, `argued`, `tested-only`, `proven-with-postulates`, `proven`. PROOF-POLICY §5 lists the -tokens in the reverse of this order. The owner rules on the order before any -proof starts. +tokens in the reverse of this order. + +The owner ruled on 2026-11-10 that the theory starts with this chain and +imports the kernel. The ruling is provisional on one point: the order follows +the result of experiment X-PF1. <> says what the experiment can +change. S-1 (the tokens are a bottleneck grade):: Take the join of the order as alternatives and the meet as sequence, with @@ -382,15 +387,135 @@ Agda compare it with the function by `refl`. This is the method that agreement of the reader is `tested-only`, by exhaustion. + *Falsifier.* One row where the reader and the function differ. +[[x-pf1]] +=== What experiment X-PF1 can change + +*What the experiment asks.* The ECHIDNA proof-route plan states it: "Is a +total order on tokens enough for the weakest-step rule?" The plan models the +meet in scratch Lean. It is not a committed proof. + +*Why a chain can fail.* Take a claim with two steps. A written argument +supports the first step. A bounded test supports the second step. The chain +ranks `argued` below `tested-only`, so the claim is `argued`. The label is +correct as a rank: the weakest step has the rank `argued`. The label is wrong +as a description: no argument covers the second step, so the claim as a +whole is not argued. + +The same loss exists for alternatives. One argued attempt and one tested +attempt fold to `tested-only`, and the report forgets the argument. + +*A candidate that keeps the difference.* Add two values between `open` and +`proven-with-postulates`. The value `mixed` is the meet of `argued` and +`tested-only`: each step has support, and the steps differ in kind. The value +`argued and tested` is their join: the whole claim has an argument and a +test. + +[source,text] +---- + proven + | + proven-with-postulates + | + argued and tested + / \ + argued tested-only + \ / + mixed + | + open +---- + +These seven values are the free distributive lattice on the two kinds of +weak evidence, with `open` below and the two proof tokens above. They are a +`ResourceAlgebra` in the same way as the chain: the join is the alternatives +and the meet is the sequence. + +*The link to the chain.* The map below sends the seven values to the five +tokens. It keeps `𝟘`, `𝟙`, the join and the meet, so it is a strict +morphism. Each result in the chain is the image of a result in the larger +algebra. + +[cols="1,1",options="header"] +|=== +|Value |Token +|`proven` |`proven` +|`proven-with-postulates` |`proven-with-postulates` +|`argued and tested` |`tested-only` +|`tested-only` |`tested-only` +|`argued` |`argued` +|`mixed` |`argued` +|`open` |`open` +|=== + +The chain forgets exactly two differences: `mixed` against `argued`, and +`argued and tested` against `tested-only`. In the terms of `echo-types`, +these are the two fibres of the map that have more than one member. + +*How the experiment decides.* List each rule, gate and report in the estate +that reads a token. For each one, ask whether its result changes between the +two members of one fibre. + +*Pass condition:* the list covers the proof-route ABI, the registry and +ledger rule 3. Each entry has an answer and a source. + +*Three outcomes.* + +[cols="2,3,4,3",options="header"] +|=== +|Outcome |Finding |Change in Mathesis |Change in other places + +|A. The chain is enough. +|Each use of a token is a threshold on rank. No use tells the members of a +fibre apart. +|None. S-1 stands. The theory records the experiment as the reason for the +chain. +|None. + +|B. The chain is enough for gates. It is not enough for reports. +|Gates read the rank only. A person who reads a report needs the kind. +|The carrier of the theory becomes the seven values. S-1 gains one statement: +the map above is a strict morphism onto the chain. The registry shows the +token and the kind, for example `argued (mixed)`. +|The five tokens stay the closed vocabulary of PROOF-POLICY §5. The kind is a +field on the record. It is not a new token. + +|C. The chain is wrong. +|One rule accepts tested evidence and refuses argued evidence. A second rule +does the reverse. No chain serves both rules. +|As in B. Each statement that uses the order is also checked against the +partial order. +|The order in the canon is the owner's ruling in the standards repository. +The Idris2 `Token` module of the proof-route ABI changes with it. +|=== + +A fourth result is possible: the order of two tokens is the wrong way +round. Then two rows of the table in S-1 change places, and the proofs keep +their shape. + +*What stays in each case.* + +* S-2 does not change. It holds for each ordered resource algebra, so it + holds for the seven values with no new proof. This is the reason to prove + it once, against the kernel. +* The embedding of the five tokens in `MinMax` stays true. In outcomes B and + C it describes the image of the larger algebra. +* The Rocq and Lean legs of a changed statement are proved again. The old + receipts get the state `superseded`, as PROOF-POLICY §8.4 rule 5 requires. + No grade is carried forward. +* The table of S-3 is generated again with the new values. + +*One more level exists.* The seven values keep the kind of the weak evidence. +They do not keep which step was weak, or which axiom a proof uses. The trust +expression of Q-1.2 keeps those. *Reading:* the three structures are a +tower. The chain is an image of the seven values, and the seven values are +an image of the trust expression. X-PF1 chooses the lowest level that the +rules of the estate need. + === Research questions Q-1.1 Is a chain enough?:: -Experiment X-PF1 of the ECHIDNA plan asks whether a total order on tokens is -enough for the weakest-step rule. A chain puts `tested-only` above `argued`. -Then a claim that rests on one tested step and one argued step is `argued`, -and the report forgets the tested step. *Reading:* the chain is a lossy view -of a richer value, and the loss can be measured with the fibre of -`echo-types`. The question is which decisions need the richer value. +This is experiment X-PF1. <> gives the candidate, the test and the +outcomes. *Reading:* the chain is a lossy view of a richer value, and the +fibre of `echo-types` measures the loss. Q-1.2 What does a recheck leg buy?:: *Reading:* a theorem with three legs rests on a disjunction. The claim holds @@ -413,6 +538,9 @@ refutes. The first map is the one in row 2: token to HYP-01 level. === First experiments +. *E-1.0* Run experiment X-PF1 as <> describes it. + + *Pass condition:* one outcome of A, B or C is recorded, with the list of + uses that decided it. The owner then confirms or changes the order. . *E-1.1* Prove S-1 in Agda against `resource-algebra` at a pinned commit. Re-prove it in Rocq and Lean. + *Pass condition:* the receipt of Mathesis derives `PWG-2ii` for S-1 through @@ -739,12 +867,12 @@ number that the estate does not have today. The number decides whether The lines depend on each other in one direction only. -. Line 0 and E-1.1 start first. They need only this repository and the - kernel. +. Line 0, E-1.0 and E-1.1 start first. They need only this repository and + the kernel. . E-1.3 follows stage 2 of the re-anchoring plan, which moves the registry to the canon reader. -. Line 2 starts when the bridge record has a ruling (decision D-7 of the - plan). +. Line 2 can start. The owner ruled on the bridge centre on 2026-11-10 + (decision D-7 of the plan). . Line 3 needs one home repository that agrees to be the slice. . Line 4 can run at any time. It shares only S-2 with the other lines. . The horizon waits for lines 1 and 2 to produce records. @@ -820,17 +948,22 @@ a line is not worth its cost. * It does not move any theorem out of its home repository. * It does not treat a proposal of a model as evidence. +[[programme-decisions]] == Decisions for the owner Each decision lists the most elegant and correct long-term arm first. The -programme assumes arm (a). +programme assumes arm (a). The owner ruled on R-1 and R-2 through the +selector on 2026-11-10. R-3, R-4 and R-5 are open. . *R-1 The order of the tokens.* (a) The chain of S-1, as PROOF-POLICY §5 lists it. (b) A partial order in which `tested-only` and `argued` are not - comparable. Arm (b) needs a new bottom value for a mixed claim. + comparable. Arm (b) needs new values for a mixed claim (<>). + *Ruled 2026-11-10: (a), provisional. The order is updated when experiment + X-PF1 has a result.* . *R-2 The kernel import.* (a) The token theory imports `resource-algebra` at a pinned commit, as `januskey` and `choreographic-types` do. (b) The token theory is self-contained, and a bridge record joins it to the kernel. + *Ruled 2026-11-10: (a).* . *R-3 The home of S-2.* (a) Mathesis, because the expression language is the ledger's. (b) `resource-algebra`, as a kernel lemma. . *R-4 The first slice for line 3.* The owner names the repository.