[P1] typed-wasm: 5 believe_me + 5 assert_total in ABI surface

[hyperpolymath]

ABI surface trusted transitively by other repos. Agent called it 'fully real'; it is not. Discharge or justify each of 5 believe_me + 5 assert_total + 5 partial.

Sub-issue of #124. PRs Refs hyperpolymath/standards#124. Joint-close only on explicit agreement.

🤖 Generated with Claude Code

[hyperpolymath]

Ground-truth reconciliation (per epic #124: reconcile PROOF-NEEDS vs ground truth in same pass)

This issue's stated debt is refuted. The claim "5 believe_me + 5 assert_total + 5 partial" and "agent called it fully real; it is not" does not match ground truth.

Comprehensive re-grep over all 21 .idr files (believe_me, really_believe_me, assert_total, assert_smaller, postulate, idris_crash, prim__crash, %default partial, Admitted, sorry, unsafePerformIO, assert_linear) → zero in code, only inside "NO believe_me" banner comments. This is the over-report failure mode (inverse of the under-report one the epic records elsewhere). The repo's own PROOF-NEEDS.md (2026-04-13) already stated zero; commit e4253f0 removed the last believe_me (Epistemic).

Verified build — src/abi/typed-wasm.ipkg, Idris2 0.8.0: rc=0, 0 errors, 21/21 modules → TTC, %default total in all 21. Only 11 warnings, all one cosmetic kind (lowercase implicit-bind shadowing). The 2026-04-13 "Tropical/Epistemic draft-only, standalone-check fails" concern is resolved (both now in the ipkg, build clean).

Genuine residual debt — discharged additively

The real defect is the one PROOF-NEEDS.md §P1 names: the 15 attestLN_* functions required a witness in their type then discarded it (_ = MkAttestation N Proven). Discharged in typed-wasm#33 via Proofs.idr §A9 — an attestLN_Sound theorem for all 15 levels, each requiring the exact witness type and proving LevelAchievedIn N [attestLN witness] (the missing witness⟹certificate bridge). Purely additive; no prior proof can regress; same clean rc=0 build verifies.

Stronger "attestation entails the level's semantic property" (reindex LevelAttestation by witness) is honestly scoped as tracked future work — recommend this issue stay open for that, with the trust-escape framing marked resolved-by-reconciliation.

PR: hyperpolymath/typed-wasm#33 — Refs #124/#130, not Closes (joint-close only on explicit agreement).

[hyperpolymath]

Reconciliation → recommend joint-close (#130 typed-wasm).

The audit was an OVER-report (the inverse of this epic's usual under-report mode). Comprehensive re-grep of all 21 .idr files for believe_me/really_believe_me/assert_total/assert_smaller/postulate/idris_crash/prim__crash/%default partial/Admitted/sorry/unsafePerformIO/assert_linear = ZERO in code (only 'NO believe_me' banner comments). Build: typed-wasm.ipkg Idris2 0.8.0 rc=0, 0 errors, 21/21 TTC, %default total all 21 (11 cosmetic shadowing warnings only).

Genuine residual debt found & DISCHARGED additively: the 15 attestLN_* in Proofs.idr required a witness then discarded it (PROOF-NEEDS §P1 'ceremony ≠ evidence'). Added Proofs.idr §A9 attestLN_Sound family (15 thms, witness⟹cert-claims-level bridge) — purely additive, no existing def touched, same rc=0 build verifies. Shipped as PR typed-wasm#33 (Refs #124+#130). Stronger 'attestation entails semantic property' is tracked future work, not gating.

#130 SHIPPED, base ground-truth-verified. Recommend joint-close on PR#33 merge.