feat(proofs): Lean array typing — mirror Coq's T_Array/T_Lit_Array (#90)

## What

Closes the one **array-shaped Tier-1 gap** on the Lean side of the
formal development. AUDIT.md flagged it as *"exactly the Tier-1 item
still open on the Lean side"*; `WokeLang.lean` is now at parity with
`WokeLang.v` on arrays.

The `array` / `vArray` syntax already existed in Lean but had **no
typing rules**, so `induction` in `progress`/`preservation` never saw an
array case. This adds the rules and the operational semantics, with full
proof coverage.

## Changes (`docs/proofs/verification/WokeLang.lean`, +117 / −0 — purely
additive)

**Typing** (mirror of Coq `T_Array` / `T_Lit_Array`):
- `tArray` — `(∀ e ∈ es, HasType Γ e t) → HasType Γ (.array es) (.array
t)`
- `tArrayVal` — `(∀ v ∈ vs, HasType Γ (.lit v) t) → HasType Γ (.lit
(.vArray vs)) (.array t)`

**Evaluation** (mirror of `S_Array_step` / `S_Array_val` + panic
propagation):
- `sArrayStep` — reduce the left-most non-value element
- `sArrayVal` — normalise `.array (vs.map .lit)` to the literal value
`.lit (.vArray vs)`
- `sArrayErr` — propagate a panic out of an array (as the binop rules
do)

**Proofs** — `progress` and `preservation` extended to cover all three
step rules; helper lemmas `isLitB` + `array_split` (the analogue of
Coq's `array_elements_progress`).

## Verification

- `lean docs/proofs/verification/WokeLang.lean` → **exit 0, empty
output** (no errors, no warnings).
- **`sorry`-free and axiom-free** under Lean 4.30.0.
- Diff is **+117 / −0** on the proof file: existing theorems are
untouched; every change is a new constructor or a new case, so no
existing `cases`/`induction` becomes non-exhaustive.
- `WokeLang.v` (Coq) is **not modified**.

## Method note (vs. Coq)

Lean's `∀ e ∈ es` premise yields a **per-element induction hypothesis
directly** from `induction`, so — unlike the Coq proof — **no
well-founded recursion on an `expr_size` measure** is needed
(`array_split` does the pure-list decomposition; the IH answers
value-or-steps per element). A fully-evaluated array is *not* an
`IsValue` (it always steps via `sArrayVal` to the array literal), so
array equality reuses the generic `.lit`-equality rules after
normalisation rather than needing the extra array-equality step rules
Coq carries. `AUDIT.md` is updated to record the new parity.

> Branch note: `claude/sleepy-carson-bREoV` was based on current `main`
(it had been 9 commits behind). Its two prior commits — a Coq repair +
CI gate and a machine-readable state update — are fully superseded by
`main` (which already carries both CI gates, the repaired `WokeLang.v`,
and the binop-parity work). They are folded into history via a `-s ours`
merge (nothing rewritten or lost); the branch tree is a clean superset
of `main`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7

---
_Generated by [Claude
Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_

---------

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

Author: hyperpolymath

docs/proofs/verification/AUDIT.md

@@ -64,7 +64,7 @@ the Rust type checker (`src/typechecker/mod.rs`).
 | 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 |
+| Calls / arrays | `call` (no typing rule); **arrays typed + evaluated** (`tArray`/`tArrayVal`, `sArrayStep`/`sArrayVal`/`sArrayErr`) | 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 |
@@ -109,8 +109,10 @@ the implementations toward it, or (b) build a *second* Lean model faithful to
      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.
+2. ~~**Array typing** (`tArray`, an `array` congruence/▸ value rule)~~ —
+   **DONE (2026-06-18).** `tArray`/`tArrayVal` + `sArrayStep`/`sArrayVal`/
+   `sArrayErr`, with full `progress`/`preservation` coverage (see
+   "Extensions landed" below). This brings Lean to parity with Coq on arrays.
 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,
@@ -151,7 +153,33 @@ theorems (`weaken_collapses_distinction`, `affine_canonical`,
     `decide`).
 - **Tier 3 (capability):** `capSubsumes` is a preorder (`_refl`, `_trans`).
 - Still open in Tier 1: **float** arithmetic variants (`sub`/`mul`/`div` on
-  `float`, mirroring `add` on float) and **`array`** typing/evaluation.
+  `float`, mirroring `add` on float).
+
+## Arrays landed (2026-06-18) — Lean now at parity with Coq
+
+The one array-shaped Tier-1 gap is closed on the Lean side, mirroring Coq's
+`T_Array`/`T_Lit_Array`:
+
+- **Typing:** `tArray` (array expression, elementwise) and `tArrayVal`
+  (fully-evaluated `.vArray` literal value), both with the `∀ e ∈ es` premise.
+- **Evaluation:** `sArrayStep` (reduce the left-most non-value element),
+  `sArrayVal` (normalise `.array (vs.map .lit)` to `.lit (.vArray vs)`), and
+  `sArrayErr` (propagate a panic out of an array, as the binop rules do). A
+  fully-evaluated array is *not* an `IsValue` — it always steps via `sArrayVal`
+  to the array literal, which is the value. (This is cleaner than Coq, where a
+  `map ELit`-array is simultaneously a value *and* steppable, forcing extra
+  array-equality step rules; in Lean, array equality reuses the generic
+  `.lit`-equality rules after normalisation.)
+- **Proofs:** `progress` and `preservation` cover all three step rules,
+  `sorry`-free and axiom-free under Lean 4.30.0. The helper `array_split`
+  does the pure-list "all-literals vs. prefix + first non-literal" split
+  (the analogue of Coq's `array_elements_progress`).
+- **Method note:** Lean's `∀ e ∈ es` premise yields a per-element induction
+  hypothesis directly from `induction`, so the Lean `progress` needs **no
+  well-founded recursion on an `expr_size` measure** — the device the Coq
+  proof requires because Coq's `Forall`-based scheme does not recurse into the
+  nested `has_type`s. The two developments now prove the same array results by
+  different means.
 
 ## Coq proofs (`WokeLang.v`) — audited 2026-06-14
 
@@ -178,10 +206,16 @@ treatment as the Lean file.
   axioms beyond those implicit in `Coq.Reals`"). Consistent, standard, honest.
 
 - **Coverage vs. the Lean file.** Complementary, not identical:
-  - Coq is **ahead on arrays** — full `T_Array`/`T_Lit_Array`, array stepping
-    (`S_Array_step`/`S_Array_val`), and a `progress` that uses **well-founded
-    induction on `expr_size`** to get an IH for array elements. (This is exactly
-    the Tier-1 item still open on the Lean side.)
+  - Arrays are **now at parity** (Lean caught up 2026-06-18): both have
+    `T_Array`/`T_Lit_Array` (Coq) ⟷ `tArray`/`tArrayVal` (Lean) and array
+    stepping. The proofs differ in method: Coq's `progress` uses **well-founded
+    induction on `expr_size`** to get an IH for array elements (its
+    `Forall`-based induction scheme does not recurse into the nested
+    `has_type`s); Lean phrases the premise as `∀ e ∈ es`, which yields the
+    per-element IH directly, so no size measure is needed. Coq additionally
+    treats a `map ELit`-array as a value (needing extra array-equality step
+    rules); Lean normalises arrays to a `.vArray` literal first and reuses
+    generic `.lit`-equality.
   - Coq models floats as `ℝ` ⇒ `value_eq_dec` is fully decidable (`Req_EM_T`),
     at the cost of the classical-reals axioms above. (Lean models `Float` as
     opaque IEEE and decides equality classically via `by_cases`.)

docs/proofs/verification/WokeLang.lean

@@ -35,6 +35,17 @@
   - preservation: stepping preserves types
   - type_safety: multi-step evaluation preserves types (by induction + preservation)
   - consent_monotonicity / consent_preservation: consent system properties
+
+  ### Arrays (parity with Coq's WokeLang.v):
+  `tArray` / `tArrayVal` type array expressions and array literal values
+  (the mirror of Coq's `T_Array` / `T_Lit_Array`); `Step` gains `sArrayStep`
+  (left-most-element congruence), `sArrayVal` (normalise a fully-evaluated
+  array to a `.vArray` literal value), and `sArrayErr` (panic propagation).
+  `progress` and `preservation` cover all three. The `∀ e ∈ es` premise shape
+  yields a per-element induction hypothesis directly, so — unlike the Coq
+  development — no well-founded recursion on an expression-size measure is
+  needed: `array_split` does the pure-list decomposition and the IH answers
+  value-or-steps per element.
 -/
 
 namespace WokeLang
@@ -221,6 +232,18 @@ inductive HasType : TypeEnv → Expr → WokeType → Prop where
       HasType Γ (.unwrap e) tOk
   | tError : ∀ Γ msg t,
       HasType Γ (.error msg) t
+  -- Arrays (mirror of Coq's `T_Array` / `T_Lit_Array` in WokeLang.v).
+  -- `tArray` types an array *expression* elementwise; `tArrayVal` types a
+  -- fully-evaluated array *literal value*. Both premises use the `∀ e ∈ es`
+  -- shape, which (unlike Coq's `Forall`) yields a per-element induction
+  -- hypothesis directly from `induction`, so the `progress`/`preservation`
+  -- array cases need no well-founded recursion on an `expr_size` measure.
+  | tArray : ∀ Γ es t,
+      (∀ e, e ∈ es → HasType Γ e t) →
+      HasType Γ (.array es) (.array t)
+  | tArrayVal : ∀ Γ vs t,
+      (∀ v, v ∈ vs → HasType Γ (.lit v) t) →
+      HasType Γ (.lit (.vArray vs)) (.array t)
 
 -- =========================================================================
 -- 4. Operational Semantics
@@ -332,6 +355,20 @@ inductive Step : Expr → Env → Expr → Env → Prop where
       Step (.oops (.error msg)) ρ (.error msg) ρ
   | sUnwrapErr : ∀ msg ρ,
       Step (.unwrap (.error msg)) ρ (.error msg) ρ
+  -- Array evaluation (mirror of Coq's `S_Array_step` / `S_Array_val`, plus
+  -- panic propagation). `sArrayStep` reduces the left-most non-value element;
+  -- `sArrayVal` normalises a fully-evaluated array to an array literal value;
+  -- `sArrayErr` propagates a panic out of an array, as the binop rules do.
+  -- A fully-evaluated array is *not* an `IsValue` (it always steps via
+  -- `sArrayVal`); the `IsValue` is the resulting `.lit (.vArray vs)`.
+  | sArrayStep : ∀ (vs : List Value) (e e' : Expr) (es : List Expr) (ρ ρ' : Env),
+      Step e ρ e' ρ' →
+      Step (.array (vs.map Expr.lit ++ e :: es)) ρ
+           (.array (vs.map Expr.lit ++ e' :: es)) ρ'
+  | sArrayVal : ∀ (vs : List Value) (ρ : Env),
+      Step (.array (vs.map Expr.lit)) ρ (.lit (.vArray vs)) ρ
+  | sArrayErr : ∀ (vs : List Value) (msg : String) (es : List Expr) (ρ : Env),
+      Step (.array (vs.map Expr.lit ++ .error msg :: es)) ρ (.error msg) ρ
 
 /-- Multi-step reduction (reflexive transitive closure) -/
 inductive MultiStep : Expr → Env → Expr → Env → Prop where
@@ -386,6 +423,40 @@ theorem canonical_forms_result : ∀ v tOk tErr,
   | tOkayVal _ _ h₁ => left; exact ⟨_, rfl⟩
   | tOopsVal _ _ => right; exact ⟨_, rfl⟩
 
+/-- `isLitB e` is `true` exactly when `e` is a literal-value expression.
+    Used by `array_split` to locate the left-most non-literal array element. -/
+def isLitB : Expr → Bool
+  | .lit _ => true
+  | _ => false
+
+theorem isLitB_true {e : Expr} : isLitB e = true → ∃ v, e = .lit v := by
+  cases e <;> simp [isLitB]
+
+theorem isLitB_false {e : Expr} : isLitB e = false → ∀ v, e ≠ .lit v := by
+  cases e <;> simp [isLitB]
+
+/-- A list of expressions is either all literal values, or splits as a prefix
+    of literal values, a left-most non-literal element, and a remainder. This
+    is the Lean analogue of Coq's `array_elements_progress` decomposition;
+    here it is pure list reasoning, with the "is it a value or does it step?"
+    question deferred to the per-element IH in the `tArray` progress case. -/
+theorem array_split (es : List Expr) :
+    (∃ vs : List Value, es = vs.map Expr.lit) ∨
+    (∃ (vs : List Value) (e : Expr) (rest : List Expr),
+        es = vs.map Expr.lit ++ e :: rest ∧ ∀ v, e ≠ .lit v) := by
+  induction es with
+  | nil => left; exact ⟨[], rfl⟩
+  | cons hd tl ih =>
+    cases hb : isLitB hd with
+    | true =>
+      obtain ⟨v, rfl⟩ := isLitB_true hb
+      cases ih with
+      | inl h => obtain ⟨vs, rfl⟩ := h; left; exact ⟨v :: vs, rfl⟩
+      | inr h => obtain ⟨vs, e, rest, rfl, hne⟩ := h
+                 right; exact ⟨v :: vs, e, rest, rfl, hne⟩
+    | false =>
+      right; exact ⟨[], hd, tl, rfl, isLitB_false hb⟩
+
 /-- 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,
     modelling WokeLang's panic semantics for unwrapping failures. -/
@@ -838,6 +909,32 @@ theorem progress : ∀ e t,
   | tError msg _ =>
     -- Error expressions are terminal values (panics).
     left; exact .error msg
+  | tArray es t hall ih =>
+    -- An array expression is never a value: it either normalises (all
+    -- elements are literals ⇒ sArrayVal), propagates a panic (left-most
+    -- non-literal is an error ⇒ sArrayErr), or steps its left-most
+    -- non-literal element (⇒ sArrayStep). The per-element progress IH `ih`
+    -- discharges the last two via `array_split`.
+    right
+    cases array_split es with
+    | inl hsplit =>
+      obtain ⟨vs, rfl⟩ := hsplit
+      exact ⟨.lit (.vArray vs), emptyEnv, .sArrayVal vs emptyEnv⟩
+    | inr hsplit =>
+      obtain ⟨vs, e, rest, rfl, hne⟩ := hsplit
+      have hin : e ∈ vs.map Expr.lit ++ e :: rest := by simp
+      cases ih e hin with
+      | inl hv =>
+        cases hv with
+        | lit v => exact absurd rfl (hne v)
+        | error msg => exact ⟨.error msg, emptyEnv, .sArrayErr vs msg rest emptyEnv⟩
+      | inr hstp =>
+        obtain ⟨e', ρ', hs⟩ := hstp
+        exact ⟨.array (vs.map Expr.lit ++ e' :: rest), ρ',
+               .sArrayStep vs e e' rest emptyEnv ρ' hs⟩
+  | tArrayVal vs t hall ih =>
+    -- A fully-evaluated array literal `.lit (.vArray vs)` is a value.
+    left; constructor
 
 /-- Preservation theorem: if a well-typed expression steps, the result is well-typed.
     Proof by induction on the Step derivation with inversion on the typing derivation.
@@ -1036,6 +1133,26 @@ theorem preservation : ∀ e e' t ρ ρ',
   | sUnwrapErr msg _ =>
     cases ht with
     | tUnwrap _ tOk tErr h₁ => exact .tError _ msg _
+  | sArrayStep vs e e' rest ρ ρ' hs ih =>
+    -- Congruence: the stepped element keeps its type (by the IH); every other
+    -- element keeps the witness it had from the original `tArray` derivation.
+    cases ht with
+    | tArray _ t' hall =>
+      refine .tArray _ _ t' (fun x hx => ?_)
+      rcases List.mem_append.1 hx with hpre | hcons
+      · exact hall x (List.mem_append.2 (Or.inl hpre))
+      · rcases List.mem_cons.1 hcons with rfl | htail
+        · exact ih t' (hall e (List.mem_append.2 (Or.inr List.mem_cons_self)))
+        · exact hall x (List.mem_append.2 (Or.inr (List.mem_cons_of_mem _ htail)))
+  | sArrayVal vs ρ =>
+    -- Normalisation: `.array (vs.map lit) : array t'` becomes the literal value
+    -- `.lit (.vArray vs) : array t'`, re-typed via `tArrayVal`.
+    cases ht with
+    | tArray _ t' hall =>
+      exact .tArrayVal _ vs t' (fun v hv => hall (Expr.lit v) (List.mem_map.2 ⟨v, hv, rfl⟩))
+  | sArrayErr vs msg rest ρ =>
+    -- Panic propagation: the result `.error msg` is well-typed at any type.
+    exact .tError _ msg _
 
 /-- Type safety theorem -/
 theorem type_safety : ∀ e t v ρ,