feat: bounded-search-is-decidable — EchoSearch decidability bridge (#251)

## What

Closes the `bounded-search-is-decidable` gap that `EchoSearch.agda`
flagged under "where next" — the concrete bridge from `EchoSearch` to
`EchoDecidable` (axis 8(3)).

## How

`EchoS enum f y n` is *exactly* the bounded existential `Σ k. (k < n) ×
(f (enum k) ≡ y)`, so under decidable equality on `B` it's decidable by
structural recursion on the budget `n`:

```agda
bounded-search-is-decidable :
  (_≟_ : (x y : B) → Dec (x ≡ y))
  (enum : SearchStrategy A) (f : A → B) (y : B) (n : ℕ) →
  Dec (EchoS enum f y n)
```

- `n = 0` → `no` (via the existing `echo-search-bound-zero`).
- `n = suc n` → test the new index `n` with `_≟_`; on a hit, `yes`;
otherwise recurse on `n`. The negative case refutes every index below
`suc n` via `<-cmp` trichotomy: indices `< n` by the recursive `¬below`,
the index `n` itself by `¬eq`, and none strictly between `n` and `suc
n`.

A small design touch: the refutation matches the `<` proof as `s≤s k≤n`
to get `k ≤ n` directly, avoiding any `≤-pred` name dependency.

## Discipline

- `--safe --without-K`, **zero postulates**, structural recursion (no
`TERMINATING`).
- Pinned in `Smoke.agda`; the module's "where next" note marked LANDED.
`EchoSearch` was already classified (only a lemma added, no new module),
so `kernel-guard.sh` PASS.
- **Verified on latest `main`:** `EchoSearch.agda`, `Smoke.agda`,
`All.agda` all `agda --safe --without-K` exit 0 (captured locally).

## Context

This is one of only three small gaps a full proof-surface survey found
still open (the rest of the historical roadmap has landed). The other
two are **not** clean closes and I'm leaving them for your steer (see
the session note): EchoApprox's Lipschitz bound needs an
interface-design decision (a multiplicative-tolerance algebra), and
EchoSearch's sequential composition needs a from-scratch `ℕ × ℕ ↔ ℕ`
Cantor pairing (stdlib has none) that the module itself defers until a
consumer needs it.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

---
_Generated by [Claude
Code](https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

proofs/agda/EchoSearch.agda

@@ -67,20 +67,23 @@
 --     ∧ trace.last ≡ x ∧ f x ≡ y`. The current `EchoS` projects from
 --     that by collapsing the trace to its terminal index.
 --
---   * A *bounded-search-is-decidable* lemma in the presence of
---     decidable equality on `B`: search up to `n` either yields an
+--   * (LANDED) A *bounded-search-is-decidable* lemma in the presence
+--     of decidable equality on `B`: search up to `n` either yields an
 --     `EchoS enum f y n` or proves `¬ EchoS enum f y n`. This is the
---     concrete bridge to `EchoDecidable`, kept as a separate slice
---     because it needs a `_≟_` on `B` and a finite-walk recursion.
+--     concrete bridge to `EchoDecidable`; it needs a `_≟_` on `B` and a
+--     finite-walk recursion on the budget. See `bounded-search-is-decidable`
+--     at the bottom of this module.
 
 module EchoSearch where
 
 open import Function.Base                         using (_∘_; id)
 open import Data.Nat.Base                         using (ℕ; zero; suc; _≤_; _<_; z≤n; s≤s)
-open import Data.Nat.Properties                   using (≤-<-trans; <-≤-trans)
+open import Data.Nat.Properties
+  using (≤-<-trans; <-≤-trans; <-cmp; <-trans; ≤-trans; ≤-refl; <-irrefl)
 open import Data.Empty                            using (⊥; ⊥-elim)
 open import Data.Product.Base                     using (Σ; _,_; _×_; proj₁; proj₂)
-open import Relation.Nullary                      using (¬_)
+open import Relation.Nullary                      using (¬_; Dec; yes; no)
+open import Relation.Binary.Definitions           using (Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; trans; cong)
 
@@ -156,3 +159,38 @@ echo-search-postcompose :
   EchoS enum f y n → EchoS enum (g ∘ f) (g y) n
 echo-search-postcompose enum f g (k , k<n , eq) =
   k , k<n , cong g eq
+
+----------------------------------------------------------------------
+-- Decidability bridge
+----------------------------------------------------------------------
+
+-- Bounded search is decidable under decidable equality on the codomain.
+-- Because `EchoS enum f y n` is exactly the bounded existential
+-- `Σ k. (k < n) × (f (enum k) ≡ y)`, searching up to the budget `n`
+-- either produces a bound-`n` search echo or refutes one. This is the
+-- concrete bridge from EchoSearch to `EchoDecidable` (axis 8(3)): no
+-- machine model is required, only the step budget and a `_≟_` on `B`.
+-- Structural recursion on `n`; the `suc` step tests the new index `n`
+-- and otherwise recurses, using trichotomy to refute every index below
+-- `suc n` in the negative case.
+bounded-search-is-decidable :
+  ∀ {a b} {A : Set a} {B : Set b}
+  (_≟_ : (x y : B) → Dec (x ≡ y))
+  (enum : SearchStrategy A) (f : A → B) (y : B) (n : ℕ) →
+  Dec (EchoS enum f y n)
+bounded-search-is-decidable _≟_ enum f y zero =
+  no (echo-search-bound-zero enum f y)
+bounded-search-is-decidable _≟_ enum f y (suc n) with f (enum n) ≟ y
+... | yes eq = yes (n , ≤-refl , eq)
+... | no ¬eq with bounded-search-is-decidable _≟_ enum f y n
+...   | yes (k , k<n , eqk) = yes (k , <-trans k<n ≤-refl , eqk)
+...   | no ¬below          = no λ { (k , k<1+n , eqk) → contra k k<1+n eqk }
+  where
+    -- No index below `suc n` can witness `y`: indices below `n` are
+    -- refuted by `¬below`, the index `n` itself by `¬eq`, and there is
+    -- no index strictly between `n` and `suc n`.
+    contra : ∀ k → k < suc n → f (enum k) ≡ y → ⊥
+    contra k (s≤s k≤n) eqk with <-cmp k n
+    ... | tri< k<n _ _ = ¬below (k , k<n , eqk)
+    ... | tri≈ _ k≡n _ = ¬eq (trans (sym (cong (λ j → f (enum j)) k≡n)) eqk)
+    ... | tri> _ _ n<k = <-irrefl refl (≤-trans n<k k≤n)

proofs/agda/Smoke.agda

@@ -482,6 +482,7 @@ open import EchoSearch using
   ; echo-search-forget
   ; echo-search-bound-zero
   ; echo-search-postcompose
+  ; bounded-search-is-decidable
   )
 
 -- Per-lemma pins for the parameterised EchoSearch via