feat: echo-search-product — bounded product (sequential) search composition

[hyperpolymath]

What

Closes the last "where next" gap in EchoSearch — product (sequential) composition of bounded searches. This is gap 3-of-3 from the proof survey (decidability #251 and Lipschitz #252 already merged).

The correction

The module's original sketch — EchoS … f b n₁ → EchoS … g y n₂ → EchoS … (g ∘ f) y (n₁ * n₂) — is ill-typed: the second search produces a g-preimage of y over its own enumerator, with no tie to the first search's output b, so g (f x) ≡ y doesn't follow. The well-typed composition is the product of two independent searches:

productEnum n₂ enum₁ enum₂ k = (enum₁ (k / n₂) , enum₂ (k % n₂))

echo-search-product :
  EchoS enum₁ f₁ y₁ n₁ → EchoS enum₂ f₂ y₂ n₂ →
  EchoS (productEnum n₂ enum₁ enum₂) (productMap f₁ f₂) (y₁ , y₂) (n₁ * n₂)

How (the row-major pairing)

The witness pairs the two step indices as k₂ + k₁ * n₂:

• bound < n₁ * n₂: k₂ + k₁*n₂ < n₂ + k₁*n₂ = suc k₁ * n₂ ≤ n₁ * n₂ (+-monoˡ-< then *-monoˡ-≤);
• recovery: / n₂ ≡ k₁ (+-distrib-/-∣ʳ + m*n/n≡m + m<n⇒m/n≡0) and % n₂ ≡ k₂ ([m+kn]%n≡m%n + m<n⇒m%n≡m).

The n₁ * n₂ budget provably requires this budget-dependent pairing — a global ℕ × ℕ ↔ ℕ cannot keep pair (n₁-1) (n₂-1) < n₁ * n₂ — which is exactly why it divides by n₂ and carries NonZero n₂ (a zero-width second dimension admits no witness anyway). That's the bijection the module deferred "to the slice that wants it".

Discipline

• --safe --without-K, zero postulates, structural.
• 3 Smoke pins (productMap, productEnum, echo-search-product); the "where next" note marked LANDED with the ill-typed-sketch correction.
• Verified on latest main: EchoSearch, Smoke.agda, All.agda all exit 0; kernel-guard.sh PASS (existing module — no new module).

Context

This is the final gap from the proof-surface survey. With it, the echo-types proof surface is gap-free apart from the deliberately parked ordinal/fidelity ladder and the author-driven Pillar E paper.

🤖 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

[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 5 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