From c66aeb3b388e05fd5197b3d68d58f0fe87ec3182 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 7 Nov 2026 01:37:22 +0000
Subject: [PATCH 1/3] Bridge Epistemic recovery to canonical Echo and restore
 required CI

---
 .github/workflows/actions.lock           |  55 +-------
 .github/workflows/agda.yml               |   9 +-
 .github/workflows/governance.yml         |   2 +-
 .github/workflows/secret-scanner.yml     |   4 +-
 Justfile                                 |   2 +-
 PROOF-STATUS.adoc                        |  28 +++-
 README.adoc                              |   8 +-
 docs/echo-recovery-adapter.adoc          | 171 +++++++++++++++++++++++
 scripts/check-canonical.sh               |  31 ++++
 tests/check-policy.sh                    |   2 +
 tests/integration/CanonicalRecovery.agda |  66 +++++++++
 tests/integration/RecoveryExamples.agda  | 137 ++++++++++++++++++
 12 files changed, 449 insertions(+), 66 deletions(-)
 create mode 100644 docs/echo-recovery-adapter.adoc
 create mode 100644 scripts/check-canonical.sh
 create mode 100644 tests/integration/CanonicalRecovery.agda
 create mode 100644 tests/integration/RecoveryExamples.agda

diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index 6e09252..31b0cf4 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -1,57 +1,25 @@
 # This file is machine-generated by `gh actions-lock`.
 # Do not edit by hand; run `gh actions-lock` to update.
 # Docs: https://gh.io/actions-lockfile
-version: 'v0.0.2'
+version: 'v0.0.3'
 workflows:
     '.github/workflows/agda.yml':
         - 'actions/checkout@v6.0.3'
     '.github/workflows/codeql.yml':
         - 'actions/checkout@v6.0.3'
         - 'github/codeql-action@v4.36.2'
-    '.github/workflows/governance.yml':
-        - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66'
+    '.github/workflows/governance.yml': []
     '.github/workflows/label-triage.yml': []
     '.github/workflows/labels.yml': []
     '.github/workflows/push-email-notify.yml':
         - 'hyperpolymath/smtp-notify-action@v0.2.0'
-    '.github/workflows/secret-scanner.yml':
-        - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66'
+    '.github/workflows/secret-scanner.yml': []
 dependencies:
-    'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9':
-        ref: 'v6.1.0'
-        commit: 'sha1-55cc8345863c7cc4c66a329aec7e433d2d1c52a9'
-        owner_id: 44036562
-        repo_id: 215566462
-    'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1':
-        ref: 'v7.0.1'
-        commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1'
-        owner_id: 44036562
-        repo_id: 197814629
     'actions/checkout@v6.0.3':
         ref: 'v6.0.3'
         commit: 'sha1-df4cb1c069e1874edd31b4311f1884172cec0e10'
         owner_id: 44036562
         repo_id: 197814629
-    'denoland/setup-deno@22d081ff2d3a40755e97629de92e3bcbfa7cf2ed':
-        ref: 'v2.0.5'
-        commit: 'sha1-22d081ff2d3a40755e97629de92e3bcbfa7cf2ed'
-        owner_id: 42048915
-        repo_id: 356423100
-    'editorconfig-checker/action-editorconfig-checker@51f63319f592f97930c73d9c46184d20bd206393':
-        ref: 'v3.0.0'
-        commit: 'sha1-51f63319f592f97930c73d9c46184d20bd206393'
-        owner_id: 26415196
-        repo_id: 297874902
-    'editorconfig-checker/action-editorconfig-checker@840e866d93b8e032123c23bac69dece044d4d84c':
-        ref: 'v2.2.0'
-        commit: 'sha1-840e866d93b8e032123c23bac69dece044d4d84c'
-        owner_id: 26415196
-        repo_id: 297874902
-    'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124':
-        ref: 'v1.24.1'
-        commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124'
-        owner_id: 47606891
-        repo_id: 331103973
     'github/codeql-action@v4.36.2':
         ref: 'v4.36.2'
         commit: 'sha1-8aad20d150bbac5944a9f9d289da16a4b0d87c1e'
@@ -62,20 +30,3 @@ dependencies:
         commit: 'sha1-ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7'
         owner_id: 6759885
         repo_id: 1352485172
-    'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66':
-        ref: '75bd5994470661a099df562d6d5ad2fe744dbd66'
-        commit: 'sha1-75bd5994470661a099df562d6d5ad2fe744dbd66'
-        owner_id: 6759885
-        repo_id: 1116521501
-        uses:
-            - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9'
-            - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
-            - 'denoland/setup-deno@22d081ff2d3a40755e97629de92e3bcbfa7cf2ed'
-            - 'editorconfig-checker/action-editorconfig-checker@51f63319f592f97930c73d9c46184d20bd206393'
-            - 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124'
-            - 'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6'
-    'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6':
-        ref: 'v2.2.0'
-        commit: 'sha1-0c5077e51419868618aeaa5fe8019c62421857d6'
-        owner_id: 108928776
-        repo_id: 512644635
diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml
index 34505f0..7cbceb7 100644
--- a/.github/workflows/agda.yml
+++ b/.github/workflows/agda.yml
@@ -72,13 +72,10 @@ jobs:
         uses: actions/checkout@v6.0.3
         with:
           repository: hyperpolymath/echo-types
-          ref: 46cd1a32d4dcf1020f01dd1aab41f816742da10e
+          ref: ebde9ac4e1a9f115b441c642c82aced1316c5983
           path: .ci-deps/echo-types
           persist-credentials: false
-      - name: Prove representation round trips and lowering agreement
+      - name: Prove residue and recovery correspondence with boundary examples
         run: |
           test "$(agda --version)" = 'Agda version 2.6.4.3'
-          agda --no-libraries --safe --without-K --cubical-compatible --double-check --ignore-interfaces \
-            -W error -W noUnsupportedIndexedMatch -i src -i tests/integration \
-            -i .ci-deps/echo-types/proofs/agda -i /usr/share/agda-stdlib/src \
-            tests/integration/CanonicalEcho.agda
+          bash scripts/check-canonical.sh .ci-deps/echo-types /usr/share/agda-stdlib/src
diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
index 4ac360c..4fefadb 100644
--- a/.github/workflows/governance.yml
+++ b/.github/workflows/governance.yml
@@ -15,4 +15,4 @@ permissions:
 
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@75bd5994470661a099df562d6d5ad2fe744dbd66
+    uses: metadatastician/standards/.github/workflows/governance-reusable.yml@ba640e9a57f22608710ffecdca282074eac55a0b
diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml
index 5f4c294..7b8353e 100644
--- a/.github/workflows/secret-scanner.yml
+++ b/.github/workflows/secret-scanner.yml
@@ -18,5 +18,5 @@ concurrency:
 permissions:
   contents: read
 jobs:
-  scan:
-    uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@75bd5994470661a099df562d6d5ad2fe744dbd66
+  secret-scan:
+    uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@75bd5994470661a099df562d6d5ad2fe744dbd66
diff --git a/Justfile b/Justfile
index 0e043c4..80cbe0c 100644
--- a/Justfile
+++ b/Justfile
@@ -14,7 +14,7 @@ check-rejections:
 
 # Optional integration gate: actual echo-types checkout and stdlib source.
 check-canonical echo_root stdlib_src:
-	agda --no-libraries --safe --without-K --cubical-compatible --double-check --ignore-interfaces -W error -W noUnsupportedIndexedMatch -i src -i tests/integration -i '{{echo_root}}/proofs/agda' -i '{{stdlib_src}}' tests/integration/CanonicalEcho.agda
+	bash scripts/check-canonical.sh '{{echo_root}}' '{{stdlib_src}}'
 
 # Build/test/validate include positive proofs and semantic rejection controls.
 build: check
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 8374aec..d6c4a6b 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = epistemic-types — proof status
-:revdate: 2026-11-04
+:revdate: 2026-11-07
 :toc:
 :sectnums:
 
@@ -17,6 +17,20 @@ not current inventory.
 
 == Status vocabulary
 
+The 2026-11-07 optional recovery integration adds
+`tests/integration/CanonicalRecovery.agda` and `RecoveryExamples.agda`.
+It is locally *AGDA-VERIFIED* under the native Agda 2.6.4.3 / stdlib 2.1
+profile and separately under Echo's Agda 2.7.0.1 / stdlib 2.3 profile,
+using Echo `ebde9ac4e1a9f115b441c642c82aced1316c5983`.
+The 23-module builtins-only core is unchanged. Its original native gate was
+reproduced with all 17 semantic rejection fixtures and four mutation controls;
+the updated policy gate covers three integration modules. The adapter proves
+inverse conversions for a fixed retention contract, preserving the total
+decoder and supplied round-trip proof, and transports the finite-alphabet
+bound. See link:docs/echo-recovery-adapter.adoc[the precise contract and local
+receipt]. These local checks are distinct from the older hosted receipts
+below and do not confer independent-review or cross-prover credit.
+
 The 2026-11-03 approval-seal extension is locally *AGDA-VERIFIED* under Agda
 2.6.4.3 and the canonical safety profile. `Applications/ApprovalSeal.agda` defines AS-1..AS-8:
 exact approval binding, agent-trace anchor preservation, an irreversible
@@ -230,7 +244,17 @@ runtime or an unlisted mathematical correspondence.
   correspondence only, not a full graded-comonad or runtime theorem.
 | TESTED
 | `tests/integration/CanonicalEcho.agda`; Echo pin
-  `46cd1a32d4dcf1020f01dd1aab41f816742da10e`
+  `ebde9ac4e1a9f115b441c642c82aced1316c5983`; locally rechecked 2026-11-07
+
+| C-3
+| For a fixed `Retention` at `Set`, native `Recovery` and canonical
+  `ExactRecovery` have inverse field-copy conversions, preserving the total
+  decoder and its round-trip proof. Exact recovery transfers the finite
+  single-fibre alphabet bound and forbids residue collisions. Certificate,
+  empty-source and off-image controls delimit the contract.
+| PROVEN — local receipt 2026-11-07
+| `tests/integration/CanonicalRecovery.agda`, `RecoveryExamples.agda`;
+  link:docs/echo-recovery-adapter.adoc[assumptions and verification scope]
 |===
 
 == External pinned evidence, not local closure
diff --git a/README.adoc b/README.adoc
index e3ed0d5..d06a261 100644
--- a/README.adoc
+++ b/README.adoc
@@ -96,8 +96,12 @@ that discarded distinctions cannot support a migration requiring those
 distinctions. Resource grades are separate, measured upper bounds.
 
 See link:docs/continuity-foundations.adoc[the breaking API correction and proof
-boundaries]. An optional integration gate proves correspondence with the actual
-sibling `EchoResidue.EchoR`; the core remains dependency-free.
+boundaries]. The optional integration gate connects the actual sibling
+`EchoResidue.EchoR` and `EchoFiniteResidue.ExactRecovery` records. The recovery
+adapter preserves the full decoder and supplied round-trip proof, transfers
+the finite-alphabet bound, and includes certificate, collision and off-image
+controls. See link:docs/echo-recovery-adapter.adoc[the contract and reproduction
+commands]. The core remains dependency-free.
 
 == Applications: the RapidNJ Q-criterion
 
diff --git a/docs/echo-recovery-adapter.adoc b/docs/echo-recovery-adapter.adoc
new file mode 100644
index 0000000..11dd88e
--- /dev/null
+++ b/docs/echo-recovery-adapter.adoc
@@ -0,0 +1,171 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Epistemic recovery and canonical Echo recovery
+:revdate: 2026-11-07
+
+== Contract and dependency boundary
+
+`tests/integration/CanonicalRecovery.agda` imports the actual owning
+`EpistemicTypes.EchoBridge.Recovery` and `EchoFiniteResidue.ExactRecovery`
+records. For a fixed `Retention A B R`, both require a total curried decoder
+and the same source-value round trip. The adapter specializes Echo's
+universe-polymorphic contract to Epistemic's `Set` carriers. It does not
+generalize the Epistemic core to arbitrary universe levels.
+
+The two adapters copy both fields. `fromToRecovery` and
+`toFromExactRecovery` prove full record inverses by record eta, including
+the supplied round-trip proofs. `decoderAgrees` covers every visible/residue
+input, including unreachable inputs. `roundtripProofAgrees` preserves the
+particular proof supplied by the caller. Neither proof uses function
+extensionality, proof irrelevance, choice, or a constructed extension from a
+partial decoder.
+
+The retention contract, its certificate family, and its soundness witness
+stay fixed. Recovery does not consume a certificate, infer its intended
+meaning, or follow from certificate validity. The existing
+`CanonicalEcho` representation conversion separately preserves the residue
+and certificate. No equality witness in the dependent fibre is reconstructed.
+
+The bridge lives in the optional integration tree so the 23-module core
+remains builtins-only. Echo does not acquire an Epistemic dependency.
+This is an identification of two existing interfaces, not a new recovery
+principle or a claim of novelty.
+
+== Transferred theorem and controls
+
+[cols="2,4",options="header"]
+|===
+|Declaration |Exact scope
+|`recoveryFiniteFibreBound`
+|An injected family of `n` sources in one observation fibre, residues in
+`Fin k`, and a supplied recovery imply `n ≤ k`. The family need not enumerate
+the fibre. This reuses Echo's finite pigeonhole theorem; cost is alphabet
+cardinality, not bits, entropy, time, or physical information loss.
+|`recoveryForbidsResidueCollision`
+|Two distinct sources with the same observation cannot have the same residue
+under a supplied exact recovery. This is a necessary condition; no general
+construction of recovery from collision-freedom is asserted.
+|`twoSymbolBound`, `twoCertificatePreserved`
+|Two sources in one visible fibre retain their own `Fin 2` values. The
+certificate restricts observations to that fibre, recovery attains `2 ≤ 2`,
+and canonical residue conversion preserves the original certificate proof.
+|`noOneSymbolRecovery`
+|The constant observation and constant one-symbol residue on `Fin 2`
+cannot support recovery, despite every generated residue being certified.
+|`emptyCertifiedDecoder`, `noEmptyRecovery`, `noEmptyExactRecovery`
+|With empty source, singleton observation/residue, and empty certificates,
+certificate-restricted decoding and its round trip are vacuous. Total
+decoding is impossible. A certified-only or reachable-only replacement would
+therefore change the contract.
+|`decodersAgreeOnImage`, `decodersDisagreeOffImage`, `adapterPreservesOffImage`
+|Two Bool decoders satisfy the same round-trip law and agree on every
+generated pair, yet differ at an unreachable pair. The adapter preserves
+that difference; on-image agreement alone does not identify total decoders.
+|===
+
+These statements concern source values and mathematical functions.
+Execution provenance, authorization, secret visibility, runtime ownership,
+linear consumption and independent proof-assistant translations remain
+separate obligations. Ordinal research is outside this work.
+
+== Reproduction
+
+Epistemic base: `a4a7a533f11996e9f57e67466566d950322b0d4f`.
+Reviewed canonical Echo pin: `ebde9ac4e1a9f115b441c642c82aced1316c5983`.
+The owning integration job retains Agda `2.6.4.3` and Debian standard-library
+package `2.1-4`; the source-only core requires no standard library.
+
+[source,shell]
+----
+bash scripts/check.sh
+bash scripts/check-canonical.sh /path/to/echo-types /path/to/stdlib/src
+----
+
+The canonical script cold-checks `RecoveryExamples`, whose import closure
+contains the existing representation bridge and the recovery adapter.
+The policy gate lists those three integration modules explicitly. Each first-party source retains
+all six canonical local options. The integration command retains the
+previous safe/without-K/cubical-compatible profile, double checking and
+`--ignore-interfaces`, with the same existing `UnsupportedIndexedMatch`
+exception to warnings-as-errors. Local source options are not imposed on
+third-party standard-library modules.
+
+Typechecking does not establish warning-free Cubical transport computation.
+The exact source revisions, executed checks and warning observations belong
+in the accompanying receipt; a future pin or compiler change needs a new one.
+
+== Local verification receipt — 2026-11-07
+
+The original Epistemic gate was reproduced with `/usr/bin/agda` from Debian
+`agda-bin=2.6.4.3-1+b2`, `agda-stdlib=2.1-4`, and `LANG=LC_ALL=C.UTF-8`.
+It checked all 23 core modules, the exact 23-span indexed-match warning
+manifest, all 17 expected semantic rejections and four approval-seal mutation
+controls. The existing `CanonicalEcho` root passed first with its original
+Echo pin `46cd1a32d4dcf1020f01dd1aab41f816742da10e`, then with `ebde9ac4`.
+Unsuppressed diagnostics on those two runs matched: 24 occurrences at four
+unique spans, with no new category or location. These are native executions
+of the workflow commands, not executions of the pinned CI container image.
+
+The updated policy gate passed with 23 source modules, 17 rejection fixtures
+and three integration modules. Source manifests confirmed that all 23 core
+modules are byte-identical to the reproduced baseline. Both the direct
+`CanonicalRecovery` root and the complete `RecoveryExamples` closure passed
+native cold checks. A separate cold check of the full closure passed with
+Agda 2.7.0.1 and stdlib 2.3 at
+`8326c7475af1fa456ca04a0203c168d5d7ff842b`.
+
+A separate unsuppressed native cold check of the expanded recovery closure
+also passed. It emitted 776 `UnsupportedIndexedMatch` diagnostics at 161
+distinct source spans, with no span in the three integration modules.
+The larger count follows the newly imported finite-bound standard-library
+cone; repeated occurrences are not separate defects. This is expressly not
+a warning-free Cubical computation result. That log's SHA256 is
+`bb18a7c395b41c0901361f0e3d35ea80c575b4230072baad58ef550a625276da`.
+
+Normalized LF source SHA256 values at those checks:
+
+[cols="1,3",options="header"]
+|===
+|Source |SHA256
+|`tests/integration/CanonicalRecovery.agda`
+|`3448f8297f3b94e2570a8c0424e95aa0ed70491b250ecaba8f2c316a8eeb77c1`
+|`tests/integration/RecoveryExamples.agda`
+|`bf288865decf52669dfa325b232da76eb7127b38b56c7990e86307d92d75524a`
+|`tests/check-policy.sh`
+|`9946df9b41a916034d53614407928520d8ba9a1307968caac51a8c0aef68aea6`
+|`scripts/check-canonical.sh`
+|`38d96565163f0c1017d0856c4f7316fa2ac94649676302b6ad0fd6950654090c`
+|===
+
+The machine's installed standard-library directory rejected interface writes.
+The successful native runs used a private writable copy whose complete Agda
+source manifest matched the installed package. The earlier attempt failed
+before theorem checking. An initial extra global `--exact-split` option also
+exposed an existing stdlib 2.1 exact-splitting diagnostic; subsequent checks
+used the actual integration command, retaining all six local first-party
+options and adding no warning-category exception. Intermittent WSL startup
+timeouts were avoided with persistent shells; they were not proof failures.
+
+Raw local logs and source manifests are retained in the coordinating
+workspace's `.echo-proof-tools/epistemic-ci-20261107/` and
+`.echo-proof-tools/recovery-adapter-20261107/`. They are local artifacts,
+not links to remotely available files. The commands, pins, source identities
+and scope above are the distributable receipt.
+
+== Required workflow repair
+
+The governance and scanner callers now use the published
+`metadatastician/standards` owner. Governance is pinned to
+`ba640e9a57f22608710ffecdca282074eac55a0b`; the scanner retains
+`75bd5994470661a099df562d6d5ad2fe744dbd66`. The scanner caller ID is
+`secret-scan`, matching the existing required `secret-scan / gitleaks`
+context. No branch rule or required check was removed.
+
+Official `github/gh-actions-lock` v0.4.1 regenerated the supported v0.0.3
+lockfile, and both `--verify-local` and online `--verify` passed. Its
+https://github.com/github/gh-actions-lock/blob/v0.4.1/README.md#limitations[documented limitation]
+excludes external reusable workflows from locking. Their explicit SHA pins
+remain in the caller source; the lock does not certify their transitive
+dependencies. The five unrelated workflow mappings and three ordinary
+action dependency records are unchanged. Successful lock verification alone
+does not establish success of the hosted governance jobs.
diff --git a/scripts/check-canonical.sh b/scripts/check-canonical.sh
new file mode 100644
index 0000000..bea198d
--- /dev/null
+++ b/scripts/check-canonical.sh
@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+# Cross-repository checks stay separate from the builtins-only core gate.
+set -euo pipefail
+if [[ $# -ne 2 ]]; then
+  printf 'Usage: bash scripts/check-canonical.sh ECHO_ROOT STDLIB_SRC\n' >&2
+  exit 64
+fi
+echo_root=$(cd -- "$1" && pwd)
+stdlib_src=$(cd -- "$2" && pwd)
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+prover=${AGDA:-agda}
+for dependency in "$echo_root/proofs/agda/Echo.agda" \
+                  "$echo_root/proofs/agda/EchoResidue.agda" \
+                  "$echo_root/proofs/agda/EchoFiniteResidue.agda" \
+                  "$stdlib_src/Data/Fin/Properties.agda"; do
+  [[ -r $dependency ]] || { printf 'FAIL: missing dependency: %s\n' "$dependency" >&2; exit 1; }
+done
+"$prover" --version
+# Retain the integration job's existing UnsupportedIndexedMatch policy.
+# Success does not assert Cubical transport computation for indexed matches.
+# Each first-party module also declares exact-split/no-sized-types/no-guardedness.
+# Do not impose those local options on the independently maintained stdlib.
+# RecoveryExamples imports both CanonicalEcho and CanonicalRecovery: one cold
+# closure checks all three policy-manifest modules without rechecking the
+# same standard library three times.
+"$prover" --no-libraries --safe --without-K --cubical-compatible \
+  --double-check --ignore-interfaces \
+  -W error -W noUnsupportedIndexedMatch -i src -i tests/integration \
+  -i "$echo_root/proofs/agda" -i "$stdlib_src" tests/integration/RecoveryExamples.agda
diff --git a/tests/check-policy.sh b/tests/check-policy.sh
index 4d7f9ec..a9af153 100755
--- a/tests/check-policy.sh
+++ b/tests/check-policy.sh
@@ -54,6 +54,8 @@ expected_rejection_fixtures=(
 # shellcheck disable=SC2034 # consumed through require_exact_inventory namerefs
 expected_integration_modules=(
   tests/integration/CanonicalEcho.agda
+  tests/integration/CanonicalRecovery.agda
+  tests/integration/RecoveryExamples.agda
 )
 
 collect_agda_paths() {
diff --git a/tests/integration/CanonicalRecovery.agda b/tests/integration/CanonicalRecovery.agda
new file mode 100644
index 0000000..84d7018
--- /dev/null
+++ b/tests/integration/CanonicalRecovery.agda
@@ -0,0 +1,66 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module CanonicalRecovery where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Data.Fin.Base using (Fin)
+open import Data.Nat.Base using (ℕ; _≤_)
+open import Relation.Binary.PropositionalEquality using (_≢_)
+import EchoFiniteResidue as Finite
+open import EpistemicTypes.EchoBridge using (Retention; Recovery)
+
+-- Import the owning definitions. Keep the full retention contract C fixed:
+-- neither conversion chooses a certificate nor reconstructs one from recovery.
+-- Epistemic's carriers are Set₀; the canonical contract is specialized here.
+toExactRecovery : {A B R : Set} {C : Retention A B R} → Recovery C →
+  Finite.ExactRecovery (Retention.observe C) (Retention.retain C)
+toExactRecovery rec = record
+  { recover = Recovery.recover rec
+  ; roundtrip = Recovery.roundtrip rec
+  }
+
+fromExactRecovery : {A B R : Set} {C : Retention A B R} →
+  Finite.ExactRecovery (Retention.observe C) (Retention.retain C) → Recovery C
+fromExactRecovery rec = record
+  { recover = Finite.ExactRecovery.recover rec
+  ; roundtrip = Finite.ExactRecovery.roundtrip rec
+  }
+
+-- Record eta suffices, including the proof field. No function extensionality
+-- or proof irrelevance is required. These laws preserve the TOTAL decoder,
+-- including inputs that no source actually produces.
+fromToRecovery : {A B R : Set} {C : Retention A B R} (rec : Recovery C) →
+  fromExactRecovery {C = C} (toExactRecovery rec) ≡ rec
+fromToRecovery rec = refl
+
+toFromExactRecovery : {A B R : Set} {C : Retention A B R}
+  (rec : Finite.ExactRecovery (Retention.observe C) (Retention.retain C)) →
+  toExactRecovery (fromExactRecovery {C = C} rec) ≡ rec
+toFromExactRecovery rec = refl
+
+decoderAgrees : {A B R : Set} {C : Retention A B R}
+  (rec : Recovery C) (y : B) (r : R) →
+  Finite.ExactRecovery.recover (toExactRecovery rec) y r ≡ Recovery.recover rec y r
+decoderAgrees rec y r = refl
+
+roundtripProofAgrees : {A B R : Set} {C : Retention A B R}
+  (rec : Recovery C) (x : A) →
+  Finite.ExactRecovery.roundtrip (toExactRecovery rec) x ≡ Recovery.roundtrip rec x
+roundtripProofAgrees rec x = refl
+
+-- The existing canonical finite-alphabet theorem now applies to the actual
+-- Epistemic observation and retention functions. The selected sources need
+-- not enumerate a whole fibre. Cost here is alphabet cardinality only.
+recoveryFiniteFibreBound : {A B : Set} {n k : ℕ} {C : Retention A B (Fin k)} →
+  Recovery C → (select : Fin n → A) →
+  (∀ {i j} → select i ≡ select j → i ≡ j) →
+  (y : B) → (∀ i → Retention.observe C (select i) ≡ y) → n ≤ k
+recoveryFiniteFibreBound rec = Finite.finite-fibre-bound (toExactRecovery rec)
+
+recoveryForbidsResidueCollision : {A B R : Set} {C : Retention A B R} →
+  Recovery C → ∀ {x z} → x ≢ z →
+  Retention.observe C x ≡ Retention.observe C z → Retention.retain C x ≢ Retention.retain C z
+recoveryForbidsResidueCollision rec =
+  Finite.recovery-forbids-residue-collision (toExactRecovery rec)
diff --git a/tests/integration/RecoveryExamples.agda b/tests/integration/RecoveryExamples.agda
new file mode 100644
index 0000000..070c246
--- /dev/null
+++ b/tests/integration/RecoveryExamples.agda
@@ -0,0 +1,137 @@
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+module RecoveryExamples where
+
+open import Data.Bool.Base using (Bool; false; true)
+open import Data.Empty using (⊥)
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Nat.Base using (_≤_)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Unit.Base using (⊤; tt)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+import CanonicalEcho as Residues
+import CanonicalRecovery as Adapter
+import EchoFiniteResidue as Exact
+import EpistemicTypes.EchoBridge as Epistemic
+
+-- Two distinct sources occupy one visible fibre. Identity retention supplies
+-- enough residue; the certificate restricts the visible index to that fibre.
+twoRetention : Epistemic.Retention (Fin 2) (Fin 2) (Fin 2)
+Epistemic.Retention.observe twoRetention _ = zero
+Epistemic.Retention.retain twoRetention x = x
+Epistemic.Retention.Cert twoRetention _ y = y ≡ zero
+Epistemic.Retention.sound twoRetention _ = refl
+
+twoRecovery : Epistemic.Recovery twoRetention
+Epistemic.Recovery.recover twoRecovery _ r = r
+Epistemic.Recovery.roundtrip twoRecovery _ = refl
+
+twoExactRecovery :
+  Exact.ExactRecovery (Epistemic.Retention.observe twoRetention)
+    (Epistemic.Retention.retain twoRetention)
+twoExactRecovery = Adapter.toExactRecovery twoRecovery
+
+twoAdapterRoundtrip : (x : Fin 2) ->
+  Epistemic.Recovery.recover
+    (Adapter.fromExactRecovery {C = twoRetention} twoExactRecovery) zero x ≡ x
+twoAdapterRoundtrip x = refl
+
+-- This is the actual two-source single-fibre bound, not a claim about bits,
+-- entropy, security or the cardinality of every source fibre.
+twoSymbolBound : 2 ≤ 2
+twoSymbolBound = Adapter.recoveryFiniteFibreBound twoRecovery
+  (λ x -> x) (λ p -> p) zero (λ _ -> refl)
+
+-- Existing canonical residue conversion copies the original proof, rather
+-- than proving all certificates equal or recovering an equality witness.
+twoCertificatePreserved : {y : Fin 2} (e : Epistemic.Echo twoRetention y) ->
+  Epistemic.Echo.certified
+    (Residues.fromCanonical {C = twoRetention} (Residues.toCanonical e)) ≡
+  Epistemic.Echo.certified e
+twoCertificatePreserved (Epistemic.echo r cert) = refl
+
+twoOtherFibreUncertified : Epistemic.Echo twoRetention (suc zero) -> ⊥
+twoOtherFibreUncertified (Epistemic.echo r ())
+
+-- A certificate may be valid while the retained pair loses a source
+-- distinction. The transferred collision theorem forbids any total recovery.
+oneSymbolRetention : Epistemic.Retention (Fin 2) ⊤ (Fin 1)
+Epistemic.Retention.observe oneSymbolRetention _ = tt
+Epistemic.Retention.retain oneSymbolRetention _ = zero
+Epistemic.Retention.Cert oneSymbolRetention _ _ = ⊤
+Epistemic.Retention.sound oneSymbolRetention _ = tt
+
+first≢second : (zero {1}) ≢ suc zero
+first≢second ()
+
+noOneSymbolRecovery : Epistemic.Recovery oneSymbolRetention -> ⊥
+noOneSymbolRecovery recovery =
+  Adapter.recoveryForbidsResidueCollision recovery first≢second refl refl
+
+-- Certificate-restricted decoding can be vacuous on an empty source. Both
+-- actual recovery interfaces demand a total decoder even off the image.
+emptyRetention : Epistemic.Retention ⊥ ⊤ ⊤
+Epistemic.Retention.observe emptyRetention ()
+Epistemic.Retention.retain emptyRetention ()
+Epistemic.Retention.Cert emptyRetention _ _ = ⊥
+Epistemic.Retention.sound emptyRetention ()
+
+emptyCertifiedDecoder : (y : ⊤) -> Epistemic.Echo emptyRetention y -> ⊥
+emptyCertifiedDecoder y (Epistemic.echo r ())
+
+emptyCertifiedRoundtrip : (x : ⊥) ->
+  emptyCertifiedDecoder (Epistemic.Retention.observe emptyRetention x)
+    (Epistemic.lower emptyRetention x) ≡ x
+emptyCertifiedRoundtrip ()
+
+noEmptyRecovery : Epistemic.Recovery emptyRetention -> ⊥
+noEmptyRecovery recovery = Epistemic.Recovery.recover recovery tt tt
+
+noEmptyExactRecovery :
+  Exact.ExactRecovery (Epistemic.Retention.observe emptyRetention)
+    (Epistemic.Retention.retain emptyRetention) -> ⊥
+noEmptyExactRecovery recovery =
+  noEmptyRecovery (Adapter.fromExactRecovery {C = emptyRetention} recovery)
+
+-- On-image equality alone does not identify total decoders: these two valid
+-- recoveries differ at an unreachable, uncertified visible/residue pair.
+offImageRetention : Epistemic.Retention Bool (Bool × Bool) ⊤
+Epistemic.Retention.observe offImageRetention b = b , false
+Epistemic.Retention.retain offImageRetention _ = tt
+Epistemic.Retention.Cert offImageRetention _ y = proj₂ y ≡ false
+Epistemic.Retention.sound offImageRetention _ = refl
+
+projectRecovery : Epistemic.Recovery offImageRetention
+Epistemic.Recovery.recover projectRecovery y _ = proj₁ y
+Epistemic.Recovery.roundtrip projectRecovery _ = refl
+
+private
+  flip : Bool -> Bool
+  flip false = true
+  flip true = false
+
+flipOffImageRecovery : Epistemic.Recovery offImageRetention
+Epistemic.Recovery.recover flipOffImageRecovery (b , false) _ = b
+Epistemic.Recovery.recover flipOffImageRecovery (b , true) _ = flip b
+Epistemic.Recovery.roundtrip flipOffImageRecovery _ = refl
+
+decodersAgreeOnImage : (b : Bool) ->
+  Epistemic.Recovery.recover projectRecovery (b , false) tt ≡
+  Epistemic.Recovery.recover flipOffImageRecovery (b , false) tt
+decodersAgreeOnImage b = refl
+
+decodersDisagreeOffImage :
+  Epistemic.Recovery.recover projectRecovery (false , true) tt ≢
+  Epistemic.Recovery.recover flipOffImageRecovery (false , true) tt
+decodersDisagreeOffImage ()
+
+offImageUncertified : Epistemic.Echo offImageRetention (false , true) -> ⊥
+offImageUncertified (Epistemic.echo r ())
+
+adapterPreservesOffImage :
+  Epistemic.Recovery.recover
+    (Adapter.fromExactRecovery {C = offImageRetention}
+      (Adapter.toExactRecovery flipOffImageRecovery)) (false , true) tt ≡ true
+adapterPreservesOffImage = refl

From 9869e8e8e39b381fb73d4afd91532f9db32edcb6 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 7 Nov 2026 01:45:31 +0000
Subject: [PATCH 2/3] Separate core and integration verification receipt scopes

---
 PROOF-STATUS.adoc | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index d6c4a6b..0901c3e 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -70,21 +70,30 @@ bash tests/check-rejections.sh
 bash tests/check-approval-seal-mutations.sh
 ----
 
-Every first-party Agda entry point is invoked with the canonical theory profile
+The core gate invokes its Agda entry points with the canonical theory profile
 `--safe --without-K --cubical-compatible --exact-split --no-sized-types
---no-guardedness`. Positive source checks use `--no-libraries --double-check
+--no-guardedness`. Core positive checks use `--no-libraries --double-check
 --ignore-interfaces -W error`. Agda 2.6.4.3's
 `UnsupportedIndexedMatch` category is disabled in that strict pass only because
 its 23 existing warning spans are checked separately against the exact manifest
 in `tests/check-proofs.sh`. A new, moved, or stale location fails the gate. The
 safe proofs check, but no Cubical transport-computation claim is made for those
 indexed eliminations, including `Kripke.Belief.believed`. The policy gate also
-compares all 23 source modules, 17 rejection fixtures, and the integration
-witness with exact path manifests; rejects additional `OPTIONS` pragmas, proof
+compares all 23 source modules, 17 rejection fixtures, and three integration
+witnesses with exact path manifests; rejects additional `OPTIONS` pragmas, proof
 escape hatches, and non-core imports; and verifies a generated negative
 control: `--safe` must reject a planted postulate with Agda's expected
 diagnostic and exit code.
 
+The separate integration command uses the existing
+`--safe --without-K --cubical-compatible` CLI profile. Each first-party
+integration module additionally declares `--exact-split --no-sized-types
+--no-guardedness` locally; those options are not imposed globally on the
+standard library. Its inherited `UnsupportedIndexedMatch` exemption is not
+bounded by the core's 23-span manifest. The expanded recovery closure has its
+own recorded unsuppressed diagnostic check; see
+link:docs/echo-recovery-adapter.adoc[the integration receipt and limitations].
+
 The most recent hosted receipt before adoption of the explicit
 `--cubical-compatible` CLI requirement is Proof Safety run
 https://github.com/hyperpolymath/epistemic-types/actions/runs/40445723481[40445723481]
@@ -125,9 +134,10 @@ validation of the security specification.
 
 == Local proof ledger
 
-All `PROVEN` rows below describe the Agda model only. They are covered by the
-canonical hosted receipt above; they do not thereby establish an external
-runtime or an unlisted mathematical correspondence.
+All `PROVEN` rows below describe the Agda model only. Each is covered by the
+receipt indicated for that row; the historical hosted runs above do not cover
+the later C-3 integration by implication. These results do not establish an
+external runtime or an unlisted mathematical correspondence.
 
 [cols="1,4,1,3",options="header"]
 |===

From 79b5668c0490eebda49a16d5f8f3eff7b8c9aab7 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 7 Nov 2026 02:27:32 +0000
Subject: [PATCH 3/3] Adopt corrected staleness fallback and qualify fibre
 collision claim

---
 .github/workflows/governance.yml |  2 +-
 PROOF-STATUS.adoc                |  3 ++-
 docs/echo-recovery-adapter.adoc  | 10 +++++++++-
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
index 4fefadb..50fa411 100644
--- a/.github/workflows/governance.yml
+++ b/.github/workflows/governance.yml
@@ -15,4 +15,4 @@ permissions:
 
 jobs:
   governance:
-    uses: metadatastician/standards/.github/workflows/governance-reusable.yml@ba640e9a57f22608710ffecdca282074eac55a0b
+    uses: metadatastician/standards/.github/workflows/governance-reusable.yml@ea2f4d8a886585ed442687ae63d4ad7493379ba4
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 0901c3e..d13809f 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -260,7 +260,8 @@ external runtime or an unlisted mathematical correspondence.
 | For a fixed `Retention` at `Set`, native `Recovery` and canonical
   `ExactRecovery` have inverse field-copy conversions, preserving the total
   decoder and its round-trip proof. Exact recovery transfers the finite
-  single-fibre alphabet bound and forbids residue collisions. Certificate,
+  single-fibre alphabet bound and forbids residue collisions within one
+  observation fibre. Certificate,
   empty-source and off-image controls delimit the contract.
 | PROVEN — local receipt 2026-11-07
 | `tests/integration/CanonicalRecovery.agda`, `RecoveryExamples.agda`;
diff --git a/docs/echo-recovery-adapter.adoc b/docs/echo-recovery-adapter.adoc
index 11dd88e..2fe617f 100644
--- a/docs/echo-recovery-adapter.adoc
+++ b/docs/echo-recovery-adapter.adoc
@@ -156,11 +156,19 @@ and scope above are the distributable receipt.
 
 The governance and scanner callers now use the published
 `metadatastician/standards` owner. Governance is pinned to
-`ba640e9a57f22608710ffecdca282074eac55a0b`; the scanner retains
+`ea2f4d8a886585ed442687ae63d4ad7493379ba4`; the scanner retains
 `75bd5994470661a099df562d6d5ad2fe744dbd66`. The scanner caller ID is
 `secret-scan`, matching the existing required `secret-scan / gitleaks`
 context. No branch rule or required check was removed.
 
+The governance revision includes standards PR #1421, which corrects the
+staleness checker's API fallback to the current repository owner. The
+owner-sensitive regression fails against the previous default and passes
+with the fix; all 32 staleness cases pass. An additional inherited-override
+control confirms that the default-owner test is isolated from its environment.
+The existing explicit-unverified policy for unavailable API checks is unchanged.
+All 85 reported checks completed without failures before that upstream merge.
+
 Official `github/gh-actions-lock` v0.4.1 regenerated the supported v0.0.3
 lockfile, and both `--verify-local` and online `--verify` passed. Its
 https://github.com/github/gh-actions-lock/blob/v0.4.1/README.md#limitations[documented limitation]