[P0] echidna: reconcile 21 believe_me + clear ParetoMaximality sorry

[hyperpolymath]

E10–E13 Lean DONE (#53/PR#71 merged). Residual: 21 Idris2 believe_me (17 files) vs PROOF-NEEDS claiming zero; 2 assert_total; 1 stray sorry in verification/proofs/lean4/ParetoMaximality.lean. Reconcile PROOF-NEEDS, discharge or justify each.

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

🤖 Generated with Claude Code

[hyperpolymath]

PR hyperpolymath/echidna#82 opened (Refs, not Closes).

Result: zero genuine believe_me/really_believe_me — all 21 raw hits are prose/brief-text/axiom-detector string literals; ParetoMaximality "sorry" hits are prose documenting deliberate absence. Doc reconciled. E10–E13 Lean already discharged (#53/PR71).

Genuine debt split out: E4 Lean half ConfidenceLattice.lean fails lake build (unfold_let removed in 4.13.0, non-mechanical) → new sub-issue #136. The believe_me arm (this #126) is doc-only; awaiting review + joint-close.

[hyperpolymath]

Joint-close approved by maintainer 2026-05-18. PR hyperpolymath/echidna#82 squash-merged. Outcome: zero genuine believe_me (all 21 = prose/detector strings); ParetoMaximality 'sorry' is prose. Genuine residual debt (ConfidenceLattice.lean lake build) split to #136.