From 8b4326aa88e1fd45e2684cec18c6459cfd2c8b71 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:07:37 +0000
Subject: [PATCH 1/2] docs(proofs): align Hypatia status with Agda and
 cross-kernel evidence policy

---
 verification/PROOF-STATUS.adoc | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc
index 53e33165..77df8a4b 100644
--- a/verification/PROOF-STATUS.adoc
+++ b/verification/PROOF-STATUS.adoc
@@ -10,8 +10,28 @@ neurosymbolic CI/CD platform.
 `+Admitted+`
 * All proofs are constructive
 * `+%default total+` in all Idris2 files
-* Idris2 for type-level proofs; Lean 4 for theorem proving where
-convenient
+* Idris2 for cross-language interface and ABI contracts; runtime code
+  obligations follow the estate's Creusot-for-Rust/SPARK-for-Ada mapping
+* For implementation-independent theory, Agda is the primary proof target.
+  Convert an earlier proof where possible; otherwise re-prove the theorem
+  in Agda, then recheck the witness or re-prove the same statement in
+  Rocq/Coq and Lean. A translation alone is not a proof.
+* Every Agda check runs: agda --safe --without-K --cubical-compatible
+  against a pinned toolchain. Capital K is required.
+* For each target recheck, record the statement/assumption correspondence,
+  checker version, exact invocation, receipt and source/witness digest.
+  Missing tools, unchecked transports and unsuccessful checks are not
+  promoted to PROVEN. An unsuccessful translation does not refute or
+  delete the earlier theorem.
+* Canonical estate policy:
+  https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[Proof and Verification Policy].
+  This file is a proof inventory, not an independent alternative policy.
+
+NOTE: This repo currently verifies Idris2, Lean and TLA+ artefacts in CI.
+It does not yet run an Agda + Rocq + Lean reconciliation pipeline.
+The pre-existing Lean files below retain their documented scope; they
+must not be represented as independently rechecking Agda proofs until
+the checked Agda source and correspondence evidence actually exist.
 
 === Proof Inventory
 

From 8d4c1a040727c09833367aaa6f3a38099659fb09 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 09:29:35 +0000
Subject: [PATCH 2/2] Update verification/PROOF-STATUS.adoc

Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
---
 verification/PROOF-STATUS.adoc | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc
index 77df8a4b..5eaeef37 100644
--- a/verification/PROOF-STATUS.adoc
+++ b/verification/PROOF-STATUS.adoc
@@ -14,8 +14,9 @@ neurosymbolic CI/CD platform.
   obligations follow the estate's Creusot-for-Rust/SPARK-for-Ada mapping
 * For implementation-independent theory, Agda is the primary proof target.
   Convert an earlier proof where possible; otherwise re-prove the theorem
-  in Agda, then recheck the witness or re-prove the same statement in
-  Rocq/Coq and Lean. A translation alone is not a proof.
+  in Agda, then transport the witness to Rocq/Coq and Lean. Re-prove the
+  same statement only when transport is unavailable or unsupported. A
+  translation alone is not a proof.
 * Every Agda check runs: agda --safe --without-K --cubical-compatible
   against a pinned toolchain. Capital K is required.
 * For each target recheck, record the statement/assumption correspondence,