hyperpolymath · Nov 1, 2026 · Nov 1, 2026 · Nov 1, 2026 · Nov 1, 2026 · Nov 1, 2026
diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
@@ -11,6 +11,8 @@ Before making claims about reversibility, obliteration, Lean↔Rust mechanisatio
 
 The bridge is **documentation-and-orientation-only**, not a mechanised dependency. Keep RMR (reversible) and RMO (irreversible + audit residue) distinct.
 
+The same discipline applies to `hyperpolymath/januskey` and its `reversible-core` crate: **not imported, not a dependency** (measured 2026-11-01 — no import under `proofs/`, no `Cargo.toml` entry, no `.gitmodules`). JanusKey's integration is planned on its side ("Phase 2 — NEXT") and the D204 ruling is a decision, not an implementation. If a change adds `reversible-core`, it is an *implementation* dependency and does not move any claim across the extraction gap. Reversibility here is *algorithmic*, not thermodynamic. Audit record: `docs/audits/2026-11-01-assurance-boundary-audit.adoc`.
+
 ## Machine-Readable Artefacts
 
 The following files in `.machine_readable/` contain structured project metadata:

diff --git a/.machine_readable/bot_directives/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml
@@ -55,7 +55,7 @@ perfective = 10   # % for SPDX headers, doc updates, formatting, style
 # Customise this per project — the template default is generic.
 
 [methodology.unique-strength]
-description = "Proof-backed MAA (Mutually Assured Accountability) framework with polyglot verification: the SAME core reversibility theorems proven across 6 independent proof systems (Coq, Lean 4, Agda, Isabelle/HOL, Mizar, Z3) on top of DIFFERENT logical foundations (CIC, dependent TT, intensional TT, HOL, Tarski-Grothendieck set theory, SMT). Cross-validation between foundations catches modelling errors that any single prover would miss, and the Idris2 ABI layer carries the proof story across the FFI boundary into the Rust CLI runtime. Sibling projects diverge: echidna is dyadic-Coq-only, proven is single-Idris2, ephapax is four-layer-Coq for typed-wasm — none of them carry cross-foundation cross-validation. Divergent-mode work in valence-shell must DEEPEN the polyglot story (close a hole in System X by porting the proof from System Y, tighten the cross-system correspondence, extend Idris2 ABI coverage of newly-proven operations) rather than introduce a 7th system or substitute a stronger single-prover stack."
+description = "Proof-backed MAA (Mutually Assured Accountability) framework with polyglot verification: the SAME core reversibility theorems proven across 6 independent proof systems (Coq, Lean 4, Agda, Isabelle/HOL, Mizar, Z3) on top of DIFFERENT logical foundations (CIC, dependent TT, intensional TT, HOL, Tarski-Grothendieck set theory, SMT). Cross-validation between foundations catches modelling errors that any single prover would miss. The Idris2 ABI layer documents the ABI (layout, encodings, axioms) and is hole-free; it does NOT transport proofs across the FFI boundary into the Rust CLI runtime — the model-to-Rust refinement gap remains open and is the project's stated trust boundary. Sibling projects diverge: echidna is dyadic-Coq-only, proven is single-Idris2, ephapax is four-layer-Coq for typed-wasm — none of them carry cross-foundation cross-validation. Divergent-mode work in valence-shell must DEEPEN the polyglot story (close a hole in System X by porting the proof from System Y, tighten the cross-system correspondence, extend Idris2 ABI coverage of newly-proven operations) rather than introduce a 7th system or substitute a stronger single-prover stack."
 deepen-not-broaden = true
 
 # ============================================================================
@@ -74,12 +74,12 @@ rules = [
   "Polyglot stays at exactly 6 verification systems (Coq, Lean 4, Agda, Isabelle/HOL, Mizar, Z3) — do not add a 7th and do not drop one to simplify",
   "Lean 4 is the canonical specification — when foundations disagree, Lean is the source of truth and the others cross-validate",
   "Coq proofs in proofs/coq/ MUST remain extractable to OCaml — no introduction of non-computational axioms beyond the documented set (funext, well-formedness, decidability of is_empty_dir)",
-  "Proof-hole count is monotone non-increasing — never trade a closed hole for a new one without an explicit ADR; PROOF_HOLES_AUDIT.md is the bookkeeping",
+  "Proof-hole count is monotone non-increasing — never trade a closed hole for a new one without an explicit ADR; PROOF_HOLES_AUDIT.adoc is the bookkeeping",
   "RMR (Remove-Match-Reverse) theorems are reversibility statements; RMO (Remove-Match-Obliterate) theorems are NON-injectivity statements — never collapse the two; the historical mis-statement obliterate_not_reversible was already caught and replaced 2026-04-03",
   "Idris2 ABI layer is the only sanctioned proof-to-FFI carrier — do not bypass it with raw C bindings or unverified Rust FFI",
   "Rust is the single production runtime — divergent work goes into impl/rust-cli/, not into impl/ocaml/ (extraction target, design only) or impl/elixir/ (reference, stale)",
   "POSIX coverage is a means, not an end — do not add shell syntax that has no path to a proof story",
-  "Honest-status discipline — every claim must have a counterpart caveat (EXPLAINME.adoc pattern); README/CLAUDE.md numbers MUST match docs/PROOF_HOLES_AUDIT.md and reality",
+  "Honest-status discipline — every claim must have a counterpart caveat (EXPLAINME.adoc pattern); README/CLAUDE.md numbers MUST match docs/PROOF_HOLES_AUDIT.adoc and reality",
 ]
 
 # Language invariant for the core strength: there is no SINGLE language —
@@ -98,7 +98,7 @@ constraints = [
   "Lean -> Rust correspondence is property-tested only (~85% confidence), NOT mechanised — closing this is the critical-path blocker to v1.0.0",
   "Elixir NIF build is broken — impl/elixir/ is reference-only; do not block work on it",
   "BEAM daemon is designed but not implemented — no current SNIF carrier",
-  "Coq has 0 remaining real proof gaps: obliterate_overwrites_all_blocks is CLOSED (Print Assumptions: Closed under the global context, re-verified 2026-07-16 under Coq 8.18.0) — see docs/PROOF_HOLES_AUDIT.md",
+  "Coq has 0 remaining real proof gaps: obliterate_overwrites_all_blocks is CLOSED (Print Assumptions: Closed under the global context, re-verified 2026-07-16 under Coq 8.18.0) — see docs/PROOF_HOLES_AUDIT.adoc",
   "Agda has 1 structural axiom (funext) — provable in cubical Agda, intentional in intensional TT",
   "Coq has 1 justified decidability axiom (is_empty_dir_dec) — infinite-domain Filesystem = Path -> option FSNode; switching to FMaps.t FSNode is the documented migration",
   "RMO (GDPR / secure deletion): the obliterate command IS implemented and wired (parser+executor -> commands::secure_deletion::obliterate_path; 3-pass overwrite + unlink + append-only audit residue at <root>/.vsh-audit.log; tests/obliterate_rmo_tests.rs). Best-effort on in-place filesystems only; CoW/SSD need hardware secure_erase; audit HMAC signing still pending. Do NOT claim a full GDPR compliance framework.",

diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
@@ -31,9 +31,9 @@ human-explainme           = "EXPLAINME.adoc"
 human-faq                 = "FAQ.adoc"
 
 [honest-status]
-# The single source of truth for proof debt is docs/PROOF_HOLES_AUDIT.md.
+# The single source of truth for proof debt is docs/PROOF_HOLES_AUDIT.adoc.
 # If you see different numbers anywhere, file an issue.
-proof-holes-doc      = "docs/PROOF_HOLES_AUDIT.md"
+proof-holes-doc      = "docs/PROOF_HOLES_AUDIT.adoc"
 deep-audit-log-dir   = "docs/audits/"
 latest-deep-audit    = "docs/audits/2026-06-01-deep-audit.adoc"
 
@@ -63,15 +63,15 @@ service-discovery = "Groove Protocol — not currently wired"
 [delivery-promises]
 # Every agent session must:
 # 1. Read INTENT before changing scope.
-# 2. Update docs/PROOF_HOLES_AUDIT.md the same commit that changes any proof.
+# 2. Update docs/PROOF_HOLES_AUDIT.adoc the same commit that changes any proof.
 # 3. Keep README/CLAUDE.md numbers in sync with reality (see docs/audits/).
 # 4. Never collapse the 6-system polyglot stack (divergent invariant).
 update-on-touch = [
   ".machine_readable/INTENT.contractile",
   ".machine_readable/MUST.contractile",
   ".machine_readable/TRUST.contractile",
   ".machine_readable/ADJUST.contractile",
-  "docs/PROOF_HOLES_AUDIT.md",
+  "docs/PROOF_HOLES_AUDIT.adoc",
   "docs/audits/",
   "CLAUDE.md",
   "README.adoc",

diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
@@ -11,11 +11,48 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 == [Unreleased]
 
+=== Changed — 2026-11-01 (assurance-boundary re-audit)
+
+- Corrected prose that had drifted across the assurance boundary. The audit
+  record is `docs/audits/2026-11-01-assurance-boundary-audit.adoc`. In summary:
+  * the CLI banner and the Elixir moduledoc no longer call the project
+    "thermodynamic" — the claim is *algorithmic* reversibility only;
+  * RMO is described everywhere as best-effort local overwrite + unlink + audit
+    residue, never as physical erasure or GDPR compliance;
+  * the trust-boundary diagram now names the shipped Rust CLI, keeping the
+    extraction/refinement gap as the boundary;
+  * a test comment that said a Lean theorem proves the Rust normaliser now says
+    what it actually proves (the Lean model of the normaliser);
+  * `docs/THEORY-FEED.adoc` states the measured JanusKey situation: zero
+    imports, no `reversible-core` dependency, integration planned upstream only.
+- Stale `.md` references to `docs/LEAN4_RUST_CORRESPONDENCE`, `PROOF_HOLES_AUDIT`,
+  `OCAML_EXTRACTION` and `ZIG_LEAN_EXTRACTION` corrected to `.adoc`.
+
+=== Added — 2026-11-01 (estate proof-policy alignment)
+
+- `EXPLAINME.adoc` now carries the **Proof Ledger** required by `standards`
+  `docs/README-EXPLAINME-STANDARD.adoc` §5: 17 obligation rows, each with a
+  status from the closed vocabulary (`proven`, `proven-with-postulates`,
+  `argued`, `tested-only`, `open`), the checker invocation, the location and the
+  trust boundary. The header states that no prover was installed in the audit
+  environment, so no row was re-run.
+- `CLAUDE.md` gains a normative proof-policy block mapping obligation classes to
+  the verifiers `standards/3-practice/PROOF-POLICY.adoc` assigns
+  (Rust→Creusot, ABI/APIs→Idris2, theory→Agda rechecked in Rocq and Lean).
+- Confidence percentages (~85%, ~95%) are no longer used on any current claim
+  surface. `mathesis` §6 forbids the form; the replacement is a status token per
+  obligation, and mathesis Grades 3/2i/2ii/1 where a grade is needed.
+- Recorded, not fixed: the Agda tree postulates `funext` and is built without
+  the canonical `--safe --without-K --cubical-compatible` invocation, so no Agda
+  row can be `proven`; the Mizar target swallows failure (`|| echo`). Both are
+  logged as AP-6, AP-7 and AP-8 in the audit.
+
 === Planned
 - Glob expansion (*.txt, ?.rs, [a-z]*)
 - Quote processing (proper escaping, single/double quotes)
 - Full POSIX shell compliance (subset)
-- RMO (Remove-Match-Obliterate) proofs for GDPR compliance
+- RMO (Remove-Match-Obliterate) non-injectivity proofs — audit evidence about the
+  abstract model, explicitly not a GDPR compliance determination
 
 === Added — 2026-07-17
 
@@ -27,10 +64,16 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   `"obliterate"` parser case (with `--force`/`-f`), and the executor arm routing
   to `secure_deletion::obliterate_path` (file/dir dispatch). Proof reference:
   `OBLITERATE_IRREVERSIBLE`.
-- **Audit residue**: obliterate now appends an append-only record to
-  `<sandbox-root>/.vsh-audit.log` — the MAA attestation that survives the data
-  destruction (GDPR Article 17 evidence). Data is destroyed; proof-of-deletion
-  persists.
+- **Audit residue**: obliterate appends an append-only record to
+  `<sandbox-root>/.vsh-audit.log` — an unsigned record that the command ran,
+  which survives the deletion.
+
+  *Corrected 2026-11-01:* this bullet originally read "the MAA attestation that
+  survives the data destruction (GDPR Article 17 evidence). Data is destroyed;
+  proof-of-deletion persists." That overstated the guarantee. The overwrite is
+  best-effort and local; CoW extents, journals, snapshots, device spares and
+  replicas are outside it, and an unsigned residue is not an attestation or legal
+  evidence. See `docs/RMO-DURABILITY-BOUNDARY.adoc`.
 - Tests: `impl/rust-cli/tests/obliterate_rmo_tests.rs` (6 tests) — dispatch
   wiring, missing-operand error, end-to-end destruction, audit residue,
   irreversibility (undo cannot resurrect), and no-old-plaintext-remains. Full
@@ -55,7 +98,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   cleanly when the oracle is not built.
 - `just build-model-oracle` / `just test-correspondence-model`; wired into
   `lean-verification.yml` CI.
-- `docs/LEAN4_RUST_CORRESPONDENCE.md` documents the harness, why the Coq
+- `docs/LEAN4_RUST_CORRESPONDENCE.adoc` documents the harness, why the Coq
   extraction is not executable (function-typed filesystem + classical axioms;
   needs `FMaps.t FSNode` migration), and the roadmap to full mechanization.
 
@@ -109,7 +152,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   2026-06-02 admits (#56/#57/#58) are all closed. Remaining assumptions
   are standard/justified: Coq `functional_extensionality` (stdlib) +
   `is_empty_dir_dec` (justified classical), Agda `funext` (structural).
-  Docs reconciled: `PROOF_HOLES_AUDIT.md`, `README.adoc`, `FAQ.adoc`,
+  Docs reconciled: `PROOF_HOLES_AUDIT.adoc`, `README.adoc`, `FAQ.adoc`,
   `CLAUDE.md`, `docs/wiki/`, `ROADMAP*.{adoc,md}`,
   `.machine_readable/6a2/STATE.a2ml`, `bot_directives/methodology.a2ml`.
 
@@ -350,7 +393,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   - Updated REPL with new parser and external execution
 
 - **Architecture Documentation**
-  - LEAN4_RUST_CORRESPONDENCE.md
+  - LEAN4_RUST_CORRESPONDENCE.adoc
   - ECHIDNA_INTEGRATION.md
   - ARCHITECTURE.md
   - POSIX_COMPLIANCE.md with 14-milestone roadmap
@@ -372,8 +415,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 === Documentation
 - PHASE6_M1_DESIGN.md
 - EXTRACTION_SUMMARY.md (500 lines)
-- docs/OCAML_EXTRACTION.md (600 lines)
-- docs/ZIG_LEAN_EXTRACTION.md (700 lines)
+- docs/OCAML_EXTRACTION.adoc (600 lines)
+- docs/ZIG_LEAN_EXTRACTION.adoc (700 lines)
 
 == [0.6.0] - 2025-12-01