SafeRateLimiter: Neg Nat at L74 and L115 blocks the package build at module 5 of 300

[hyperpolymath]

Summary

With the SafePolicy.idr divergence fixed, idris2 --build proven.ipkg now answers
(6s, rc=1) instead of being cancelled at CI's 45-minute timeout. It stops at module 5 of
300 on two errors in Proven.SafeRateLimiter:

Proven.SafeRateLimiter:74  Can't find an implementation for Neg Nat
Proven.SafeRateLimiter:115 Can't find an implementation for Neg Nat

Ordinary - is being used on Nat. Nat has no Neg implementation by design —
truncating subtraction is minus.

Why nobody has ever seen this

The build never got here. SafePolicy is module 1 of 300 and it never terminated, so
every subsequent module was unreached and the job was cancelled at the timeout. Steps
after the build — including the one named "Type check all modules" — were reported
skipped on every run. The compile status was VOID (no check performed), not red.

This is the first defect revealed by making the build answer, and there will be more
behind it: a full per-file census found 91 files with own defects (see the companion
issue).

Note

Proven.SafeRateLimiter is not enumerated in proven.ipkg (only
Proven.FFI.SafeRateLimiter, L339) — it is built transitively via import. Any audit that
decides what is built by reading the ipkg module list will miss it.

Measured 2026-08-27 against c83c7bf3.