From 82283b1d96da44f1b47caed7315dc82b4d46ff04 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 11 Nov 2026 18:18:45 +0000 Subject: [PATCH] docs: affirm the state of Mathesis at c81cb84 (re-anchoring WO 3.6) Stages 0 to 3 of the re-anchoring plan are merged. This affirmation records what was true and checked at main c81cb84e4ff3d5ceedc09a7fb0a2fcdb0ef989f5, from runs in one session between 2026-11-11T18:16:17Z and 18:16:56Z on a clean tree, and from CI run 43072763288 at the same commit (read in the session, labelled as CI by owner ruling). Each claim names its command. Owner ruling 2026-11-11: this commit is signed with the session key, and the owner's merge of the pull request is the owner's attestation. Refuted at this commit and stated in the file: just ijson-check exits 1 on the two coaptation files (an open finding from before stage 3). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk Signed-off-by: Claude --- docs/AFFIRMATION.adoc | 362 +++++++++++++++++++++++------------------- 1 file changed, 200 insertions(+), 162 deletions(-) diff --git a/docs/AFFIRMATION.adoc b/docs/AFFIRMATION.adoc index 14866b0..f9ec6a0 100644 --- a/docs/AFFIRMATION.adoc +++ b/docs/AFFIRMATION.adoc @@ -1,192 +1,233 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= AFFIRMATION — Mathesis, as of += AFFIRMATION: Mathesis, as of 2026-11-11 :toc: macro :toclevels: 2 :std-docs: https://github.com/hyperpolymath/standards/blob/main/docs -_the No-Bullshit file: what we affirm was true and checkable at this moment._ +_What we affirm was true and checkable at one commit._ -[NOTE] -==== -*This file is a template.* Replace the `{{…}}` placeholders and the `<…>` anchor -fields, then re-run your project's own checks in the same session before -signing. It conforms to *profile A (evidential)* of the -link:{std-docs}/AFFIRMATION-STANDARD.adoc[AFFIRMATION authoring standard]. A -policy-surface repo should use profile B (MUST / INTEND / WISH) instead — see -that standard for the profile B skeleton. - -An *affirmation* is a solemn declaration of the truth of a statement, made by -someone who _declines to swear an oath_ — our truth-as-best-believed at a -stamped instant, binding on our honesty, not a claim of infallibility. It is the -third of the README / EXPLAINME / AFFIRMATION trio: - -[cols="1,3,2",options="header"] -|=== -| File | Answers | Tense -| `README.adoc` | _Where is this going, and why?_ — steering, intent, vision | future / aspirational -| `EXPLAINME.adoc` | _How is it built, and what's the evidence?_ — engineering | descriptive / mechanism -| *`AFFIRMATION.adoc`* (this file) | _What can we honestly affirm was *true and checkable* at a stamped moment?_ | a frozen instant, falsifiable -|=== - -This file is *optional*. Delete it rather than carry an affirmation you have not -re-verified — a stale affirmation is worse than none. -==== +This file follows profile A (evidential) of the +link:{std-docs}/AFFIRMATION-STANDARD.adoc[AFFIRMATION authoring standard]. It +is the third file of the README, EXPLAINME and AFFIRMATION trio: the README +says where Mathesis is going, `EXPLAINME.adoc` says how it is built and where +the evidence is, and this file says what was true and checked at one commit. +It closes stage 3 of the re-anchoring plan (WO 3.6). toc::[] == What this is, and how it works -*What it is.* A short, dated, signed snapshot of what hyperpolymath can honestly and -verifiably claim about *Mathesis* at one exact commit. Nothing here is -marketing and nothing is a promise about the future — those live in the README. -This file is the receipt. - -*What the project is.* Estate-wide mathematical knowledge atlas and proof census - -*How it stays trustworthy.* Three moving parts: +A short, dated, signed snapshot of what can honestly be claimed about +Mathesis at the commit in <>. Each claim below comes from +a check that ran in the session that wrote this file, or from a CI run that +the session read, labelled as such (owner ruling 2026-11-11). Nothing here +is copied from a status document or from memory. -. *Ground truth, not memory.* Every claim below must be produced by _running the - project's own checks_ in the session that writes this file (build, tests, - typecheck, `just audit`). Where a status doc, the `Justfile`, or memory says - otherwise, the live run wins and the contradiction is flagged here. -. *A frozen anchor.* The file names the exact commit SHA, branch, UTC timestamp, - working-tree delta and toolchain (see <>), so "true" always - means "true _at this point_". Move the SHA and this file is a draft until it - is re-run. -. *A real signature.* It is landed by a *signed git commit*; that signature over - this content at the anchored SHA is what makes the affirmation tamper-evident - and attributable — not the prose alone. +*What the project is.* The maths section of the estate: an atlas of the +mathematics in other repositories, the theory that no single system owns, +and methods that apply mathematics to decisions. Each statement carries its +evidence; Mathesis derives status from the receipts of the home +repositories and does not assert it. -*We are fallible.* This is our best honest belief, not a proof of its own -correctness. Treat it as a falsifiable claim, not gospel. +== The epistemic contract -== The epistemic contract (read this before you trust _or_ attack) +This file records our best belief at the timestamp below. It is not a +guarantee of correctness; the only guarantee is no intentional overclaim. An +honest claim that later turns out false is an error to fix, not a lie. -This document records hyperpolymath's *best belief* at the timestamp below. It is -*not a guarantee of correctness.* The only guarantee is *no intentional -overclaim*: where something is proven we say "proven"; where it is a documented -trust boundary, an experiment, or an unwired module, we say so; where a claim is -the README's aspiration rather than a checked result, we say so. An honest claim -that later turns out false is an *error to be fixed* — not a lie. +* You may conclude that each claim below was produced by the command that it + names, at the anchor commit. +* You may not conclude that anything is true at another commit, or that an + unlisted thing passes. Silence is not a claim. -What you may conclude from this file: - -* Every claim below was produced by *running the tool* in the session that wrote - this file — not from memory, not copied forward from a previous affirmation, - and not read off a status document. -* Where a live run and a status document disagreed, the live run won and the - status document is named as stale in <>. - -What you may *not* conclude: - -* That anything is true *now*. This file describes the commit in - <> and nothing else. -* That unlisted things pass. *Silence is not a claim.* - -*Standing invitation to refute.* You are invited to bulldoze any claim in this -file. Bring a counter-example, a failing run, or a contradicting source. +You are invited to refute any claim: bring a failing run or a contradicting +source. [#verifiable-anchor] == Verifiable anchor [cols="1,3",options="header"] |=== -| Field | Value +|Field |Value -| Project -| Mathesis +|Project +|Mathesis -| Repo -| `hyperpolymath/mathesis` +|Repo +|`hyperpolymath/mathesis` -| Branch -| `main` +|Branch +|`main` -| Commit (HEAD) -| `` +|Commit (HEAD) +|`c81cb84e4ff3d5ceedc09a7fb0a2fcdb0ef989f5` -| Permalink -| https://github.com/hyperpolymath/mathesis/tree/ +|Permalink +|https://github.com/hyperpolymath/mathesis/tree/c81cb84e4ff3d5ceedc09a7fb0a2fcdb0ef989f5 -| Verified (UTC) -| `` +|Verified (UTC) +|`2026-11-11T18:16:17Z` to `2026-11-11T18:16:56Z` (local checks); CI run +43072763288 completed `2026-11-11T18:16:39Z` -| Working-tree delta at verification -| `clean`, or every modified and untracked file present when the checks ran, - with an explicit statement of whether it affects the results below. +|Working-tree delta at verification +|`clean` before and after the checks (`git status --short` printed nothing) -| Toolchain -| `` +|Toolchain +|Local: just 1.56.0, Nickel 1.18.0, Bun 1.4.4, jq 1.7, Asciidoctor 2.0.26; +`metadatastician/standards` at `8e48b1c` (the CI pin, for the deed and k9 +validators) and at `e2a03dc` (main, for the registry reader and the +capability checker). CI, read from the job log: Agda 2.7.0.1, Rocq (The Coq +Proof Assistant) 8.18.0, Lean 4.29.0, in the Guix shell pinned by +`build/channels.scm`. -| Affirmed by -| Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> +|Affirmed by +|The engineering party: a Claude Code session +(https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk), which ran the +checks. The owner attests by merging the pull request that carries this +file (owner ruling 2026-11-11). |=== [IMPORTANT] ==== -*Never anchor to a tag.* Tags move, and a moved tag silently invalidates every -claim in this file. - -If you are reading this at a later commit, the claims may have drifted. Re-run -<> and write a fresh affirmation; do not trust a stale one. +Never anchor to a tag. If you read this at a later commit, re-run +<> and write a fresh affirmation. ==== -== Companion documents and repo metadata (cross-check) - -The files a sceptic should read against this one — *including any that -contradict it*. A contradiction named here is honest; one the reader finds for -themselves is not. +== Companion documents (cross-check) -* `README.adoc` — the aspirational claims this file is measured against. -* `EXPLAINME.adoc`: the mechanism. -* `docs/AUDIT.adoc` — the standing conformance audit. -* `*_chora.deed` (repo deed) — machine-readable repo metadata (AI allocation + ply tree). -* `` +* `README.adoc`: the claims this file is measured against. +* `EXPLAINME.adoc`: the mechanism, and the proof ledger. +* `mathesis_chora.deed`: the identity, boundaries and golden path. +* `docs/status/READINESS.adoc`: grade D, provisional until the owner + confirms it. This file does not affirm a grade. +* `docs/AUDIT.adoc`: the template's "Audit Gate" summary (2026-04-07, before + this repository existed). It is not an audit of this commit. == The honest state (one breath) -`` +At this commit the generated views match their data, the deed, the arrival +pack, the contracts and the coaptation receipt agree, the scaffold matches +the declared capabilities, no tracked file names a private repository, and +CI checks THY-1 in Agda, Rocq and Lean with planted controls. One theorem of +thirteen in the registry is graded; the rest are `ungraded` because their +homes have no receipt that the canon reader accepts. Stages 4 and 5 are not +started, and the coaptation band reads amber for that reason. === What is solid (and how we checked) [cols="2,1,3",options="header"] |=== -| Claim | Status | Evidence (command, and what it printed) -| _e.g. The library builds clean_ | affirmed | `just build` at the anchor SHA — exit 0 -| _e.g. The ABI seam typechecks_ | affirmed | `idris2 --typecheck src/interface/abi.ipkg` — 0 errors -| _e.g. Feature X is complete_ | aspiration | README §… — *not checked*, do not read as affirmed +|Claim |Status |Evidence (command, and what it printed) + +|The generated views match their data +|affirmed +|`MATHESIS_STANDARDS= just check-views`: exit 0; 28 `PASS` +lines, 0 `FAIL`; "generated atlas matches census"; atlas tests "13 pass, +0 fail"; registry tests "14 pass, 0 fail" + +|The registry derives each grade through the canon reader +|affirmed +|same run: "claims registry derived from 3 pinned source(s); views match (18 +claims, 2 bridges)"; `docs/atlas/generated/registry.adoc` reads "1 at +`PWG-1` ... 12 `ungraded`, of 13 theorems" + +|THY-1 checks in Agda, Rocq and Lean, and planted escapes fail the gate +|affirmed (CI run, read in this session) +|CI run 43072763288 at the anchor commit: conclusion `success`; steps "Agda +lane (gate, then planted controls)", "Rocq lane ...", "Lean lane ..." and +"Golden path (just check), then its controls" each `success` + +|The deed is valid +|affirmed +|`STANDARDS_DIR= bash .github/hooks/validate-deed.sh`: +"DEED: 3 file(s), 0 failing"; `just validate-state`: "valid (phase +incubating, maturity experimental)" + +|The contracts are valid k9 +|affirmed +|`STANDARDS_DIR= bash .github/hooks/validate-k9.sh`: "K9: +14 file(s), 0 failing" + +|The six Mathesis `must` probes hold +|affirmed +|each probe of `.machine_readable/contractiles/must/must.k9.ncl`, section +"Mathesis Invariants", run with `bash -c`: `views-current`, +`no-private-name`, `no-hand-typed-grade`, `receipts-stay-home`, +`home-theorem-has-receipt`, `rows-have-provenance` each passed + +|The arrival pack and the coaptation receipt match their sources +|affirmed +|`just validate-claude-md`: "OK: CLAUDE.md arrival pack is in sync with the +deed"; `just validate-coapt`: "OK: coaptation receipt is in sync" + +|The scaffold matches the declared capabilities +|affirmed +|`bash scripts/check-rsr-profile.sh ` from standards `e2a03dc`: "OK, +scaffold matches declared capabilities (13 baseline path(s) present)"; +`just validate-rsr`: "RSR compliance: PASS" + +|No tracked file names a private repository +|affirmed +|`git ls-files` searched for each name of the old private list as a quoted +JSON value: 0 files. The frame holds 465 public records; +`docs/atlas/census/private-count.json` records 40 private repositories + +|The documents render, and the root and the map are current +|affirmed +|`bash scripts/check-adoc-renders.sh`: "all 180 tracked .adoc file(s) render +clean"; `bash scripts/check-root-shape.sh .`: "root matches allowlist"; +`just validate-repo-map`: "up to date"; `tests/shape/*.sh`: exit 0; +`bash scripts/check-no-placeholders.sh .`: exit 0 |=== === The honest nuance you must not lose -Where a true claim above is easily over-read. This section is what separates an -affirmation from marketing. - -* `` +* "THY-1 is proven" is about a graph model. That the model matches Cargo's + feature resolution is argued, not proved. +* The proof result is a CI run that this session read, not a local run: this + container had no Guix and no provers. +* The six `must` probes passed when run by hand. No runner executes `must` + probes yet, so the contract is not a gate on its own. `just check` in CI + enforces three of the six rules: `views-current` (the catalogue and atlas + checks), the public frame of `no-private-name` (`census-atlas.mjs check`), + and `rows-have-provenance` (the atlas row validation). It does not enforce + `receipts-stay-home`, `home-theorem-has-receipt` (a missing receipt yields + `ungraded`, not a failure) or `no-hand-typed-grade`. +* Census counts are textual candidates, not kernel verdicts. === Known-incomplete but honestly fenced -Gaps that fail *loudly* rather than silently. Name the guard that makes the -failure loud — a gap with no guard belongs in <> instead. - -* `` — fenced by `` +* Theorems without an accepted receipt: fenced by the registry, which shows + each as `ungraded` with the reader's reason, never as a grade. +* Private repositories: fenced by `census-atlas.mjs check` and both census + writers, which refuse an entry outside the public frame. +* A stale view or a failing proof: fenced by `just check` in CI, whose + controls (`tests/golden/check_controls_test.sh`) show that each fails it. [#outstanding] === Outstanding / weak / refuted (no spin) -Known gaps, trust boundaries, postulates, unwired modules and stale docs. -*Silence is not affirmation* — name what you have not verified, and name -anything this session *refuted*. - -[IMPORTANT] -==== -Never delete a refuted claim. Deleting it is exactly the spin this genre exists -to prevent — mark it refuted and say what refuted it. -==== +* *Refuted at this commit:* `just ijson-check` exits 1: ".machine_readable/ + coaptation/clauses.json" and "facts.json" are "NOT CANONICAL" (21 files + checked, 19 canonical). This is an open finding from before stage 3. +* The coaptation receipt reads `band = "amber"`: three committed stages + (3, 4, 5) were open when it was generated. +* Two home repositories' receipts are refused by the canon reader, so their + pins derive no grade. +* One public repository in the frame could not be cloned in the last census. +* `just crg-grade` prints `X` whatever `READINESS.adoc` says: the template + recipe reads a root `READINESS.md` that does not exist. +* *Overstated at this commit:* the "Known gaps" of `EXPLAINME.adoc` and the + abstract of the `must` contract say that CI enforces the same rules as the + `must` probes. It enforces three of the six (see the nuance above). The + contract text needs an owner-reviewed correction. +* The template example proofs still sit in the proof gate until WO 4.1. +* The git history still holds the private names (ruling D-2 (a)). +* `docs/AUDIT.adoc` is the template's audit-gate summary, not an audit of + Mathesis. +* Not checked here: the signatures of earlier commits, and any CI workflow + other than the proof gate. [#reproduce] == Reproduce it yourself @@ -195,41 +236,38 @@ to prevent — mark it refuted and say what refuted it. ---- git clone https://github.com/hyperpolymath/mathesis cd mathesis -git checkout -# +git checkout c81cb84e4ff3d5ceedc09a7fb0a2fcdb0ef989f5 +export MATHESIS_STANDARDS=/path/to/standards # the reader pin +just check-views # exit 0, 0 FAIL lines +just validate-state validate-claude-md validate-coapt validate-rsr validate-repo-map +STANDARDS_DIR=/path/to/standards bash .github/hooks/validate-deed.sh # 3 files, 0 failing +STANDARDS_DIR=/path/to/standards bash .github/hooks/validate-k9.sh # 14 files, 0 failing +guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- just check-proofs +just ijson-check # exit 1: the two coaptation files (see above) ---- == One-line characterisation (quote this) -> `` +> At `c81cb84`, Mathesis tells the truth about itself: its views match its +> data, its deed and contracts describe Mathesis, it names no private +> repository, and it grades one theorem of thirteen because only one has a +> receipt that the canon reader accepts. == Joint attestation -We, the undersigned, assert that *to the best of our joint belief at the -timestamp above, every claim in this file is true and was checked as described* -— with no intentional overclaim, and with the open gaps stated rather than -hidden. - -* *Engineering party (AI):* `` — ran the checks recorded - here at `` and stands behind the wording above as a faithful - report of those runs. -* *Owner / maintainer:* Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> — _signs by committing - this file with `-S`; the git commit signature over this content, at the - commit SHA recorded above, is the cryptographic form of this affirmation._ - -[source,bash] ----- -git commit -S -s docs/AFFIRMATION.adoc -m "docs: affirm state at " -git log --show-signature -1 ----- - -[WARNING] -==== -Do not use `--no-verify`. The pre-commit hook enforces the SPDX header, and an -affirmation landed past its own repo's gates is self-refuting. -==== - -_Landed by a signed git commit. Verify with `git log --show-signature` that the -anchor SHA above matches the parent of the commit that introduced this -affirmation. If they do not match, this file is a *draft* and must be read as -one._ +To the best of our joint belief at the timestamp above, every claim in this +file is true and was checked as described, with no intentional overclaim, +and with the open gaps stated rather than hidden. + +* *Engineering party (AI):* a Claude Code session + (https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk). It ran the checks + recorded here between 2026-11-11T18:16:17Z and 2026-11-11T18:16:56Z, read + CI run 43072763288, and signed the commit that adds this file with the + session's key. +* *Owner / maintainer:* Jonathan D.A. Jewell. By owner ruling of + 2026-11-11, the owner's merge of the pull request that carries this file + is the owner's attestation. + +_Verify with `git log --show-signature` that the anchor commit above is the +parent of the commit that introduced this file. If it is not, read this file +as a draft._