Verified interval arithmetic for Lean 4 — prove bounds on exp, sin, cos, find roots, all machine-checked