Skip to content

feat: first estate proof census and maths catalogue #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 2 commits into from
Oct 26, 2026
Merged

feat: first estate proof census and maths catalogue #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f63c51f
feat: first estate proof census and maths catalogue
claude Oct 26, 2026
55aa899
fix: move the catalogue under docs/ and commit rows, not raw paths
claude Oct 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions Justfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -713,3 +713,17 @@ uncloak:
else
echo "Use 'ls -a' to view dotfiles on this OS."
fi

# ── mathesis: estate maths catalogue ──────────────────────────────────────

# Re-run the proof census over docs/catalogue/census/repos.jsonl and regenerate the catalogue
census:
bash scripts/census/run-census.sh

# Re-render docs/catalogue/catalogue.adoc from the committed census rows
catalogue:
bash scripts/census/render-catalogue.sh docs/catalogue/census > docs/catalogue/catalogue.adoc

# Fail if the committed catalogue does not match the committed census rows
catalogue-check:
bash scripts/census/render-catalogue.sh docs/catalogue/census | diff -u docs/catalogue/catalogue.adoc -
229 changes: 71 additions & 158 deletions README.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,172 +1,85 @@
// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath)
= {{PROJECT_NAME}}
= mathesis
:toc:
:toc-placement: preamble

// ── Licensing ───────────────────────────────────────────────────────────────
image:https://img.shields.io/badge/Code-MPL--2.0-blue.svg?logo=mozilla[Code licence: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"]
image:https://img.shields.io/badge/Docs-CC--BY--SA--4.0-blue.svg?logo=creativecommons[Docs licence: CC-BY-SA-4.0,link="https://creativecommons.org/licenses/by-sa/4.0/"]
image:https://img.shields.io/badge/Provenance-Quantum--Safe-blueviolet[Quantum-Safe Provenance,link="docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt"]
The estate's maths section. It answers "where does that proof live?" for
every hyperpolymath repository: which repos carry proofs, in which prover,
whether the work reads as theory or engineering, which have holes or
axioms, and where each repo's proof-status file is.

// ── Standard & quality gates ────────────────────────────────────────────────
image:https://img.shields.io/badge/RSR-Rhodium_Standard-9C27B0[Rhodium Standard Repository,link="https://github.com/hyperpolymath/rhodium-standard-repositories"]
image:https://img.shields.io/endpoint?url=https://raw.githubusercontent.com/{{OWNER}}/{{REPO}}/governance-badges/badges/k9.json[K9 conformance,link="https://github.com/{{OWNER}}/{{REPO}}/actions/workflows/dogfood-gate.yml"]
image:https://www.bestpractices.dev/projects/{{OPENSSF_BP_ID}}/badge[OpenSSF Best Practices,link="https://www.bestpractices.dev/projects/{{OPENSSF_BP_ID}}"]
image:https://api.scorecard.dev/projects/github.com/{{OWNER}}/{{REPO}}/badge[OpenSSF Scorecard,link="https://scorecard.dev/viewer/?uri=github.com/{{OWNER}}/{{REPO}}"]
image:https://sonarcloud.io/api/project_badges/measure?project={{OWNER}}_{{REPO}}&metric=alert_status[SonarQube Quality Gate,link="https://sonarcloud.io/summary/new_code?id={{OWNER}}_{{REPO}}"]
image:https://archive.softwareheritage.org/badge/origin/https://{{FORGE}}/{{OWNER}}/{{REPO}}/[Archived in Software Heritage,link="https://archive.softwareheritage.org/browse/origin/?origin_url=https://{{FORGE}}/{{OWNER}}/{{REPO}}"]
Proofs stay in their home repositories. mathesis points at them. Later it
will also hold the Agda sources for theory that has no other natural home.

// ── Provenance & ecosystem ──────────────────────────────────────────────────
image:https://img.shields.io/badge/Idris-Inside-5E5086?logo=idris&logoColor=white[Idris Inside,link="https://github.com/hyperpolymath/proven"]
image:https://img.shields.io/badge/Zig-Zero--overhead-F7A41D?logo=zig&logoColor=black[Zig Zero-overhead FFI,link="https://github.com/hyperpolymath/typed-wasm"]
image:https://api.thegreenwebfoundation.org/greencheckimage/{{FORGE}}[Green Web,link="https://www.thegreenwebfoundation.org/green-web-check/?url={{FORGE}}"]
The rules for where a proof *should* live are not here: they are
`standards/3-practice/PROOF-POLICY.adoc` (Creusot for Rust, SPARK for Ada,
Idris2 for APIs, ABIs and engineering properties, Agda for theory rechecked
in Rocq and Lean). The working method is the proof-craft skill.

{{PROJECT_DESCRIPTION}}

[IMPORTANT]
====
*This file is a template.* You are reading `README.adoc` from the *RSR template repo*
(or a freshly-cloned copy of it). Run `just repo-init` to replace every `{{PLACEHOLDER}}`
token with your project's details, then delete this admonition. Until you do, the
`{{...}}` markers below are intentional placeholders, not content.
====

== What this is

A new repository scaffolded from the *Rhodium Standard Repository (RSR)* template:
a batteries-included starting point that ships with CI/CD, machine-readable project
metadata, an AI-agent gatekeeper protocol, a formally-typed ABI/FFI seam
(Idris2 + Zig), container and reproducible-build scaffolding, and governance
infrastructure — all wired and passing the RSR validators on day one.

Replace this section with a description of *your* project once initialised.

== Quick start

[source,bash]
----
# 1. Create a repo from this template (or clone it), then from the repo root:
just repo-init # interactive bootstrap: fills every {{PLACEHOLDER}}

# 2. See the available tasks:
just # lists all phases (build, test, validate, audit, ...)

# 3. Check the repo still satisfies the RSR shape:
just validate # structure + metadata checks
----

`just repo-init` prompts for the project name, owner, author, licence contact, and the
other values listed in `.machine_readable/ai/PLACEHOLDERS.adoc`, substitutes them
across the tree, validates the result, and (if available) runs the `k9-svc` checks.

[[ai-install]]
== AI-Assisted Installation (Recommended)

=== Just say it

Say this to any AI assistant that can read a URL and run commands (or give you
commands to paste):

[source,text]
----
Create a new repository from https://github.com/hyperpolymath/rsr-template-repo
----

The URL is the key: it leads the assistant to
link:docs/AI_INSTALLATION_GUIDE.adoc[`docs/AI_INSTALLATION_GUIDE.adoc`], the
complete step-by-step recipe. The assistant checks your system, installs the
prerequisites, instantiates the template with `just repo-init`, and verifies the
result with `just doctor`.

* "Set up rsr-template-repo so I can work on the template itself — https://github.com/hyperpolymath/rsr-template-repo"
* `./launcher.sh --ai-setup` (or `just ai-setup`) prints the line and the guide path.

=== What you will be asked

. Your operating system (Linux, macOS, or Windows via WSL2).
. The new project's name, owner, author and licence contact (the values listed in
`.machine_readable/ai/PLACEHOLDERS.adoc`).
. To confirm the privacy notice below.

=== Privacy and security

[IMPORTANT]
====
Setting up rsr-template-repo clones this repository and installs its developer
tools per-user with mise (no administrator rights, nothing sent anywhere).
`just repo-init` rewrites files only inside the new checkout; it creates no
remote repository and pushes nothing until you do.
====

=== Minting without a terminal

Agents and CI can mint non-interactively: set `RSR_NON_INTERACTIVE=1` and pass
the answers as environment variables named like the prompts' variables in
`build/just/repo-init.just` (`PROJECT_NAME`, `REPO`, `OWNER`, `AUTHOR` and
`AUTHOR_EMAIL` are required; any other answer left unset is blank or takes its
default). Piping the answers to stdin in prompt order also works.

=== Troubleshooting

Run `just doctor`; each FAIL carries a code explained in
link:docs/SETUP.adoc#troubleshooting[`docs/SETUP.adoc` §Troubleshooting], and
`just heal` applies the automatic fixes. Prefer to do it yourself? The full
manual route is link:docs/SETUP.adoc[`docs/SETUP.adoc`]; developers and
maintainers can brief an AI with `just ai-warmup dev` / `just ai-warmup maintainer`.

== What you get

* *Machine-readable metadata* (`.machine_readable/descriptiles/`) — `STATE`, `META`,
`ECOSYSTEM`, `PLAYBOOK`, `AGENTIC`, `NEUROSYM`, `CLADE`, and `anchors/ANCHOR`,
in deed, so tools and agents can read the project's state and boundaries.
* *AI gatekeeper protocol* — `rsr-template-repo_chora.deed` (the repo deed) is the
universal entry point that tells an AI agent how to work in this repo before it
touches anything; it carries the AI allocation policy and the ply directory tree.
* *Typed ABI/FFI seam* — `src/interface/Abi/` (Idris2 type + layout proofs) over
`src/interface/ffi/` (Zig implementation), with generated C headers.
* *CI/CD* — GitHub Actions for quality, security (CodeQL, Scorecard, secret
scanning), multi-forge mirroring, and RSR anti-pattern enforcement.
* *Supply-chain & reproducibility* — container layering (stapeln), Guix shells,
SBOM, and signing hooks.
* *Governance* — `GOVERNANCE.adoc`, `MAINTAINERS.adoc`, `.github/` community health
files, and a release `AUDIT.adoc` gate.

== Repository map

The authoritative map is generated, so it cannot drift from the tree:
link:docs/architecture/REPOSITORY-MAP.adoc[docs/architecture/REPOSITORY-MAP.adoc]
(regenerate with `just repo-map`; CI fails if it is stale).

The short version:
== What is here

[cols="1,3"]
|===
| Path | What lives there

| `README.adoc`, `CLAUDE.md` | Start here - humans and AI agents respectively.
| `src/`, `tests/` | The code and its tests.
| `docs/` | Human documentation, including the full map above.
| `.machine_readable/` | Manifests, contractiles and policies that tools read.
| `build/`, `Justfile` | Every task runs through `just`; phases live in `build/just/`.
| `ci/`, `.github/` | CI configuration; GitHub reads `.github/` and no other path.
|`docs/catalogue/catalogue.adoc` |The catalogue: one row per repository with proof files of its own, split into theory and engineering. Generated; do not edit by hand.
|`docs/catalogue/census/` |What the catalogue is rendered from: `catalogue-rows.jsonl` (one row of counts per repository, no file paths), `repos.jsonl` (the census input), `unreachable.jsonl` and `template-paths.txt`. Each JSONL file is I-JSON/JCS, one object per line.
|`scripts/census/` |`run-census.sh` (whole census), `census-repo.sh` (one repo), `summarise.sh`, `build-rows.sh` (raw census to rows), `render-catalogue.sh` (rows to catalogue), and proof-craft's `proof-holes.sh`.
|`Justfile` |`just census`, `just catalogue`, `just catalogue-check` (the committed catalogue matches the committed data).
|===

== Where to go next

* link:docs/architecture/REPOSITORY-MAP.adoc[The repository map] — generated; what every directory is for.
* link:docs/EXPLAINME.adoc[EXPLAINME] — the engineering deep-dive: how the pieces actually work.
* link:docs/AFFIRMATION.adoc[AFFIRMATION] — the dated, signed honesty snapshot of the repo's true state.
* link:docs/AUDIT.adoc[AUDIT] — the release audit gate.
* link:docs/AI_INSTALLATION_GUIDE.adoc[AI installation guide] — for agents instantiating this template.
* link:.machine_readable/ai/PLACEHOLDERS.adoc[PLACEHOLDERS] — the full placeholder reference.
== How the census works

. *List repositories.* `docs/catalogue/census/repos.jsonl` is the input. Agent sessions build
it with the Claude Code remote `list_repos` tool, because the GitHub API is
not reachable from them.
. *List proof files cheaply.* Each repository is cloned blobless with
`--no-checkout`, and its file names are filtered by prover extension:
Agda, Idris2, Lean, Rocq, Isabelle, TLA+, Dedukti/Lambdapi, SMT-LIB, TPTP,
SPARK, Why3, F*, Dafny and Alloy.
. *Read only the proof files.* Only those files are checked out. Top-level
declaration names go to `decls.jsonl`, and proof-craft's `proof-holes.sh`
inventories holes, axioms, disabled checkers and policy breaches
(`holes.jsonl`).
. *Set the template aside.* Files the RSR template ships
(`docs/catalogue/census/template-paths.txt`) are boilerplate wherever they appear. The
catalogue counts only a repo's *own* files.
. *Keep rows, not paths.* The raw, path-level census (clones, every proof file, every declaration, every hole finding, and a `summary.md`) goes to a scratch directory (`MATHESIS_WORK`) and is not committed. `build-rows.sh` folds it into one row of counts per repository, and only those rows are committed, so the data stays small and does not repeat other repositories' file paths.

== Reading the catalogue (first pass, 2026-10-26)

The first census covered 476 repositories:

* *Scope:* 462 repositories were cloned; 5 forks and 9 awesome-lists were
skipped. 275 have proof files, and 239 still have them once template
boilerplate is set aside.
* *Unreached:* 37 private repositories could not be cloned and are listed at
the end of the catalogue, among them `cut-calculus`.
* *Possibly missing:* the listing returned only repositories pushed since
2026-09-15, so older, untouched repos may be absent. Add them to
`docs/catalogue/census/repos.jsonl` and rerun.
* *Theory or engineering* is a heuristic: more Agda, Lean, Rocq or Isabelle
files than Idris2 or SPARK files reads as theory. Confirm each row against
PROOF-POLICY.
* *Hole, axiom, unsafe and policy counts* are textual candidates, not kernel
verdicts. The kernel is the authority. `import Mathlib` shows under
policy.
* *Declaration counts* overcount Agda and Idris2:
every column-0 type signature counts, helpers included.
* *Older template copies* survive as "own" files in some repos: for example
asdf-tool-plugins, whose plugins each carry a stubbed `Layout.idr`.
* *Fixtures:* files under `tests/`, `fixtures/`, `corpus/` or `benches/` are
counted as fixtures. `examples/` is not, because some verifiers (Atoma)
keep real verification conditions there.

== Next steps

* Confirm the theory/engineering split per row, and record each repo's
obligations with the status vocabulary of PROOF-POLICY §5.
* Theorem-level rows for the theory repos: statement, Agda source, Rocq
leg, Lean leg, route.
* A scheduled CI job that reruns the census and fails on catalogue drift.
* A deed (`mathesis_chora.deed`) once the repo is instantiated from the RSR
template.

== Licence

Code, configuration and scripts are link:LICENSE[Mozilla Public License 2.0]
(`MPL-2.0`); prose documentation is `CC-BY-SA-4.0`. Both texts live in
`LICENSES/`, and per-file `SPDX-License-Identifier` headers are authoritative.
The GitHub-detected licence is MPL-2.0 (the root `LICENSE`). Long-term
attribution uses Quantum-Safe Provenance — see
link:docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt[the Quantum-Safe Provenance exhibit].
Code (`scripts/`, `Justfile`): MPL-2.0. Documentation and the catalogue:
CC-BY-SA-4.0. See `LICENSES/`.
Loading
Loading