From a26f66ed35d4178c2d1d9c974968dd7253022931 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 18:32:36 +0000 Subject: [PATCH] feat(proofs): write the machine receipt of THY-1 (WO 1.5) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit verification/receipts/theory_praxis.deed is the PROOF-POLICY 8.5.1 receipt of THY-1, written from its record in PROOF-STATUS.adoc. The canon reader (standards be39f90, deed_lint.js --proof-receipt-json) derives PWG-2ii from it, the grade PROOF-STATUS records, and refuses the same receipt when it claims PWG-1. Each receipt says it is a local run, because no CI lane has given one yet; that is why the grade is not PWG-1. - The trusted base is the Agda.Primitive block: agda --dependency-graph puts Agda.Primitive in the cone of FeatureReachability (checked 2026-11-10), and it postulates exactly Level, lzero, lsuc and _⊔_, each bound by BUILTIN. The THY-1 record said the cone was the module alone; it now names Agda.Primitive (PROOF-POLICY 8.4). - CI validates every verification/receipts/*_praxis.deed with the canon reader. The canon pin of the other checks (8e48b1c) predates the reader, so this step has its own pinned, sparse checkout. Not done here: the claim hyperpolymath/mathesis#THY-1 in the registry. The registry's own parser reads only the older quoted receipt shape, so it would show THY-1 as ungraded. WO 2.2 moves the registry to the canon reader; the claim lands with it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- .github/workflows/proven-tests.yml | 17 ++++++++++ docs/status/PROOF-STATUS.adoc | 14 ++++++-- verification/receipts/theory_praxis.deed | 41 ++++++++++++++++++++++++ 3 files changed, 69 insertions(+), 3 deletions(-) create mode 100644 verification/receipts/theory_praxis.deed diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml index 5a3b708..2462066 100644 --- a/.github/workflows/proven-tests.yml +++ b/.github/workflows/proven-tests.yml @@ -45,6 +45,23 @@ jobs: - name: Set up Bun uses: oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6 # v2.2.0 + # PROOF-POLICY 8.5.1: the receipt must read, and the grade it records must + # be the grade the canon reader derives (re-anchoring plan WO 1.5). The + # canon pin above (8e48b1c) predates the reader, so the reader has its own + # pinned, sparse checkout. + - name: Proof receipt reads and derives its recorded grade + run: | + set -euo pipefail + r="$RUNNER_TEMP/receipt-reader" + git init -q "$r" + git -C "$r" remote add origin https://github.com/metadatastician/standards.git + git -C "$r" config core.sparseCheckout true + printf '1-formats/deed/tools/\n' > "$r/.git/info/sparse-checkout" + git -C "$r" fetch -q --depth 1 origin be39f900665fb7c042c05d1165da018adc1860f4 + git -C "$r" checkout -q FETCH_HEAD + for f in verification/receipts/*_praxis.deed; do + bun "$r/1-formats/deed/tools/deed_lint.js" --proof-receipt-json "$f" + done - name: Mathesis census atlas integrity and tests run: | bun scripts/atlas/census-atlas.mjs check diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 32f2f43..583c3d4 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -106,9 +106,12 @@ missing crate as missing from every build. `scripts/check-proofs.sh agda`, which passes. * Source: `f68b78d6ceb8d3c83f96f5ab8e57779442a8834f`; file SHA-256 `4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564`. -* Import cone: the module alone. It imports nothing, the standard - library included, and contains no postulate (comment-aware scan). - `--safe` refuses postulates. +* Import cone: the module and `Agda.Primitive`, which the prover supplies + (`agda --dependency-graph`, checked 2026-11-10). The module imports + nothing, the standard library included, and contains no postulate + (comment-aware scan). `--safe` refuses postulates. `Agda.Primitive` + postulates exactly `Level`, `lzero`, `lsuc` and `_⊔_`, each bound by its + `BUILTIN` pragma: the trusted base the receipt records (§8.4). * Negative controls, all rejected: a planted postulate, a planted false claim, a non-terminating definition, and a `reach-mono` that skips the monotonicity step. @@ -203,6 +206,11 @@ same hypotheses and conclusions. The differences are encoding only: Residual assumptions: none in any leg. +|Machine receipt (§8.5.1) +|`verification/receipts/theory_praxis.deed`. The canon reader +(`deed_lint.js --proof-receipt-json`) derives `PWG-2ii` from it, the grade +below, and CI runs that reader on each change. + |`pwg` |`2ii`: the Agda leg checks, and both recheck legs count (kernel-checked and `RECONCILED`). It is not `PWG-1`, because no leg has a per-commit CI diff --git a/verification/receipts/theory_praxis.deed b/verification/receipts/theory_praxis.deed new file mode 100644 index 0000000..852d62e --- /dev/null +++ b/verification/receipts/theory_praxis.deed @@ -0,0 +1,41 @@ +;; SPDX-License-Identifier: CC-BY-SA-4.0 +;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +;; The proof receipt of Mathesis (PROOF-POLICY §8.5.1), written from the THY-1 +;; record in docs/status/PROOF-STATUS.adoc (re-anchoring plan WO 1.5). Every +;; receipt below is a local run, because no CI lane has given one yet: the run +;; field says so instead of naming a run that does not exist. The reader in +;; standards 1-formats/deed/tools/deed_lint.js derives the grade: +;; bun deed_lint.js --proof-receipt-json verification/receipts/theory_praxis.deed +;; The trusted base is the Agda.Primitive block of the import cone that +;; agda --dependency-graph reports for FeatureReachability (2026-11-10). +(praxis-deed + :schema-version "1.0.0" + :canonical-name "mathesis-theory-receipt" + :beholding-chora #u5"estate/chora" + :profile proof-receipt + :repository "hyperpolymath/mathesis" + :source-commit "f1be654e69b23873ea40651cb40e0e095ac53680" + (trusted-base + (primitive :prover agda :module "Agda.Primitive" :name "Level" :binding "BUILTIN LEVEL") + (primitive :prover agda :module "Agda.Primitive" :name "lzero" :binding "BUILTIN LEVELZERO") + (primitive :prover agda :module "Agda.Primitive" :name "lsuc" :binding "BUILTIN LEVELSUC") + (primitive :prover agda :module "Agda.Primitive" :name "_⊔_" :binding "BUILTIN LEVELMAX")) + (claim :id "THY-1" :pwg PWG-2ii :foundation-diverse #f + (leg :prover agda :route source :token proven :state AGDA-VERIFIED + (receipt :run "local run, 2026-11-09; no CI receipt yet" + :commit "f68b78d6ceb8d3c83f96f5ab8e57779442a8834f" + :checker "agda 2.6.3 (Ubuntu 24.04 agda package)" + :invocation "agda --safe --without-K --cubical-compatible FeatureReachability.agda" + :state current)) + (leg :prover rocq :route re-proved :token proven :state RECONCILED + (receipt :run "local run, 2026-11-09; no CI lane runs Rocq yet" + :commit "f1be654e69b23873ea40651cb40e0e095ac53680" + :checker "coqc 8.18.0 (Ubuntu 24.04 coq package)" + :invocation "coqc FeatureReachability.v" + :state current)) + (leg :prover lean :route re-proved :token proven :state RECONCILED + (receipt :run "local run, 2026-11-09; no CI lane runs Lean yet" + :commit "f1be654e69b23873ea40651cb40e0e095ac53680" + :checker "lean 4.15.0 (11651562caae, release archive)" + :invocation "lean FeatureReachability.lean" + :state current))))