proof(lean4): complete preservation + determinism; build Phronesis.lean on core Lean (#40)

Clears the two TODO/sorry placeholders in the Lean 4 type-safety formalization
by porting the big-step evaluation relation + theorems from the complete Coq
development (../coq/Phronesis.v):
  * Eval : ValEnv -> PhrExpr -> PhrValue -> Prop  (big-step, mirrors Coq)
  * preservation : a well-typed closed expr evaluates to a value of its type
  * determinism  : evaluation is deterministic

Also makes the whole file actually compile (it imported Mathlib but had no
build setup and several core errors, so it had never been checked): drops the
unnecessary Mathlib imports (proofs use only core tactics), makes size and
containsDangerous structurally terminate via mutual helpers, drops the
non-core-derivable (unused) DecidableEq on PhrType, fixes le_refl and size
type annotations. Adds lakefile.lean + lean-toolchain (Lean v4.12.0, no deps)
so CI can build with only the toolchain.

Verified: lake build succeeds; '#print axioms' shows determinism depends on NO
axioms and preservation only on propext -- no sorryAx anywhere.

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

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

Author: hyperpolymath

academic/formal-verification/lean4/.gitignore

@@ -0,0 +1 @@
+/.lake/