formal: add replay boundary kernel

[doomhammerhell]

Closes #6.

Summary

• adds a small Lean replay-boundary predicate over expected hashes, submitted hashes, assignment completeness, metadata well-formedness, and reported/recomputed energy equality
• proves accepted candidates preserve energy agreement, problem-hash identity, and assignment completeness in the simplified kernel
• adds a readable TLA+ single-candidate state sketch with submitted, verified, and rejected transitions
• scopes formal claims to reviewable kernels, not implementation-wide correctness

Verification

• cd formal/lean && lake build
• bash scripts/run_audit.sh