feat: add Lean 4 formal proofs — progress, preservation, determinism

560 LOC covering syntax, typing judgment (13 rules), small-step
semantics (26 rules), canonical forms, and three core theorems.
Zero sorry. Covers knot-theoretic compose/tensor/close operations.

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

Author: hyperpolymath