Bridge total recovery to Echo and restore required CI

.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

.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

.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@ea2f4d8a886585ed442687ae63d4ad7493379ba4

.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

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

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
@@ -56,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]
@@ -111,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"]
 |===
@@ -230,7 +254,18 @@ 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 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`;
+  link:docs/echo-recovery-adapter.adoc[assumptions and verification scope]
 |===
 
 == External pinned evidence, not local closure

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