feat(proofs): eliminate all 12 Lean4 sorry proofs

Added 17 Step constructors (sAddFloat, sAddString, sEqFalse, sAnd,
sNegFloat, sUnOpCong, sOkayCong, sOopsCong, sUnwrapCong, sUnwrapError,
plus 6 error propagation rules). Added Expr.error and 3 canonical forms
lemmas. Progress, preservation, type_safety fully proved. 527→747 lines.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath