[P0-discharge] proof-of-work: discharge OWED ABI postulates

[hyperpolymath]

Seam (src/abi/{Types,Foreign,Invariants}.idr, 559 LOC) + RUST-SPARK-STANCE.adoc landed 2026-05-18. Remaining: discharge OWED postulates — difficulty monotonicity (I5) and hash collision-resistance — or keep as documented runtime obligations with Rust source refs.

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

🤖 Generated with Claude Code

[hyperpolymath]

PR hyperpolymath/proof-of-work#56 opened (Refs, not Closes).

Key finding: the audit's 'seam + stance landed today' was inaccurate — src/abi/{Types,Foreign,Invariants}.idr + RUST-SPARK-STANCE.adoc were untracked, never version-controlled. PR #56 commits them.

I5 genuinely discharged & idris2-verified: decNonDecreasing : (ds) -> Dec (NonDecreasing ds) (total) + builtinPackMonotone : NonDecreasing [1,2,3,4,5]; blanket postulate kept erased only as the runtime-obligation statement.

Remaining (keeps #128 open): I3 placePreservesWF TRUE+dischargeable but needs cons-distribution lemmas for foldl-based Prelude all/any (tracked); I2 real defect; I4/I7 OWED; I6 genuine crypto hardness (correctly postulated). Also: wire idris2 --check into CI (flat src/abi vs hierarchical modules, no .ipkg).