docs: plan verified application libraries

[kim-em]

Summary

• expand SPEC/future-work.md with implementable roadmaps for widely applicable computational mathematics
• name the proposed algorithms, library boundaries, verification theorems, and manual examples
• incorporate design lessons from established computer-algebra systems while keeping computational libraries Mathlib-free
• distinguish checked results, completeness claims, heuristic outcomes, and noncanonical constructions

Verification

• git diff --check origin/main...HEAD
• documentation-only change; no Lean build required