diff --git a/docs/proposals/mathesis-re-anchoring.adoc b/docs/proposals/mathesis-re-anchoring.adoc new file mode 100644 index 0000000..5aac968 --- /dev/null +++ b/docs/proposals/mathesis-re-anchoring.adoc @@ -0,0 +1,1278 @@ +// 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* (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 +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. + +*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. + +*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. + +*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 +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. + +*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`, +`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. + +*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 +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:: +*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 +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. +*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 +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. + +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. *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. *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. *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. *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 + +* 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. diff --git a/docs/proposals/mathesis-research-programme.adoc b/docs/proposals/mathesis-research-programme.adoc new file mode 100644 index 0000000..2a076f8 --- /dev/null +++ b/docs/proposals/mathesis-research-programme.adoc @@ -0,0 +1,1252 @@ +// 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* (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. + +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 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 +`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. + +[[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?:: +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 +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.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 + 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, 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 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. + +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. + +[[programme-decisions]] +== Decisions for the owner + +Each decision lists the most elegant and correct long-term arm first. The +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 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. +. *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`.