diff --git a/.github/workflows/lean-proofs.yml b/.github/workflows/lean-proofs.yml
new file mode 100644
index 0000000..a167b7b
--- /dev/null
+++ b/.github/workflows/lean-proofs.yml
@@ -0,0 +1,46 @@
+# SPDX-License-Identifier: MPL-2.0
+# lean-proofs.yml — machine-checks the Lean 4 formal-verification proofs.
+#
+# Guards the root cause documented in docs/proofs/verification/AUDIT.md: the
+# proofs had bit-rotted because no CI ever ran the prover. This gate keeps the
+# "sorry-free, compiles" invariant honest from now on.
+name: lean-proofs
+
+on:
+  push:
+    paths:
+      - 'docs/proofs/verification/**'
+      - '.github/workflows/lean-proofs.yml'
+  pull_request:
+    paths:
+      - 'docs/proofs/verification/**'
+      - '.github/workflows/lean-proofs.yml'
+
+permissions:
+  contents: read
+
+jobs:
+  lean-check:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install Lean (version pinned by lean-toolchain)
+        run: |
+          set -euo pipefail
+          ver="$(sed -E 's#.*:v##' docs/proofs/verification/lean-toolchain)"
+          echo "Installing Lean ${ver}"
+          sudo apt-get update
+          sudo apt-get install -y zstd
+          curl -sSL -o /tmp/lean.tar.zst \
+            "https://github.com/leanprover/lean4/releases/download/v${ver}/lean-${ver}-linux.tar.zst"
+          sudo mkdir -p /opt/lean
+          sudo tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst -C /opt/lean
+          echo "/opt/lean/lean-${ver}-linux/bin" >> "$GITHUB_PATH"
+
+      - name: Verify WokeLang.lean (sorry-free; must exit 0 with no errors)
+        run: |
+          set -euo pipefail
+          lean --version
+          lean docs/proofs/verification/WokeLang.lean
+          echo "✅ WokeLang.lean verified"
diff --git a/docs/proofs/verification/AUDIT.md b/docs/proofs/verification/AUDIT.md
new file mode 100644
index 0000000..2a32a73
--- /dev/null
+++ b/docs/proofs/verification/AUDIT.md
@@ -0,0 +1,121 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+SPDX-FileCopyrightText: 2026 Hyperpolymath
+-->
+# WokeLang Lean4 Proof Audit
+
+This document records a completeness/correspondence audit of
+`WokeLang.lean`, answering the two questions raised in
+[`PROOF-NEEDS.md`](../../../PROOF-NEEDS.md): *is the sorry-free claim still
+true?* and *do the proofs cover the full type system or only a subset?*
+
+## Toolchain
+
+- **Prover:** Lean 4, pinned to **v4.30.0** (`lean-toolchain` in this
+  directory).
+- **Build / check:** the proof file has **no external dependencies**
+  (no Mathlib — only the Lean core prelude), so it is checked directly:
+
+  ```sh
+  lean docs/proofs/verification/WokeLang.lean   # exit 0, no output ⇒ verified
+  ```
+
+- **CI:** `.github/workflows/lean-proofs.yml` installs the pinned toolchain
+  and runs the check on every push. See the headline finding below for why
+  this gate was added.
+
+## Headline finding — the proofs had bit-rotted (now fixed)
+
+The file's doc-comment claimed *"all 12 `sorry` eliminated … verified"*. That
+claim was **true against an older Lean but had silently broken**: under Lean
+4.30.0 the file did **not** compile (~100 errors). Two root causes:
+
+1. **`deriving DecidableEq` no longer applies** to `Value` and `WokeType`.
+   `Value` contains `Float` (no `DecidableEq` in Lean 4 — NaN), and both types
+   nest `List Self`, which the `DecidableEq` deriving handler does not see
+   through. Fixed by deriving only `Repr`; equality decisions that the proofs
+   need (`by_cases v₁ = v₂`) work via Lean's classical fallback with no
+   instance required.
+2. **`induction h` on `HasType emptyTypeEnv …`** fails because `emptyTypeEnv`
+   is a *concrete* (non-variable) index. Fixed by generalising the index
+   (`generalize hΓ : emptyTypeEnv = Γ at h`) and threading the equation
+   through the induction hypotheses.
+
+The decisive lesson: **no CI ever ran the prover** (workflows only covered the
+OCaml core and e2e), so the headline correctness claim was never enforced.
+The repair restores `sorry`-free compilation *and* adds the missing CI gate.
+
+> The numeric "12 `sorry`" figure in the file header is historical; the
+> verified invariant going forward is simply *the CI `lean` check is green*.
+
+## Coverage — Lean model vs. the real language
+
+The Lean model formalises a **clean expression core** and is a **strict
+subset** of the surface language defined in `core/ast.ml` and implemented by
+the Rust type checker (`src/typechecker/mod.rs`).
+
+| Area | Lean `WokeLang.lean` | Surface language (`core/ast.ml`, `src/typechecker`) |
+|---|---|---|
+| Literals | int, float, string, bool, unit | + arrays, measured, `thanks` |
+| Arithmetic | `add` only (int/float/string) | `add sub mul div mod` (+ div/mod-by-zero), **mixed int/float promotion** |
+| Comparison | `eq` (same-type), no ordering | `eq ne lt gt le ge`, structural `eq` across **any** types |
+| Logical | `and` (both `bool`) | `and or` with **`to_bool` coercion** of any value |
+| Result type | `okay`/`oops`/`unwrap`/`error`, `tOkay…tUnwrap` | present in **Rust** typechecker (`Result(_, _)`); **absent** from `core/eval.ml` |
+| Unary | `neg` (int/float), `not` | + measured propagation |
+| Calls / arrays | `call`, `array` exprs (no typing rules) | builtins + user functions; arrays typed |
+| Statements | declared (`Stmt`), **no typing/exec** | full eval in `core/eval.ml` |
+| Units of measure | **not modelled** | `EMeasured` / `VMeasured`, unit-match checking |
+| Pattern matching, workers, custom types | **not modelled** | present |
+| Consent | `consent_monotonicity/preservation` | matches **spec** `axiomatic-semantics.md` (consent Hoare logic) |
+| Capabilities | data + `capSubsumes`/`hasCapability` (no theorems) | — |
+
+### What *is* proven (and now machine-checked)
+`canonical_forms_{int,float,string,bool,result}`, **`progress`**,
+**`preservation`**, **`type_safety`** (multi-step), and
+`consent_{monotonicity,preservation}` — for the expression core above,
+including the Result/`unwrap`/`error` panic-propagation fragment.
+
+## Correspondence map (re PROOF-NEEDS #2)
+
+PROOF-NEEDS #2 ("prove evaluation semantics match the Lean spec") rests on a
+**mismatch that must be acknowledged**: the three artefacts model *different*
+languages.
+
+- **Lean type system / Result / progress+preservation** ⟷ the **Rust**
+  `src/typechecker` (Hindley–Milner unification with `Result`, function
+  types). This is the right correspondence target for the type-safety story.
+- **Lean `consent_*`** ⟷ the **spec** `spec/axiomatic-semantics.md` (consent
+  Hoare triples). In correspondence. ✓
+- **`core/eval.ml`** is a *separate, older tree-walking interpreter*: it has
+  **no Result type**, but adds units-of-measure, `to_bool` coercions, mixed
+  int/float arithmetic, and structural cross-type `eq`. It is **not** the
+  language the Lean `Step` relation models.
+
+Consequently, "eval matches the Lean spec" is **not** currently a
+well-posed single theorem — the evaluator and the spec diverge. The honest
+options are (a) treat `WokeLang.lean` as the **normative spec** and converge
+the implementations toward it, or (b) build a *second* Lean model faithful to
+`core/eval.ml` (units + coercions + no Result) and prove properties there.
+
+## Recommended next proof steps
+
+1. **Broaden the verified core toward the Rust type system** (each is a small,
+   pattern-following extension to `Step`/`HasType` + the `progress`/
+   `preservation` cases, fully checkable):
+   - integer `sub`/`mul` (total), then `div`/`mod` with a divide-by-zero
+     `error` step (mirrors `unwrap`-of-`oops` panic propagation already
+     proven);
+   - ordering comparisons `lt/gt/le/ge` ⇒ `bool`;
+   - `or` (mirror of `and`).
+2. **Array typing** (`tArray`, an `array` congruence/▸ value rule) to retire
+   one of the `array`-shaped TODO gaps.
+3. **Decide the eval-correspondence question** (a) vs (b) above with the
+   maintainer before attempting PROOF-NEEDS #2.
+4. **Compiler/VM track** (the file's §8 TODO stubs: bytecode, compiler,
+   VM semantics, compiler-correctness) remains open and is a larger effort.
+
+## Status
+
+- Repair to `sorry`-free under Lean 4.30.0: see CI / `lean` check.
+- Coverage: **subset** of the surface language, as tabulated above — *not* a
+  full-language proof, and honestly so.
diff --git a/docs/proofs/verification/WokeLang.lean b/docs/proofs/verification/WokeLang.lean
index 30ac8ad..325db2e 100644
--- a/docs/proofs/verification/WokeLang.lean
+++ b/docs/proofs/verification/WokeLang.lean
@@ -55,7 +55,7 @@ inductive WokeType where
   | result : WokeType → WokeType → WokeType
   | function : List WokeType → WokeType → WokeType
   | typeVar : Nat → WokeType
-  deriving Repr, DecidableEq
+  deriving Repr
 
 /-- Runtime values -/
 inductive Value where
@@ -67,7 +67,7 @@ inductive Value where
   | vArray : List Value → Value
   | vOkay : Value → Value
   | vOops : String → Value
-  deriving Repr, DecidableEq
+  deriving Repr
 
 /-- Binary operators -/
 inductive BinOp where
@@ -323,8 +323,8 @@ theorem canonical_forms_result : ∀ v tOk tErr,
   (∃ inner, v = .vOkay inner) ∨ (∃ s, v = .vOops s) := by
   intro v tOk tErr h
   cases h with
-  | tOkayVal _ _ _ h₁ => left; exact ⟨_, rfl⟩
-  | tOopsVal _ _ _ => right; exact ⟨_, rfl⟩
+  | tOkayVal _ _ h₁ => left; exact ⟨_, rfl⟩
+  | tOopsVal _ _ => right; exact ⟨_, rfl⟩
 
 /-- Progress theorem: a well-typed closed expression is either a value or can step.
     unwrap of an error value steps to an error expression via sUnwrapError,
@@ -339,12 +339,12 @@ theorem progress : ∀ e t,
   | tString => left; constructor
   | tBool => left; constructor
   | tUnit => left; constructor
-  | tOkayVal _ _ _ _ => left; constructor
-  | tOopsVal _ _ _ => left; constructor
-  | tVar Γ x t hx =>
+  | tOkayVal _ _ _ => left; constructor
+  | tOopsVal _ _ => left; constructor
+  | tVar x t hx =>
     -- Variable in empty env is contradiction
     simp [emptyTypeEnv] at hx
-  | tAddInt Γ e₁ e₂ h₁ h₂ ih₁ ih₂ =>
+  | tAddInt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
     right
     cases ih₁ with
     | inl hv₁ =>
@@ -360,13 +360,15 @@ theorem progress : ∀ e t,
             exact ⟨.lit (.vInt (n₁ + n₂)), emptyEnv, .sAddInt n₁ n₂ emptyEnv⟩
           | error msg =>
             exact ⟨.error msg, emptyEnv, .sBinOpErrRight .add v₁ msg emptyEnv⟩
-        | inr ⟨e₂', ρ', hs₂⟩ =>
+        | inr hstp =>
+          obtain ⟨e₂', ρ', hs₂⟩ := hstp
           exact ⟨.binOp .add (.lit v₁) e₂', ρ', .sBinOpRight .add v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .add msg e₂ emptyEnv⟩
-    | inr ⟨e₁', ρ', hs₁⟩ =>
+    | inr hstp =>
+      obtain ⟨e₁', ρ', hs₁⟩ := hstp
       exact ⟨.binOp .add e₁' e₂, ρ', .sBinOpLeft .add _ e₁' e₂ emptyEnv ρ' hs₁⟩
-  | tAddFloat Γ e₁ e₂ h₁ h₂ ih₁ ih₂ =>
+  | tAddFloat e₁ e₂ h₁ h₂ ih₁ ih₂ =>
     right
     cases ih₁ with
     | inl hv₁ =>
@@ -382,13 +384,15 @@ theorem progress : ∀ e t,
             exact ⟨.lit (.vFloat (f₁ + f₂)), emptyEnv, .sAddFloat f₁ f₂ emptyEnv⟩
           | error msg =>
             exact ⟨.error msg, emptyEnv, .sBinOpErrRight .add v₁ msg emptyEnv⟩
-        | inr ⟨e₂', ρ', hs₂⟩ =>
+        | inr hstp =>
+          obtain ⟨e₂', ρ', hs₂⟩ := hstp
           exact ⟨.binOp .add (.lit v₁) e₂', ρ', .sBinOpRight .add v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .add msg e₂ emptyEnv⟩
-    | inr ⟨e₁', ρ', hs₁⟩ =>
+    | inr hstp =>
+      obtain ⟨e₁', ρ', hs₁⟩ := hstp
       exact ⟨.binOp .add e₁' e₂, ρ', .sBinOpLeft .add _ e₁' e₂ emptyEnv ρ' hs₁⟩
-  | tAddString Γ e₁ e₂ h₁ h₂ ih₁ ih₂ =>
+  | tAddString e₁ e₂ h₁ h₂ ih₁ ih₂ =>
     right
     cases ih₁ with
     | inl hv₁ =>
@@ -404,13 +408,15 @@ theorem progress : ∀ e t,
             exact ⟨.lit (.vString (s₁ ++ s₂)), emptyEnv, .sAddString s₁ s₂ emptyEnv⟩
           | error msg =>
             exact ⟨.error msg, emptyEnv, .sBinOpErrRight .add v₁ msg emptyEnv⟩
-        | inr ⟨e₂', ρ', hs₂⟩ =>
+        | inr hstp =>
+          obtain ⟨e₂', ρ', hs₂⟩ := hstp
           exact ⟨.binOp .add (.lit v₁) e₂', ρ', .sBinOpRight .add v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .add msg e₂ emptyEnv⟩
-    | inr ⟨e₁', ρ', hs₁⟩ =>
+    | inr hstp =>
+      obtain ⟨e₁', ρ', hs₁⟩ := hstp
       exact ⟨.binOp .add e₁' e₂, ρ', .sBinOpLeft .add _ e₁' e₂ emptyEnv ρ' hs₁⟩
-  | tEq Γ e₁ e₂ t h₁ h₂ ih₁ ih₂ =>
+  | tEq e₁ e₂ _ h₁ h₂ ih₁ ih₂ =>
     right
     cases ih₁ with
     | inl hv₁ =>
@@ -426,13 +432,15 @@ theorem progress : ∀ e t,
             · exact ⟨.lit (.vBool false), emptyEnv, .sEqFalse v₁ v₂ emptyEnv heq⟩
           | error msg =>
             exact ⟨.error msg, emptyEnv, .sBinOpErrRight .eq v₁ msg emptyEnv⟩
-        | inr ⟨e₂', ρ', hs₂⟩ =>
+        | inr hstp =>
+          obtain ⟨e₂', ρ', hs₂⟩ := hstp
           exact ⟨.binOp .eq (.lit v₁) e₂', ρ', .sBinOpRight .eq v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .eq msg e₂ emptyEnv⟩
-    | inr ⟨e₁', ρ', hs₁⟩ =>
+    | inr hstp =>
+      obtain ⟨e₁', ρ', hs₁⟩ := hstp
       exact ⟨.binOp .eq e₁' e₂, ρ', .sBinOpLeft .eq _ e₁' e₂ emptyEnv ρ' hs₁⟩
-  | tAnd Γ e₁ e₂ h₁ h₂ ih₁ ih₂ =>
+  | tAnd e₁ e₂ h₁ h₂ ih₁ ih₂ =>
     right
     cases ih₁ with
     | inl hv₁ =>
@@ -448,13 +456,15 @@ theorem progress : ∀ e t,
             exact ⟨.lit (.vBool (b₁ && b₂)), emptyEnv, .sAnd b₁ b₂ emptyEnv⟩
           | error msg =>
             exact ⟨.error msg, emptyEnv, .sBinOpErrRight .and v₁ msg emptyEnv⟩
-        | inr ⟨e₂', ρ', hs₂⟩ =>
+        | inr hstp =>
+          obtain ⟨e₂', ρ', hs₂⟩ := hstp
           exact ⟨.binOp .and (.lit v₁) e₂', ρ', .sBinOpRight .and v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .and msg e₂ emptyEnv⟩
-    | inr ⟨e₁', ρ', hs₁⟩ =>
+    | inr hstp =>
+      obtain ⟨e₁', ρ', hs₁⟩ := hstp
       exact ⟨.binOp .and e₁' e₂, ρ', .sBinOpLeft .and _ e₁' e₂ emptyEnv ρ' hs₁⟩
-  | tNegInt Γ e h₁ ih =>
+  | tNegInt e h₁ ih =>
     right
     cases ih with
     | inl hv =>
@@ -465,9 +475,10 @@ theorem progress : ∀ e t,
         exact ⟨.lit (.vInt (-n)), emptyEnv, .sNegInt n emptyEnv⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sUnOpErr .neg msg emptyEnv⟩
-    | inr ⟨e', ρ', hs⟩ =>
+    | inr hstp =>
+      obtain ⟨e', ρ', hs⟩ := hstp
       exact ⟨.unOp .neg e', ρ', .sUnOpCong .neg _ e' emptyEnv ρ' hs⟩
-  | tNegFloat Γ e h₁ ih =>
+  | tNegFloat e h₁ ih =>
     right
     cases ih with
     | inl hv =>
@@ -478,9 +489,10 @@ theorem progress : ∀ e t,
         exact ⟨.lit (.vFloat (-f)), emptyEnv, .sNegFloat f emptyEnv⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sUnOpErr .neg msg emptyEnv⟩
-    | inr ⟨e', ρ', hs⟩ =>
+    | inr hstp =>
+      obtain ⟨e', ρ', hs⟩ := hstp
       exact ⟨.unOp .neg e', ρ', .sUnOpCong .neg _ e' emptyEnv ρ' hs⟩
-  | tNot Γ e h₁ ih =>
+  | tNot e h₁ ih =>
     right
     cases ih with
     | inl hv =>
@@ -491,9 +503,10 @@ theorem progress : ∀ e t,
         exact ⟨.lit (.vBool (!b)), emptyEnv, .sNot b emptyEnv⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sUnOpErr .not msg emptyEnv⟩
-    | inr ⟨e', ρ', hs⟩ =>
+    | inr hstp =>
+      obtain ⟨e', ρ', hs⟩ := hstp
       exact ⟨.unOp .not e', ρ', .sUnOpCong .not _ e' emptyEnv ρ' hs⟩
-  | tOkay Γ e t h₁ ih =>
+  | tOkay e _ h₁ ih =>
     right
     cases ih with
     | inl hv =>
@@ -502,9 +515,10 @@ theorem progress : ∀ e t,
         exact ⟨.lit (.vOkay v), emptyEnv, .sOkay v emptyEnv (.lit v)⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sOkayErr msg emptyEnv⟩
-    | inr ⟨e', ρ', hs⟩ =>
+    | inr hstp =>
+      obtain ⟨e', ρ', hs⟩ := hstp
       exact ⟨.okay e', ρ', .sOkayCong _ e' emptyEnv ρ' hs⟩
-  | tOops Γ e t h₁ ih =>
+  | tOops e _ h₁ ih =>
     right
     cases ih with
     | inl hv =>
@@ -515,9 +529,10 @@ theorem progress : ∀ e t,
         exact ⟨.lit (.vOops s), emptyEnv, .sOops s emptyEnv⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sOopsErr msg emptyEnv⟩
-    | inr ⟨e', ρ', hs⟩ =>
+    | inr hstp =>
+      obtain ⟨e', ρ', hs⟩ := hstp
       exact ⟨.oops e', ρ', .sOopsCong _ e' emptyEnv ρ' hs⟩
-  | tUnwrap Γ e tOk tErr h₁ ih =>
+  | tUnwrap e tOk tErr h₁ ih =>
     right
     cases ih with
     | inl hv =>
@@ -527,17 +542,20 @@ theorem progress : ∀ e t,
         -- sUnwrapOkay handles vOkay; sUnwrapError handles vOops.
         have hcf := canonical_forms_result v tOk tErr h₁
         cases hcf with
-        | inl ⟨inner, hinner⟩ =>
+        | inl hstp =>
+          obtain ⟨inner, hinner⟩ := hstp
           subst hinner
           exact ⟨.lit inner, emptyEnv, .sUnwrapOkay inner emptyEnv⟩
-        | inr ⟨s, hs⟩ =>
+        | inr hstp =>
+          obtain ⟨s, hs⟩ := hstp
           subst hs
           exact ⟨.error s, emptyEnv, .sUnwrapError s emptyEnv⟩
       | error msg =>
         exact ⟨.error msg, emptyEnv, .sUnwrapErr msg emptyEnv⟩
-    | inr ⟨e', ρ', hs⟩ =>
+    | inr hstp =>
+      obtain ⟨e', ρ', hs⟩ := hstp
       exact ⟨.unwrap e', ρ', .sUnwrapCong _ e' emptyEnv ρ' hs⟩
-  | tError _ msg _ =>
+  | tError msg _ =>
     -- Error expressions are terminal values (panics).
     left; exact .error msg
 
@@ -550,117 +568,125 @@ theorem preservation : ∀ e e' t ρ ρ',
   Step e ρ e' ρ' →
   HasType emptyTypeEnv e' t := by
   intro e e' t ρ ρ' ht hs
-  induction hs with
+  induction hs generalizing t with
   | sVar x ρ v hx =>
     -- Typed as (var x) in empty env ⇒ contradiction in progress,
     -- but preservation receives any ρ. By inversion on typing:
     -- HasType emptyTypeEnv (var x) t requires emptyTypeEnv x = some t,
     -- which is a contradiction.
     cases ht with
-    | tVar _ _ _ hx' => simp [emptyTypeEnv] at hx'
+    | tVar _ _ hx' => simp [emptyTypeEnv] at hx'
   | sBinOpLeft op e₁ e₁' e₂ ρ ρ' hs₁ ih =>
     cases ht with
-    | tAddInt _ _ _ h₁ h₂ => exact .tAddInt _ _ _ (ih h₁) h₂
-    | tAddFloat _ _ _ h₁ h₂ => exact .tAddFloat _ _ _ (ih h₁) h₂
-    | tAddString _ _ _ h₁ h₂ => exact .tAddString _ _ _ (ih h₁) h₂
-    | tEq _ _ _ _ h₁ h₂ => exact .tEq _ _ _ _ (ih h₁) h₂
-    | tAnd _ _ _ h₁ h₂ => exact .tAnd _ _ _ (ih h₁) h₂
+    | tAddInt _ _ h₁ h₂ => exact .tAddInt _ _ _ (ih _ h₁) h₂
+    | tAddFloat _ _ h₁ h₂ => exact .tAddFloat _ _ _ (ih _ h₁) h₂
+    | tAddString _ _ h₁ h₂ => exact .tAddString _ _ _ (ih _ h₁) h₂
+    | tEq _ _ _ h₁ h₂ => exact .tEq _ _ _ _ (ih _ h₁) h₂
+    | tAnd _ _ h₁ h₂ => exact .tAnd _ _ _ (ih _ h₁) h₂
   | sBinOpRight op v₁ e₂ e₂' ρ ρ' _hv hs₂ ih =>
     cases ht with
-    | tAddInt _ _ _ h₁ h₂ => exact .tAddInt _ _ _ h₁ (ih h₂)
-    | tAddFloat _ _ _ h₁ h₂ => exact .tAddFloat _ _ _ h₁ (ih h₂)
-    | tAddString _ _ _ h₁ h₂ => exact .tAddString _ _ _ h₁ (ih h₂)
-    | tEq _ _ _ _ h₁ h₂ => exact .tEq _ _ _ _ h₁ (ih h₂)
-    | tAnd _ _ _ h₁ h₂ => exact .tAnd _ _ _ h₁ (ih h₂)
+    | tAddInt _ _ h₁ h₂ => exact .tAddInt _ _ _ h₁ (ih _ h₂)
+    | tAddFloat _ _ h₁ h₂ => exact .tAddFloat _ _ _ h₁ (ih _ h₂)
+    | tAddString _ _ h₁ h₂ => exact .tAddString _ _ _ h₁ (ih _ h₂)
+    | tEq _ _ _ h₁ h₂ => exact .tEq _ _ _ _ h₁ (ih _ h₂)
+    | tAnd _ _ h₁ h₂ => exact .tAnd _ _ _ h₁ (ih _ h₂)
   | sAddInt n₁ n₂ _ =>
     cases ht with
-    | tAddInt _ _ _ h₁ h₂ => exact .tInt _ _
+    | tAddInt _ _ h₁ h₂ => exact .tInt _ _
+    | tAddFloat _ _ h₁ _ => nomatch h₁
+    | tAddString _ _ h₁ _ => nomatch h₁
   | sAddFloat f₁ f₂ _ =>
     cases ht with
-    | tAddFloat _ _ _ h₁ h₂ => exact .tFloat _ _
+    | tAddFloat _ _ h₁ h₂ => exact .tFloat _ _
+    | tAddInt _ _ h₁ _ => nomatch h₁
+    | tAddString _ _ h₁ _ => nomatch h₁
   | sAddString s₁ s₂ _ =>
     cases ht with
-    | tAddString _ _ _ h₁ h₂ => exact .tString _ _
+    | tAddString _ _ h₁ h₂ => exact .tString _ _
+    | tAddInt _ _ h₁ _ => nomatch h₁
+    | tAddFloat _ _ h₁ _ => nomatch h₁
   | sEqTrue v _ =>
     cases ht with
-    | tEq _ _ _ _ h₁ h₂ => exact .tBool _ _
+    | tEq _ _ _ h₁ h₂ => exact .tBool _ _
   | sEqFalse v₁ v₂ _ hneq =>
     cases ht with
-    | tEq _ _ _ _ h₁ h₂ => exact .tBool _ _
+    | tEq _ _ _ h₁ h₂ => exact .tBool _ _
   | sAnd b₁ b₂ _ =>
     cases ht with
-    | tAnd _ _ _ h₁ h₂ => exact .tBool _ _
+    | tAnd _ _ h₁ h₂ => exact .tBool _ _
   | sNegInt n _ =>
     cases ht with
-    | tNegInt _ _ h₁ => exact .tInt _ _
+    | tNegInt _ h₁ => exact .tInt _ _
+    | tNegFloat _ h₁ => nomatch h₁
   | sNegFloat f _ =>
     cases ht with
-    | tNegFloat _ _ h₁ => exact .tFloat _ _
+    | tNegFloat _ h₁ => exact .tFloat _ _
+    | tNegInt _ h₁ => nomatch h₁
   | sNot b _ =>
     cases ht with
-    | tNot _ _ h₁ => exact .tBool _ _
+    | tNot _ h₁ => exact .tBool _ _
   | sUnOpCong op e e' ρ ρ' hs₁ ih =>
     cases ht with
-    | tNegInt _ _ h₁ => exact .tNegInt _ _ (ih h₁)
-    | tNegFloat _ _ h₁ => exact .tNegFloat _ _ (ih h₁)
-    | tNot _ _ h₁ => exact .tNot _ _ (ih h₁)
+    | tNegInt _ h₁ => exact .tNegInt _ _ (ih _ h₁)
+    | tNegFloat _ h₁ => exact .tNegFloat _ _ (ih _ h₁)
+    | tNot _ h₁ => exact .tNot _ _ (ih _ h₁)
   | sOkay v _ _hv =>
     cases ht with
-    | tOkay _ _ _ h₁ => exact .tOkayVal _ v _ h₁
+    | tOkay _ _ h₁ => exact .tOkayVal _ v _ h₁
   | sOkayCong e e' ρ ρ' hs₁ ih =>
     cases ht with
-    | tOkay _ _ _ h₁ => exact .tOkay _ _ _ (ih h₁)
+    | tOkay _ _ h₁ => exact .tOkay _ _ _ (ih _ h₁)
   | sOops s _ =>
     cases ht with
-    | tOops _ _ _ h₁ => exact .tOopsVal _ s _
+    | tOops _ _ h₁ => exact .tOopsVal _ s _
   | sOopsCong e e' ρ ρ' hs₁ ih =>
     cases ht with
-    | tOops _ _ _ h₁ => exact .tOops _ _ _ (ih h₁)
+    | tOops _ _ h₁ => exact .tOops _ _ _ (ih _ h₁)
   | sUnwrapOkay v _ =>
     cases ht with
-    | tUnwrap _ _ tOk tErr h₁ =>
+    | tUnwrap _ tOk tErr h₁ =>
       -- h₁ : HasType emptyTypeEnv (lit (vOkay v)) (result tOk tErr)
       -- By inversion via tOkayVal, the inner value v has type tOk.
       cases h₁ with
-      | tOkayVal _ _ _ hinner => exact hinner
+      | tOkayVal _ _ hinner => exact hinner
   | sUnwrapError s _ =>
     cases ht with
-    | tUnwrap _ _ tOk tErr h₁ =>
+    | tUnwrap _ tOk tErr h₁ =>
       -- unwrap(oops(s)) steps to (error s), which is well-typed at any type
       -- via tError. This models runtime panic propagation.
-      exact .tError _ s tOk
+      exact .tError _ s t
   | sUnwrapCong e e' ρ ρ' hs₁ ih =>
     cases ht with
-    | tUnwrap _ _ tOk tErr h₁ => exact .tUnwrap _ _ tOk tErr (ih h₁)
+    | tUnwrap _ _ tErr h₁ => exact .tUnwrap _ _ _ _ (ih _ h₁)
   | sBinOpErrLeft op msg e₂ _ =>
     -- error propagates through binOp — result is error, typed at any type via tError.
     cases ht with
-    | tAddInt _ _ _ h₁ h₂ => exact .tError _ msg _
-    | tAddFloat _ _ _ h₁ h₂ => exact .tError _ msg _
-    | tAddString _ _ _ h₁ h₂ => exact .tError _ msg _
-    | tEq _ _ _ _ h₁ h₂ => exact .tError _ msg _
-    | tAnd _ _ _ h₁ h₂ => exact .tError _ msg _
+    | tAddInt _ _ h₁ h₂ => exact .tError _ msg _
+    | tAddFloat _ _ h₁ h₂ => exact .tError _ msg _
+    | tAddString _ _ h₁ h₂ => exact .tError _ msg _
+    | tEq _ _ _ h₁ h₂ => exact .tError _ msg _
+    | tAnd _ _ h₁ h₂ => exact .tError _ msg _
   | sBinOpErrRight op v₁ msg _ =>
     cases ht with
-    | tAddInt _ _ _ h₁ h₂ => exact .tError _ msg _
-    | tAddFloat _ _ _ h₁ h₂ => exact .tError _ msg _
-    | tAddString _ _ _ h₁ h₂ => exact .tError _ msg _
-    | tEq _ _ _ _ h₁ h₂ => exact .tError _ msg _
-    | tAnd _ _ _ h₁ h₂ => exact .tError _ msg _
+    | tAddInt _ _ h₁ h₂ => exact .tError _ msg _
+    | tAddFloat _ _ h₁ h₂ => exact .tError _ msg _
+    | tAddString _ _ h₁ h₂ => exact .tError _ msg _
+    | tEq _ _ _ h₁ h₂ => exact .tError _ msg _
+    | tAnd _ _ h₁ h₂ => exact .tError _ msg _
   | sUnOpErr op msg _ =>
     cases ht with
-    | tNegInt _ _ h₁ => exact .tError _ msg _
-    | tNegFloat _ _ h₁ => exact .tError _ msg _
-    | tNot _ _ h₁ => exact .tError _ msg _
+    | tNegInt _ h₁ => exact .tError _ msg _
+    | tNegFloat _ h₁ => exact .tError _ msg _
+    | tNot _ h₁ => exact .tError _ msg _
   | sOkayErr msg _ =>
     cases ht with
-    | tOkay _ _ _ h₁ => exact .tError _ msg _
+    | tOkay _ _ h₁ => exact .tError _ msg _
   | sOopsErr msg _ =>
     cases ht with
-    | tOops _ _ _ h₁ => exact .tError _ msg _
+    | tOops _ _ h₁ => exact .tError _ msg _
   | sUnwrapErr msg _ =>
     cases ht with
-    | tUnwrap _ _ tOk tErr h₁ => exact .tError _ msg _
+    | tUnwrap _ tOk tErr h₁ => exact .tError _ msg _
 
 /-- Type safety theorem -/
 theorem type_safety : ∀ e t v ρ,
@@ -668,17 +694,22 @@ theorem type_safety : ∀ e t v ρ,
   MultiStep e emptyEnv (.lit v) ρ →
   HasType emptyTypeEnv (.lit v) t := by
   intro e t v ρ ht hms
+  -- emptyEnv and (lit v) are concrete indices of hms; generalise them so the
+  -- induction on MultiStep is well-formed. The start value-env need not be
+  -- empty (preservation holds for any env), so its equation is cleared.
+  generalize hev : (Expr.lit v) = ev at hms ⊢
+  generalize hρ0 : emptyEnv = ρ0 at hms
+  clear hρ0
   induction hms with
   | refl => exact ht
   | step e₁ e₂ e₃ ρ₁ ρ₂ ρ₃ hs hms' ih =>
-    apply ih
-    exact preservation e₁ e₂ t ρ₁ ρ₂ ht hs
+    exact ih (preservation e₁ e₂ t ρ₁ ρ₂ ht hs) hev
 
 -- =========================================================================
 -- 6. Consent System
 -- =========================================================================
 
-def Permission := String
+abbrev Permission := String
 
 def ConsentState := Permission → Bool
 
diff --git a/docs/proofs/verification/lean-toolchain b/docs/proofs/verification/lean-toolchain
new file mode 100644
index 0000000..af9e5d3
--- /dev/null
+++ b/docs/proofs/verification/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.30.0