v0.2: minimal formal alignment for replay boundary

[doomhammerhell]

Problem

The formal artifacts should reflect the replay boundary at a small, honest level: a candidate assignment is accepted only when hash identity and energy agreement hold under the declared model.

Acceptance Criteria

• Add or extend a small Lean definition for replay acceptance over a simplified energy model.
• Prove at least one true lemma about accepted candidates preserving recomputed energy equality.
• Add a readable TLA+ sketch for candidate states: submitted, verified, rejected.
• Keep formal claims explicitly scoped to simplified kernels.
• cd formal/lean && lake build passes when Lean is available.

Boundary

This issue must not imply a proof of the entire Python/Rust implementation.