diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml
index 3e10706..aba43b6 100644
--- a/.github/workflows/agda.yml
+++ b/.github/workflows/agda.yml
@@ -115,3 +115,35 @@ jobs:
         run: bash scripts/setup-agda.sh
       - name: Typecheck isolated full-Cubical profile
         run: agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --cubical -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda
+
+  # PROOF-POLICY section 2 recheck legs for EchoSearchExample: hand
+  # re-proofs in Rocq and in Lean core (no Mathlib). Each fails on any axiom.
+  # Toolchains are version-asserted (Lean archive checksum-pinned); the
+  # section 6 deviation is recorded in proofs/RECHECK-EchoSearchExample.adoc.
+  rocq-recheck:
+    name: Rocq recheck leg
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+      - name: Install version-asserted Rocq (Coq 8.18.0)
+        run: bash scripts/setup-recheck.sh rocq
+      - name: Check the Rocq leg (no axioms)
+        run: bash scripts/check-recheck.sh rocq
+
+  lean-recheck:
+    name: Lean recheck leg
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+      - name: Install checksum-pinned Lean 4.30.0
+        run: bash scripts/setup-recheck.sh lean
+      - name: Check the Lean leg (no axioms)
+        run: bash scripts/check-recheck.sh lean
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 7954516..edfb85d 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -27,6 +27,56 @@ below. The ordinal lane, including its order-type *Fidelity* scaffold, moved to
 https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
 on 2026-10-20.
 
+== Proof Witness Grades (PROOF-POLICY §8)
+
+Grades are computed per theorem from receipts and §2.2 records. They are
+never assigned to the repository as a whole.
+
+[cols="2,1,4",options="header"]
+|===
+|Theorem |PWG |Record
+
+|`EchoSearchExample` headlines (`search-double-6-decided`, `search-as-echo`, `search-as-cost`, `search-as-dec`, `search-as-feasible`)
+|`PWG-2ii`, no axioms
+|link:proofs/RECHECK-EchoSearchExample.adoc[`proofs/RECHECK-EchoSearchExample.adoc`].
+The Agda receipt is the cold check at `ccec4d7` (2026-11-09). The Rocq and
+Lean legs are re-proved and kernel-checked with no axioms. They are
+`RECONCILED` by owner acceptance of the recorded statement comparison
+(2026-11-09). `PWG-1` additionally needs current pinned CI receipts for
+every witness.
+|===
+
+Census (PROOF-POLICY §8.4), counted per theorem on 2026-11-09 over the 722
+headline pins in the `using` clauses of `proofs/agda/Smoke.agda` (the pins
+include some definitions as well as theorems): `PWG-1` 0, `PWG-2ii` 5,
+`PWG-2i` 0, `PWG-3` 0, `ungraded` 717. The five graded theorems are the
+`EchoSearchExample` headlines above; every other pin is `ungraded` because no
+per-theorem record exists for it yet.
+Agda results for the whole closure are dated checks, not grades.
+
+== Agda cold check (2026-11-09)
+
+At source commit `ccec4d79866e3e433ae2268d2f8b7899396cb34f`, with a clean
+tree and the CI toolchain from `scripts/setup-agda.sh` (Agda 2.7.0.1;
+release archive sha256
+`975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a`; stdlib
+`8326c74`; absolute-zero `f486c29`), these all exited 0:
+
+* the five static guards (kernel, experimental aggregate wiring and
+  controls, invocation lint, foundation guardrail);
+* the seven `--safe --without-K --cubical-compatible` roots, cold
+  (`--ignore-interfaces`): `All`, `Smoke`, `AuditSmoke`,
+  `characteristic/All`, `examples/All`, `experimental/echo-additive/All`
+  and `NarrowingSmoke`;
+* the `--safe --cubical` island.
+
+The only warnings were the known `UnsupportedIndexedMatch` ones (triage
+remains open; see below). The log is
+`docs/receipts/agda-cold-2026-11-09.log.gz`; the uncompressed log has
+sha256 `7f9de4d1f874a0f249eadeb3fc675be346f437cb28cb31fd3e6db1b635e54eb0`.
+This is a local run of a clean commit with the pinned toolchain. It is not
+a GitHub Actions receipt.
+
 == CI coverage audit (2026-11-01)
 
 * `experimental/echo-additive/` has a separate aggregate entrypoint, but
@@ -43,7 +93,7 @@ on 2026-10-20.
   other three) in warm and cold jobs under the standard profile. A local
   cold check now succeeds as detailed below; the changed workflow has not
   yet had a successful CI run. The exhibit remains outside the shipped
-  `All.agda` closure and is not a clean-commit Grade 3 receipt.
+  `All.agda` closure and is not a clean-commit `PWG-3` receipt.
 * On 2026-11-01 the local cold checks and static guards passed with Agda
   `2.7.0.1-cf6e2d9` and stdlib v2.3. The compiler is not the latest
   upstream stable; CI's compiler remains unpinned (#322). Full provenance,
@@ -110,7 +160,7 @@ with an unsolved hole was rejected (exit 42); it is not a theorem check.
 * Complete combined stdout/stderr is preserved in
   `docs/receipts/agda-local-2026-11-01.log.gz` (uncompressed SHA-256
   `617263834bee297a9f8e092c32e7cd9934af940f1e9fa7f9e19663b44cde99ad`).
-  No new clean-commit Grade 3 promotion is asserted on this basis.
+  No new clean-commit `PWG-3` promotion is asserted on this basis.
 
 In separate copied proof trees, replacing `fin-injective refl = refl` in
 experimental `Grade` with a hole caused its aggregate to exit 42, while
diff --git a/docs/proof-witness-audit.adoc b/docs/proof-witness-audit.adoc
index d8368b3..9f931b1 100644
--- a/docs/proof-witness-audit.adoc
+++ b/docs/proof-witness-audit.adoc
@@ -1,6 +1,21 @@
 // SPDX-License-Identifier: MPL-2.0
 = Proof-witness audit: Echo Types and Mathesis
 
+[NOTE]
+====
+*Superseded scale (2026-11-09).* This dated audit uses the Mathesis brief's
+grade definitions. PROOF-POLICY §8, by owner ruling of 2026-11-04, now
+governs, and corrects the brief in two places:
+
+* `PWG-2ii` means both the Rocq leg and the Lean leg count. A non-DTT
+  witness is the tag `+foundation-diverse`, not a condition of the grade
+  (§8.3).
+* Every grade carries the `PWG-` prefix.
+
+The audit text below is kept as written. Current per-theorem grades are
+in `PROOF-STATUS.adoc` §"Proof Witness Grades".
+====
+
 Audit date: 2026-11-01. Echo Types source base:
 `b0982c44f36133acd2d0e1d4e03cf031fff7a470` (working tree also has
 uncommitted CI/documentation edits). This is a source and receipt inspection,
diff --git a/docs/receipts/agda-cold-2026-11-09.log.gz b/docs/receipts/agda-cold-2026-11-09.log.gz
new file mode 100644
index 0000000..2f44430
Binary files /dev/null and b/docs/receipts/agda-cold-2026-11-09.log.gz differ
diff --git a/proofs/RECHECK-EchoSearchExample.adoc b/proofs/RECHECK-EchoSearchExample.adoc
new file mode 100644
index 0000000..c4c1bbd
--- /dev/null
+++ b/proofs/RECHECK-EchoSearchExample.adoc
@@ -0,0 +1,235 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= EchoSearchExample: Agda source, Rocq and Lean recheck legs
+:toc:
+
+This is the per-theorem record that PROOF-POLICY §2.2, §5 and §8.5 ask
+for (https://github.com/metadatastician/standards/blob/9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5/3-practice/PROOF-POLICY.adoc[standards@9bdf864]).
+It covers the headlines of `proofs/agda/EchoSearchExample.agda` (echo-types
+#353), a theory development: a worked axis-8 exhibit with no dependence on
+any one system's code. The Agda proof is the source of truth.
+
+[IMPORTANT]
+====
+*Grade: `PWG-2ii`, not rested on axioms.* The Agda source is `PROVEN`. Both
+recheck legs (Rocq and Lean) are kernel-checked as `PROVEN` with no axioms,
+and are `RECONCILED` (§2.2), so both legs count (§8.2).
+
+*How the legs were reconciled.* An agent wrote the statement comparison
+below. The owner accepted it on 2026-11-09 (echo-types#368), without a
+separate line-by-line review. Treat the comparison, the residual
+differences and the owner's acceptance together as the bridge record.
+
+`PWG-1` additionally needs current receipts from the pinned CI lanes
+(`check`, `cold-check`, `rocq-recheck`, `lean-recheck`) on the exact source
+commit for every witness. Those lanes run on pull requests, on pushes to
+`main` and `master`, and on manual dispatch; a push to any other branch with
+no open pull request produces no receipt.
+====
+
+== Ledger
+
+[cols="2,1,1,1,1,3",options="header"]
+|===
+|Leg |Route |§5 token |§2.2 state |Axioms |Receipt
+
+|Agda (source)
+|—
+|`PROVEN`
+|`AGDA-VERIFIED`
+|none
+|Cold check at echo-types `ccec4d79866e3e433ae2268d2f8b7899396cb34f`, 2026-11-09. See "Receipts".
+
+|Rocq
+|`re-proved`
+|`PROVEN`
+|`RECONCILED`
+|none (`Print Assumptions`: closed)
+|`proofs/rocq/EchoSearchExample.v`, Coq 8.18.0, 2026-11-09.
+
+|Lean 4
+|`re-proved`
+|`PROVEN`
+|`RECONCILED`
+|none (`#print axioms`: none)
+|`proofs/lean4/EchoSearchExample.lean`, Lean 4.30.0, 2026-11-09.
+|===
+
+Record (§8.5): `pwg: 2ii`, `foundation_diverse: false`. All three legs: `PROVEN`, with no axioms. Rocq and Lean: route `re-proved`, §2.2 `RECONCILED` (owner acceptance, 2026-11-09).
+
+*Why re-proved, not transported.* The policy prefers Dedukti transport
+(§2). No Agda→Dedukti→Rocq/Lean pipeline is set up in this repo. Separately,
+no released Lambdapi Lean exporter exists, so the Lean leg would be a
+re-proof in any case (§2). The theorems are small and concrete, so a hand
+re-proof against the same definitions is the direct route.
+
+== Statement correspondence
+
+The comparison was made by reading: each Rocq and Lean definition restates
+the Agda definition it mirrors, clause by clause.
+
+[cols="1,3,3,3",options="header"]
+|===
+|Headline |Agda |Rocq |Lean 4
+
+|`double`
+|`double zero = zero`; `double (suc n) = suc (suc (double n))`
+|same two clauses on `nat`
+|`double 0 = 0`; `double (n+1) = double n + 2` (= `succ (succ (double n))` by `Nat.add` unfolding)
+
+|`search-double-6`
+|`EchoS countUp double 6 4`, witness `(3 , s≤s⁴ z≤n , refl)`
+|`EchoS countUp double 6 4`, `existT _ 3 (le_n 4, eq_refl)`
+|`EchoS countUp double 6 4`, `⟨3, by decide, rfl⟩`
+
+|`search-double-6-decided`
+|`bounded-search-is-decidable _≟_ countUp double 6 4 ≡ yes search-double-6`, by `refl`
+|`bounded_search_is_decidable nat_eq_dec countUp double 6 4 = yes search_double_6`, by `reflexivity`
+|`boundedSearchIsDecidable Nat.decEq countUp double 6 4 = Dec.yes searchDouble6`, by `rfl`
+
+|`search-as-echo`
+|`Echo double 6`
+|`Echo double 6`
+|`Echo double 6`
+
+|`search-as-cost`
+|`EchoC search-steps 4 double 6` (`Cost stepCostAlgebra`)
+|`EchoC search_steps 4 double 6`
+|`EchoC searchSteps 4 double 6`
+
+|`search-as-dec`
+|`EchoDec double 6`
+|`EchoDec double 6`
+|`EchoDec double 6`
+
+|`search-as-feasible`
+|`CEcho feasible double 6`, by `degrade-access free≤feasible`
+|`CEcho feasible double 6`, by `degrade_access free_feasible`
+|`CEcho .feasible double 6`, by `degradeAccess .freeFeasible`
+|===
+
+The definitions behind them:
+
+* `Echo f y = Σ A (λ x → f x ≡ y)` (`Echo.agda`). Rocq writes it as
+  `{x : A & f x = y}` (`sigT`), Lean as `(x : A) ×' (f x = y)` (`PSigma`).
+* `EchoS enum f y n = Σ ℕ (λ k → (k < n) × (f (enum k) ≡ y))`
+  (`EchoSearch.agda`). Both targets use a proof-relevant Σ over `k` with the
+  same two components.
+* `bounded-search-is-decidable` recurses structurally on the budget, and its
+  successor step tests the new top index `n` first, then recurses. The
+  targets recurse the same way and in the same order, so the `decided`
+  equation computes to the same witness. The Agda comment notes this is one
+  comparison, not an ascending walk.
+* `EchoC` at `stepCostAlgebra = (ℕ, 0, _+_, _≤_, …)`: `Cost stepCostAlgebra`
+  unfolds to `Σ A (λ x → (f x ≡ y) × (cost x ≤ c))`. The targets restate
+  that instance directly, not the generic `CostAlgebra` record. The generic
+  record and its laws are not part of these headlines.
+* `search-steps = suc`; `count-up-search-to-cost` re-pairs, because `k < n` is
+  `suc k ≤ n` definitionally. This holds in all three systems: stdlib `_<_`;
+  Rocq `lt n m := S n <= m`; Lean `Nat.lt n m := Nat.le (n+1) m`.
+* `EchoDec f y = Dec (Echo f y)`; `search-to-dec s = yes (echo-search-forget s)`.
+* `CEcho`, `_≤a_` (15 Hasse pairs) and `degrade-access` are restated in full,
+  case for case.
+
+== Residual differences and assumptions
+
+These do not change what the headlines state about this example, but they
+are differences between the systems and are listed as the policy requires.
+
+. *Identity type.* Agda's `_≡_` is used under `--without-K`. Rocq's `eq` lives
+  in `Prop`, with no UIP axiom assumed. Lean's `Eq` lives in `Prop` with
+  definitional proof irrelevance, so K holds in Lean. Every proof here is a
+  closed computation (`refl` / `reflexivity` / `rfl`) or a re-pairing, so
+  none of them uses K. The Lean leg is still checked in a strictly stronger
+  theory.
+. *Order and decision types.* Agda's `_<_` is a data type in `Set`; in Rocq
+  and Lean it is a `Prop`. Agda's stdlib `Dec` is a record (`does`/`proof`);
+  the targets use a local `yes`/`no` inductive with the same two cases.
+  Decidable equality on ℕ is stdlib `_≟_` in Agda, a `decide equality` term
+  in Rocq, and `Nat.decEq` in Lean.
+. *Universes.* Agda is universe-polymorphic with `Lift` padding in `CEcho`.
+  Rocq uses `Type` with template polymorphism; Lean uses `Type u` with
+  `PUnit`. Both targets use the unit type where Agda uses `Lift (a ⊔ b) ⊤`.
+. *Scope.* The `CostAlgebra` laws (`≤-refl`, `≤-trans`, `+-identityˡ`,
+  `+-mono-≤`) are not restated, because no headline in this module depends
+  on them. They are Agda-only facts for this theorem.
+
+== Receipts
+
+*Agda (PWG-3 receipt).*
+
+* Source: echo-types `ccec4d79866e3e433ae2268d2f8b7899396cb34f`, clean tree.
+  `proofs/agda/EchoSearchExample.agda` sha256
+  `b73a9bb1fab531531f2442ea5f23cda74bd933e6e80e12e84986aa8ef716be33`.
+* Checker: Agda 2.7.0.1 from `scripts/setup-agda.sh`, release archive sha256
+  `975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a`.
+  Pins: stdlib `8326c7475af1fa456ca04a0203c168d5d7ff842b`, absolute-zero
+  `f486c29903434589117fa0662c6f29b0f17d1d5f`.
+* Invocation: `agda --no-libraries -i $AGDA_STDLIB -i $ABSOLUTE_ZERO_AGDA
+  --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda
+  proofs/agda/All.agda`. That is the §2.1 profile, cold; `All` imports
+  `EchoSearchExample`.
+* The same run also checked `Smoke`, `AuditSmoke`, `characteristic/All`,
+  `examples/All`, `experimental/echo-additive/All`, `NarrowingSmoke`, the
+  `--safe --cubical` island and the five static guards. All exited 0.
+* Import cone (§1.1): first-party `EchoSearchExample`, `Echo`, `EchoCost`,
+  `EchoDecidable`, `EchoAccess`, `EchoSearch`, plus the pinned stdlib.
+  Compiled under `--safe`, which refuses `postulate`. A comment-aware scan of
+  the first-party cone finds zero postulates. Postulate count: 0.
+* Warnings: `UnsupportedIndexedMatch` (Cubical computation on transports)
+  appears in the cone, including `EchoSearch.agda` lines 192–204 (the
+  decider) and `EchoAccess.agda`. These are the known warnings triaged in
+  `PROOF-STATUS.adoc`. They are not errors and not postulates.
+* Log: `docs/receipts/agda-cold-2026-11-09.log.gz`. The uncompressed log has
+  sha256 `7f9de4d1f874a0f249eadeb3fc675be346f437cb28cb31fd3e6db1b635e54eb0`.
+
+*Rocq leg.* Source: `hyperpolymath/echo-types` at commit
+`7e9b5f446a50cc6e78faa815e8a5efe7092cdb0b`. `proofs/rocq/EchoSearchExample.v` sha256
+`2a016469af61f11daf2df82ca5ecae6d6ec4b0a2d2a6406b18fef2b516836068`, checked
+with Coq 8.18.0 (OCaml 4.14.1; Ubuntu `coq 8.18.0+dfsg-1build2`). Invocation:
+`bash scripts/check-recheck.sh rocq`, which runs `coqc -q` and requires every
+`Print Assumptions` to report "Closed under the global context" and requires
+one for each of the five headlines by name. Result: six checks (the five
+headlines and `search_as_cost_witness`), all closed, no axioms.
+
+*Lean leg.* Source: `hyperpolymath/echo-types` at commit
+`7e9b5f446a50cc6e78faa815e8a5efe7092cdb0b`. `proofs/lean4/EchoSearchExample.lean` sha256
+`fdb271bfbaa9b1feeee99fce767cf269c8dbaa3da374d870300413ffa4068d94`, checked
+with Lean 4.30.0 (commit `d024af099ca4bf2c86f649261ebf59565dc8c622`; release
+archive sha256 `4dad74141c2c119ca1aa626656be83b8e14238afba97271fd7bf1eb3f081b319`).
+Core only, with no imports and no Mathlib. Invocation:
+`bash scripts/check-recheck.sh lean`, which requires no error, warning or
+`sorry`, every `#print axioms` to report none, and an axiom-free result for
+each of the five headlines by name. Result: six checks (the five headlines
+and `searchAsCostWitness`), no axioms.
+
+*Sensitivity.* Planted errors make each leg fail: `double` changed to add one,
+and the decided budget changed from 4 to 3, which leaves the witness out of
+reach. Each mutant exits non-zero in both Rocq and Lean.
+
+*CI.* The `rocq-recheck` and `lean-recheck` jobs in `.github/workflows/agda.yml`
+run the same scripts on every push and pull request. These are the
+per-commit receipts that `PWG-1` will need.
+
+== Toolchain deviation (§6)
+
+* Legs affected: Rocq and Lean, for this theorem.
+* Tools: Coq 8.18.0 from the Ubuntu 24.04 archive (`coq 8.18.0+dfsg-1build2`);
+  Lean 4.30.0 from the upstream release archive at the sha256 above.
+  `scripts/setup-recheck.sh` asserts both versions and fails on a mismatch.
+* Why not Guix or the container: the repo's Agda lane already installs from a
+  checksum-pinned release archive (`scripts/setup-agda.sh`). These legs follow
+  the same pattern, so that every prover in CI comes from one method, until
+  the Guix manifest carries pinned Rocq and Lean.
+* State: `open`.
+
+== Revalidation triggers
+
+Re-run all three legs, and recompute the grade from the receipts (§8.4.4),
+if any of the following changes:
+
+* the Agda sources in the cone;
+* either target file;
+* the Agda, stdlib, absolute-zero, Coq or Lean pin.
+
+A failing leg drops the grade.
diff --git a/proofs/lean4/EchoSearchExample.lean b/proofs/lean4/EchoSearchExample.lean
new file mode 100644
index 0000000..82855e8
--- /dev/null
+++ b/proofs/lean4/EchoSearchExample.lean
@@ -0,0 +1,177 @@
+/-
+SPDX-License-Identifier: MPL-2.0
+SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+Lean 4 recheck leg (re-proved) of proofs/agda/EchoSearchExample.agda.
+
+PROOF-POLICY section 2: every Agda theory proof is rechecked in Rocq and
+Lean, with no Mathlib.  This file is a hand re-proof in Lean core: no
+imports beyond the prelude, no `sorry`, no new axioms.  Each definition
+restates the Agda definition it mirrors, and each theorem the Agda headline
+of the same name.  The statement correspondence and the residual
+differences are recorded in proofs/RECHECK-EchoSearchExample.adoc.  The
+closing `#print axioms` commands must report no axioms.
+-/
+
+namespace EchoSearchExample
+
+universe u v
+
+/-! Echo.agda: `Echo f y := Σ (x : A), f x ≡ y` -/
+def Echo {A : Type u} {B : Type v} (f : A → B) (y : B) : Type u :=
+  (x : A) ×' (f x = y)
+
+/-! EchoSearch.agda -/
+def SearchStrategy (A : Type u) : Type u := Nat → A
+
+/-- `EchoS enum f y n = Σ k, (k < n) × (f (enum k) ≡ y)` -/
+def EchoS {A : Type u} {B : Type v}
+    (enum : SearchStrategy A) (f : A → B) (y : B) (n : Nat) : Type :=
+  (k : Nat) ×' (k < n) ×' (f (enum k) = y)
+
+def echoSearchForget {A : Type u} {B : Type v}
+    {enum : SearchStrategy A} {f : A → B} {y : B} {n : Nat}
+    (s : EchoS enum f y n) : Echo f y :=
+  ⟨enum s.1, s.2.2⟩
+
+/-- Agda's `Dec`, with `yes` / `no`. -/
+inductive Dec (P : Sort u) : Sort (max 1 u) where
+  | yes : P → Dec P
+  | no : (P → False) → Dec P
+
+theorem echoSearchBoundZero {A : Type u} {B : Type v}
+    (enum : SearchStrategy A) (f : A → B) (y : B) :
+    EchoS enum f y 0 → False :=
+  fun s => Nat.not_lt_zero _ s.2.1
+
+theorem ltSuccInv {k n : Nat} (h : k < n + 1) : k < n ∨ k = n :=
+  Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h)
+
+/-- `bounded-search-is-decidable`: structural recursion on the budget; the
+successor step tests the new top index `n` FIRST, then recurses, as the
+Agda procedure does. -/
+def boundedSearchIsDecidable {A : Type u} {B : Type v}
+    (deq : (x y : B) → Decidable (x = y))
+    (enum : SearchStrategy A) (f : A → B) (y : B) :
+    (n : Nat) → Dec (EchoS enum f y n)
+  | 0 => Dec.no (echoSearchBoundZero enum f y)
+  | m + 1 =>
+    match deq (f (enum m)) y with
+    | isTrue e => Dec.yes ⟨m, Nat.lt_succ_self m, e⟩
+    | isFalse ne =>
+      match boundedSearchIsDecidable deq enum f y m with
+      | Dec.yes s => Dec.yes ⟨s.1, Nat.lt_succ_of_lt s.2.1, s.2.2⟩
+      | Dec.no below =>
+        Dec.no fun s =>
+          match ltSuccInv s.2.1 with
+          | Or.inl klt => below ⟨s.1, klt, s.2.2⟩
+          | Or.inr keq => ne (keq ▸ s.2.2)
+
+/-! EchoSearchExample.agda -/
+
+def double : Nat → Nat
+  | 0 => 0
+  | n + 1 => double n + 2
+
+def countUp : SearchStrategy Nat := fun k => k
+
+/-- The hit is at step `3 < 4`, where `double 3 = 6` by computation. -/
+def searchDouble6 : EchoS countUp double 6 4 :=
+  ⟨3, by decide, rfl⟩
+
+/-- The decider, run on this instance, computes to `yes` on exactly that
+witness. -/
+theorem searchDouble6Decided :
+    boundedSearchIsDecidable (fun a b => Nat.decEq a b) countUp double 6 4
+      = Dec.yes searchDouble6 := by
+  rfl
+
+/-- `EchoCost.Cost` at the step-count algebra `(ℕ, 0, +, ≤)`: the instance
+unfolds to `Σ x, (f x ≡ y) × (cost x ≤ c)`. -/
+def EchoC {A : Type u} {B : Type v}
+    (cost : A → Nat) (c : Nat) (f : A → B) (y : B) : Type u :=
+  (x : A) ×' (f x = y) ×' (cost x ≤ c)
+
+def searchSteps : Nat → Nat := Nat.succ
+
+/-- `k < n` is `k + 1 ≤ n` on the nose, so the bridge is a re-pairing. -/
+def countUpSearchToCost {B : Type v} {f : Nat → B} {y : B} {n : Nat}
+    (s : EchoS countUp f y n) : EchoC searchSteps n f y :=
+  ⟨s.1, s.2.2, s.2.1⟩
+
+/-- EchoDecidable: `EchoDec f y := Dec (Echo f y)`. -/
+def EchoDec {A : Type u} {B : Type v} (f : A → B) (y : B) : Type u :=
+  Dec (Echo f y)
+
+def searchToDec {A : Type u} {B : Type v}
+    {enum : SearchStrategy A} {f : A → B} {y : B} {n : Nat}
+    (s : EchoS enum f y n) : EchoDec f y :=
+  Dec.yes (echoSearchForget s)
+
+/-! EchoAccess: the five grades, the 15-pair Hasse order, `CEcho` and
+`degrade-access`, restated in full. -/
+
+inductive Access where
+  | free | decidable | enum | feasible | infeasible
+
+inductive LeA : Access → Access → Type where
+  | freeFree : LeA .free .free
+  | freeDecidable : LeA .free .decidable
+  | freeEnum : LeA .free .enum
+  | freeFeasible : LeA .free .feasible
+  | freeInfeasible : LeA .free .infeasible
+  | decidableDecidable : LeA .decidable .decidable
+  | decidableEnum : LeA .decidable .enum
+  | decidableFeasible : LeA .decidable .feasible
+  | decidableInfeasible : LeA .decidable .infeasible
+  | enumEnum : LeA .enum .enum
+  | enumFeasible : LeA .enum .feasible
+  | enumInfeasible : LeA .enum .infeasible
+  | feasibleFeasible : LeA .feasible .feasible
+  | feasibleInfeasible : LeA .feasible .infeasible
+  | infeasibleInfeasible : LeA .infeasible .infeasible
+
+def CEcho {A : Type u} {B : Type v} : Access → (A → B) → B → Type u
+  | .free, f, y => Echo f y
+  | .decidable, f, y => EchoDec f y
+  | .enum, _, _ => PUnit
+  | .feasible, _, _ => PUnit
+  | .infeasible, _, _ => PUnit
+
+def degradeAccess {A : Type u} {B : Type v} {f : A → B} {y : B} :
+    {c1 c2 : Access} → LeA c1 c2 → CEcho c1 f y → CEcho c2 f y
+  | _, _, .freeFree, e => e
+  | _, _, .freeDecidable, e => Dec.yes e
+  | _, _, .freeEnum, _ => PUnit.unit
+  | _, _, .freeFeasible, _ => PUnit.unit
+  | _, _, .freeInfeasible, _ => PUnit.unit
+  | _, _, .decidableDecidable, d => d
+  | _, _, .decidableEnum, _ => PUnit.unit
+  | _, _, .decidableFeasible, _ => PUnit.unit
+  | _, _, .decidableInfeasible, _ => PUnit.unit
+  | _, _, .enumEnum, e => e
+  | _, _, .enumFeasible, _ => PUnit.unit
+  | _, _, .enumInfeasible, _ => PUnit.unit
+  | _, _, .feasibleFeasible, e => e
+  | _, _, .feasibleInfeasible, _ => PUnit.unit
+  | _, _, .infeasibleInfeasible, e => e
+
+/-! The bridges fired on the concrete witness. -/
+def searchAsEcho : Echo double 6 := echoSearchForget searchDouble6
+def searchAsCost : EchoC searchSteps 4 double 6 := countUpSearchToCost searchDouble6
+def searchAsDec : EchoDec double 6 := searchToDec searchDouble6
+def searchAsFeasible : CEcho .feasible double 6 :=
+  degradeAccess LeA.freeFeasible searchAsEcho
+
+/-- Computational sanity: the bridges carry the witness `3`. -/
+theorem searchAsEchoWitness : searchAsEcho.1 = 3 := rfl
+theorem searchAsCostWitness : searchAsCost.1 = 3 := rfl
+
+end EchoSearchExample
+
+#print axioms EchoSearchExample.searchDouble6Decided
+#print axioms EchoSearchExample.searchAsEcho
+#print axioms EchoSearchExample.searchAsCost
+#print axioms EchoSearchExample.searchAsDec
+#print axioms EchoSearchExample.searchAsFeasible
+#print axioms EchoSearchExample.searchAsCostWitness
diff --git a/proofs/rocq/EchoSearchExample.v b/proofs/rocq/EchoSearchExample.v
new file mode 100644
index 0000000..f6c4669
--- /dev/null
+++ b/proofs/rocq/EchoSearchExample.v
@@ -0,0 +1,206 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
+
+(* Rocq recheck leg (re-proved) of proofs/agda/EchoSearchExample.agda.
+
+   PROOF-POLICY section 2: every Agda theory proof is rechecked in Rocq and
+   Lean.  This file is a hand re-proof, not a Dedukti transport.  Each
+   definition restates the Agda definition it mirrors, and each theorem
+   restates the Agda headline of the same name.  The statement-by-statement
+   correspondence, and the residual differences between the systems, are
+   recorded in proofs/RECHECK-EchoSearchExample.adoc.
+
+   Core library only (Init + the prelude); no Require, no axioms.  The
+   closing `Print Assumptions` commands must report "Closed under the
+   global context". *)
+
+(* ---------------------------------------------------------------- *)
+(* Echo.agda: Echo f y := Sigma (x : A), f x = y                     *)
+(* ---------------------------------------------------------------- *)
+
+Definition Echo {A B : Type} (f : A -> B) (y : B) : Type :=
+  { x : A & f x = y }.
+
+(* ---------------------------------------------------------------- *)
+(* EchoSearch.agda                                                   *)
+(* ---------------------------------------------------------------- *)
+
+Definition SearchStrategy (A : Type) : Type := nat -> A.
+
+(* EchoS enum f y n = Sigma k, (k < n) x (f (enum k) = y) *)
+Definition EchoS {A B : Type}
+  (enum : SearchStrategy A) (f : A -> B) (y : B) (n : nat) : Type :=
+  { k : nat & ((k < n) * (f (enum k) = y))%type }.
+
+Definition echo_search_forget {A B : Type}
+  {enum : SearchStrategy A} {f : A -> B} {y : B} {n : nat}
+  (s : EchoS enum f y n) : Echo f y :=
+  match s with existT _ k (_, eq) => existT _ (enum k) eq end.
+
+(* Agda's Dec, with yes / no. *)
+Inductive Dec (P : Type) : Type :=
+| yes : P -> Dec P
+| no  : (P -> False) -> Dec P.
+Arguments yes {P} _.
+Arguments no  {P} _.
+
+(* Decidable equality on nat, transparent so that the decider computes. *)
+Definition nat_eq_dec : forall x y : nat, {x = y} + {x <> y}.
+Proof. decide equality. Defined.
+
+(* An index below `S n` is either below `n` or is `n` itself. *)
+Lemma lt_succ_inv : forall k n, k < S n -> (k < n) + (k = n).
+Proof.
+  intros k n H. unfold lt in H. apply le_S_n in H.
+  destruct (nat_eq_dec k n) as [e | ne]; [ right; exact e | left ].
+  revert ne. induction H as [| m Hm IH]; intro ne.
+  - exfalso. apply ne. reflexivity.
+  - apply le_n_S. exact Hm.
+Qed.
+
+Lemma echo_search_bound_zero {A B : Type}
+  (enum : SearchStrategy A) (f : A -> B) (y : B) :
+  EchoS enum f y 0 -> False.
+Proof. intros [k [H _]]. inversion H. Qed.
+
+(* bounded-search-is-decidable: structural recursion on the budget; the
+   successor step tests the new top index `n` FIRST, then recurses, as the
+   Agda procedure does.  Defined (transparent) so it computes. *)
+Fixpoint bounded_search_is_decidable {A B : Type}
+  (deq : forall x y : B, {x = y} + {x <> y})
+  (enum : SearchStrategy A) (f : A -> B) (y : B) (n : nat)
+  : Dec (EchoS enum f y n) :=
+  match n with
+  | O => no (echo_search_bound_zero enum f y)
+  | S m =>
+      match deq (f (enum m)) y with
+      | left e => yes (existT _ m (le_n (S m), e))
+      | right ne =>
+          match bounded_search_is_decidable deq enum f y m with
+          | yes (existT _ k (klt, ek)) => yes (existT _ k (le_S _ _ klt, ek))
+          | no below =>
+              no (fun s =>
+                    match s with
+                    | existT _ k (klt, ek) =>
+                        match lt_succ_inv k m klt with
+                        | inl kltm => below (existT _ k (kltm, ek))
+                        | inr keq =>
+                            ne (eq_rect k (fun j => f (enum j) = y) ek m keq)
+                        end
+                    end)
+          end
+      end
+  end.
+
+(* ---------------------------------------------------------------- *)
+(* EchoSearchExample.agda                                            *)
+(* ---------------------------------------------------------------- *)
+
+Fixpoint double (n : nat) : nat :=
+  match n with
+  | O => O
+  | S m => S (S (double m))
+  end.
+
+Definition countUp : SearchStrategy nat := fun k => k.
+
+(* The hit is at step 3 < 4, where double 3 = 6 by computation. *)
+Definition search_double_6 : EchoS countUp double 6 4 :=
+  existT _ 3 (le_n 4, eq_refl).
+
+(* The decider, run on this instance, computes to `yes` on exactly that
+   witness. *)
+Theorem search_double_6_decided :
+  bounded_search_is_decidable nat_eq_dec countUp double 6 4
+  = yes search_double_6.
+Proof. reflexivity. Qed.
+
+(* EchoCost.Cost at the step-count algebra (N, 0, +, <=): the instance
+   unfolds to Sigma x, (f x = y) x (cost x <= c). *)
+Definition EchoC {A B : Type}
+  (cost : A -> nat) (c : nat) (f : A -> B) (y : B) : Type :=
+  { x : A & ((f x = y) * (cost x <= c))%type }.
+
+Definition search_steps : nat -> nat := S.
+
+(* `k < n` is `S k <= n` on the nose, so the bridge is a re-pairing. *)
+Definition count_up_search_to_cost {B : Type} {f : nat -> B} {y : B} {n : nat}
+  (s : EchoS countUp f y n) : EchoC search_steps n f y :=
+  match s with existT _ k (klt, eq) => existT _ k (eq, klt) end.
+
+(* EchoDecidable: EchoDec f y := Dec (Echo f y). *)
+Definition EchoDec {A B : Type} (f : A -> B) (y : B) : Type := Dec (Echo f y).
+
+Definition search_to_dec {A B : Type}
+  {enum : SearchStrategy A} {f : A -> B} {y : B} {n : nat}
+  (s : EchoS enum f y n) : EchoDec f y :=
+  yes (echo_search_forget s).
+
+(* EchoAccess: the five access grades, the 15-pair Hasse order, CEcho and
+   degrade-access, restated in full. *)
+Inductive Access : Type := free | decidable | enum_ | feasible | infeasible.
+
+Inductive le_a : Access -> Access -> Type :=
+| free_free : le_a free free
+| free_decidable : le_a free decidable
+| free_enum : le_a free enum_
+| free_feasible : le_a free feasible
+| free_infeasible : le_a free infeasible
+| decidable_decidable : le_a decidable decidable
+| decidable_enum : le_a decidable enum_
+| decidable_feasible : le_a decidable feasible
+| decidable_infeasible : le_a decidable infeasible
+| enum_enum : le_a enum_ enum_
+| enum_feasible : le_a enum_ feasible
+| enum_infeasible : le_a enum_ infeasible
+| feasible_feasible : le_a feasible feasible
+| feasible_infeasible : le_a feasible infeasible
+| infeasible_infeasible : le_a infeasible infeasible.
+
+Definition CEcho {A B : Type} (c : Access) (f : A -> B) (y : B) : Type :=
+  match c with
+  | free => Echo f y
+  | decidable => EchoDec f y
+  | enum_ | feasible | infeasible => unit
+  end.
+
+Definition degrade_access {A B : Type} {f : A -> B} {y : B}
+  {c1 c2 : Access} (p : le_a c1 c2) : CEcho c1 f y -> CEcho c2 f y :=
+  match p in le_a c1 c2 return CEcho c1 f y -> CEcho c2 f y with
+  | free_free => fun e => e
+  | free_decidable => fun e => yes e
+  | free_enum => fun _ => tt
+  | free_feasible => fun _ => tt
+  | free_infeasible => fun _ => tt
+  | decidable_decidable => fun d => d
+  | decidable_enum => fun _ => tt
+  | decidable_feasible => fun _ => tt
+  | decidable_infeasible => fun _ => tt
+  | enum_enum => fun e => e
+  | enum_feasible => fun _ => tt
+  | enum_infeasible => fun _ => tt
+  | feasible_feasible => fun e => e
+  | feasible_infeasible => fun _ => tt
+  | infeasible_infeasible => fun e => e
+  end.
+
+(* The bridges fired on the concrete witness. *)
+Definition search_as_echo : Echo double 6 := echo_search_forget search_double_6.
+Definition search_as_cost : EchoC search_steps 4 double 6 :=
+  count_up_search_to_cost search_double_6.
+Definition search_as_dec : EchoDec double 6 := search_to_dec search_double_6.
+Definition search_as_feasible : CEcho feasible double 6 :=
+  degrade_access free_feasible search_as_echo.
+
+(* Computational sanity: the bridges carry the witness 3. *)
+Theorem search_as_echo_witness : projT1 search_as_echo = 3.
+Proof. reflexivity. Qed.
+Theorem search_as_cost_witness : projT1 search_as_cost = 3.
+Proof. reflexivity. Qed.
+
+Print Assumptions search_double_6_decided.
+Print Assumptions search_as_echo.
+Print Assumptions search_as_cost.
+Print Assumptions search_as_dec.
+Print Assumptions search_as_feasible.
+Print Assumptions search_as_cost_witness.
diff --git a/scripts/check-recheck.sh b/scripts/check-recheck.sh
new file mode 100755
index 0000000..ab715ab
--- /dev/null
+++ b/scripts/check-recheck.sh
@@ -0,0 +1,75 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Check the Rocq and Lean recheck legs and fail on any axiom.
+# Usage: scripts/check-recheck.sh [rocq|lean|all]. Needs coqc on PATH and
+# LEAN set to the lean binary (scripts/setup-recheck.sh provides both).
+# Save stdout and stderr if a receipt is needed.
+set -euo pipefail
+cd "$(dirname "$0")/.."
+want="${1:-all}"
+case "$want" in
+  all|rocq|lean) ;;
+  *) printf 'usage: %s [rocq|lean|all]\n' "$0" >&2; exit 2 ;;
+esac
+printf 'Source commit: %s\n' "$(git rev-parse HEAD)"
+
+# The five headlines of the PWG record (PROOF-STATUS.adoc). Each must have its
+# own assumption check: a check on a supporting lemma never stands in for one.
+rocq_headlines=(search_double_6_decided search_as_echo search_as_cost search_as_dec search_as_feasible)
+lean_headlines=(searchDouble6Decided searchAsEcho searchAsCost searchAsDec searchAsFeasible)
+
+if [ "$want" = all ] || [ "$want" = rocq ]; then
+  v=proofs/rocq/EchoSearchExample.v
+  coqc --version
+  if ! out="$(cd proofs/rocq && coqc -q EchoSearchExample.v 2>&1)"; then
+    printf '%s\n' "$out"
+    printf 'Rocq leg: coqc failed\n' >&2
+    exit 1
+  fi
+  printf '%s\n' "$out"
+  for h in "${rocq_headlines[@]}"; do
+    if ! grep -qx "Print Assumptions $h\." "$v"; then
+      printf 'Rocq leg: no Print Assumptions for headline %s\n' "$h" >&2
+      exit 1
+    fi
+  done
+  # Every Print Assumptions must close; any axiom fails the leg.
+  n_closed="$(printf '%s\n' "$out" | grep -c '^Closed under the global context$' || true)"
+  n_print="$(grep -c '^Print Assumptions' "$v")"
+  if [ "$n_closed" -ne "$n_print" ]; then
+    printf 'Rocq leg: %s of %s Print Assumptions closed\n' "$n_closed" "$n_print" >&2
+    exit 1
+  fi
+  rm -f proofs/rocq/*.vo proofs/rocq/*.vok proofs/rocq/*.vos proofs/rocq/*.glob proofs/rocq/.*.aux
+  printf 'Rocq leg: OK (%s headlines and %s checks in all, no axioms)\n' \
+    "${#rocq_headlines[@]}" "$n_print"
+fi
+
+if [ "$want" = all ] || [ "$want" = lean ]; then
+  lean="${LEAN:?set LEAN to the lean binary}"
+  "$lean" --version
+  if ! out="$("$lean" proofs/lean4/EchoSearchExample.lean 2>&1)"; then
+    printf '%s\n' "$out"
+    printf 'Lean leg: lean failed\n' >&2
+    exit 1
+  fi
+  printf '%s\n' "$out"
+  if printf '%s\n' "$out" | grep -qE 'error|warning|sorry|depends on axioms'; then
+    printf 'Lean leg: error, warning, sorry or axiom reported\n' >&2
+    exit 1
+  fi
+  for h in "${lean_headlines[@]}"; do
+    if ! printf '%s\n' "$out" | grep -qF "'EchoSearchExample.$h' does not depend on any axioms"; then
+      printf 'Lean leg: headline %s has no axiom-free #print axioms result\n' "$h" >&2
+      exit 1
+    fi
+  done
+  n_free="$(printf '%s\n' "$out" | grep -c 'does not depend on any axioms' || true)"
+  n_print="$(grep -c '^#print axioms' proofs/lean4/EchoSearchExample.lean)"
+  if [ "$n_free" -ne "$n_print" ]; then
+    printf 'Lean leg: %s of %s #print axioms axiom-free\n' "$n_free" "$n_print" >&2
+    exit 1
+  fi
+  printf 'Lean leg: OK (%s headlines and %s checks in all, no axioms)\n' \
+    "${#lean_headlines[@]}" "$n_print"
+fi
diff --git a/scripts/setup-recheck.sh b/scripts/setup-recheck.sh
new file mode 100755
index 0000000..97f96e4
--- /dev/null
+++ b/scripts/setup-recheck.sh
@@ -0,0 +1,62 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Linux x86-64 toolchain for the Rocq and Lean recheck legs
+# (PROOF-POLICY section 2). Versions are asserted; a mismatch fails before
+# any proof is checked.
+#
+# Deviation (PROOF-POLICY section 6): these provers are installed from the
+# Ubuntu archive (Rocq/Coq) and from the upstream Lean release archive at a
+# checked-in SHA-256, not from the repo's Guix manifest or container. The
+# Agda lane makes the same choice in scripts/setup-agda.sh. The record is in
+# proofs/RECHECK-EchoSearchExample.adoc, "Toolchain deviation". State: open.
+set -euo pipefail
+
+COQ_DEB_VERSION=8.18.0+dfsg-1build2
+COQ_VERSION=8.18.0
+LEAN_VERSION=4.30.0
+LEAN_SHA256=4dad74141c2c119ca1aa626656be83b8e14238afba97271fd7bf1eb3f081b319
+
+test "$(uname -s)-$(uname -m)" = Linux-x86_64
+tool_dir="${RECHECK_TOOLS_DIR:-${RUNNER_TEMP:?RUNNER_TEMP or RECHECK_TOOLS_DIR is required}/echo-recheck}"
+mkdir -p "$tool_dir"
+tool_dir="$(cd "$tool_dir" && pwd)"
+
+want="${1:-all}"
+case "$want" in
+  all|rocq|lean) ;;
+  *) printf 'usage: %s [rocq|lean|all]\n' "$0" >&2; exit 2 ;;
+esac
+
+if [ "$want" = all ] || [ "$want" = rocq ]; then
+  if ! dpkg-query -W -f='${Version}' coq 2>/dev/null | grep -qx "$COQ_DEB_VERSION"; then
+    sudo_cmd=""
+    [ "$(id -u)" -eq 0 ] || sudo_cmd=sudo
+    $sudo_cmd apt-get update -qq
+    $sudo_cmd env DEBIAN_FRONTEND=noninteractive apt-get install -y -qq "coq=$COQ_DEB_VERSION"
+  fi
+  actual="$(coqc --print-version | awk '{print $1}')"
+  if [ "$actual" != "$COQ_VERSION" ]; then
+    printf 'Rocq/Coq mismatch: expected %s, got %s\n' "$COQ_VERSION" "$actual" >&2
+    exit 1
+  fi
+  printf 'coq=%s (deb %s)\n' "$actual" "$COQ_DEB_VERSION"
+fi
+
+if [ "$want" = all ] || [ "$want" = lean ]; then
+  archive="$tool_dir/lean-$LEAN_VERSION-linux.tar.zst"
+  if [ ! -f "$archive" ]; then
+    curl --fail --location --retry 3 --proto '=https' --output "$archive" \
+      "https://github.com/leanprover/lean4/releases/download/v$LEAN_VERSION/lean-$LEAN_VERSION-linux.tar.zst"
+  fi
+  printf '%s  %s\n' "$LEAN_SHA256" "$archive" | sha256sum --check --strict -
+  tar --zstd -xf "$archive" -C "$tool_dir"
+  lean="$tool_dir/lean-$LEAN_VERSION-linux/bin/lean"
+  actual="$("$lean" --version)"
+  case "$actual" in
+    "Lean (version $LEAN_VERSION,"*) ;;
+    *) printf 'Lean mismatch: expected %s, got %s\n' "$LEAN_VERSION" "$actual" >&2; exit 1 ;;
+  esac
+  printf 'export LEAN=%q\n' "$lean" > "$tool_dir/env.sh"
+  [ -z "${GITHUB_ENV:-}" ] || printf 'LEAN=%s\n' "$lean" >> "$GITHUB_ENV"
+  printf '%s\nlean-archive-sha256=%s\n' "$actual" "$LEAN_SHA256"
+fi