[P0] boj-server: audit 9 believe_me in safety-critical MCP boundary

[hyperpolymath]

9 believe_me across 3 .idr files in the unified MCP (SafePromptInjection etc.). PROOF-NEEDS wrongly states zero. Audit each: replace with real proof or document as justified runtime obligation. Reconcile PROOF-NEEDS.md.

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

🤖 Generated with Claude Code

[hyperpolymath]

PR hyperpolymath/boj-server#81 opened (Refs, not Closes).

Audit result: 5 believe_me (raw grep 9 = 5 real + 4 comment mentions), all in src/abi/Boj/SafetyLemmas.idr, all class (J) genuinely-unavoidable backend-primitive axioms (prim__eqChar soundness/symmetry; prim__str* length semantics) — irreducible within Idris2 0.8.0, %unsafe, isolated, individually documented. No removable debt. The real defect (stale origin/main PROOF-NEEDS claiming "4") is fixed by #81 with a per-site Axiom Audit table. Awaiting review; joint-close on agreement.

[hyperpolymath]

Joint-close approved by maintainer 2026-05-18. PR hyperpolymath/boj-server#81 squash-merged. Outcome: 5 believe_me confirmed all class-(J) justified backend-primitive axioms (0 removable debt); stale 'zero/4' PROOF-NEEDS reconciled with per-site Axiom Audit table.