feat: bounded-search-is-decidable — EchoSearch decidability bridge

[hyperpolymath]

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:

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.ai/code/session_018CaSgNjNURC7ocsyjYh9We

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 6 issues detected

Severity	Count
🔴 Critical	0
🟠 High	3
🟡 Medium	3

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "Repository has 6 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Scorecard): TokenPermissionsID -- Token-Permissions -- 18 day(s) old [STALE]",
    "type": "CSA001",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert TokenPermissionsID (high) at .github/workflows/scorecard.yml is 18 days old (threshold: 7 days) -- overdue for remediation",
    "type": "CSA003",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert hypatia/code_safety/agda_postulate dismissed as 'false positive' -- ensure dismissal is documented and justified",
    "type": "CSA004",
    "file": "proofs/agda/EchoImageFactorizationPropPostulated.agda",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence