governance(hypatia): no_tests high finding is a false-positive on a proof library — allow-list it #271

Hypatia honest_completion no_tests (high, −20 deduction), surfaced on the #266 scan.

No test directory or test files found.

Assessment (verified): false positive for this repo. echo-types is a constructive Agda proof library; the verified suite is proofs/agda/All.agda + proofs/agda/Smoke.agda under --safe --without-K (run by .github/workflows/agda.yml), plus scripts/kernel-guard.sh. There is no separate test/ directory by design — a green agda All.agda / agda Smoke.agda is the test. The −20 fires on every commit.

Disposition: tune the rule for this repo — allow-list no_tests, or point honest_completion at the Agda suite (All.agda/Smoke.agda) as the test oracle. Pre-existing; not introduced by any specific PR.

Source: Hypatia neurosymbolic scan on #266.