ci(lean): add Lean proof gate (lake build) guarding the metatheory (#61)

There was no Lean CI anywhere in the estate, so the mechanized proofs
(type safety, Sandbox Isolation Thm 1, Capability Soundness Thm 2,
Ethical Verdict Consistency, BFT quorum-intersection Thm 3) were
unguarded against regression. This gate runs `lake build` on every
push/PR via leanprover/lean-action (SHA-pinned v1.5.0), building
academic/formal-verification/lean4/ on core Lean (no Mathlib, no
test/lint targets). A broken proof now fails CI.

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath