Merge pull request #58 from hyperpolymath/marina/eager-dijkstra-wlmapg

feat(proofs): write the machine receipt of THY-1 (WO 1.5)

Author: hyperpolymath

.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

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

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))))