diff --git a/docs/plans/loop-recur.2.md b/docs/plans/loop-recur.2.md
new file mode 100644
index 0000000..b93b592
--- /dev/null
+++ b/docs/plans/loop-recur.2.md
@@ -0,0 +1,1035 @@
+# loop-recur.2 — Typecheck Semantics (Component 4) — Implementation Plan
+
+> **Parent spec:** `docs/specs/2026-05-17-loop-recur.md`
+>
+> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
+> to run this plan. Steps use `- [ ]` checkboxes for tracking.
+
+**Goal:** Replace the iter-1 `synth` `CheckError::Internal` stub for
+`Term::Loop` / `Term::Recur` with real typecheck semantics — binder
+typing, positional `recur` arity + per-arg type checking via a
+`loop_stack` frame, a new private `verify_loop_body` tail-position
+pass, and the four `Recur*` diagnostics — so a `sum_to`-class loop
+program passes `ail check` and the four negatives fire point-exactly.
+
+**Architecture:** `synth` gains a `loop_stack: &mut Vec<Vec<Type>>`
+param threaded exactly as mut.2's `mut_scope_stack` (stack of
+*ordered binder-type vectors* — `recur` is positional, not
+name-keyed, so unlike `mut` the frame is not an `IndexMap`; binder
+*names* enter the ordinary `locals` scope exactly as `Term::Let`
+binds its name). `Term::Loop` synths each binder init (later inits
++ body see earlier binder names via `locals`), pushes the ordered
+binder types onto `loop_stack`, synths the body (loop's static type
+= body's type), pops. `Term::Recur` reads `loop_stack.last()`:
+empty → `RecurOutsideLoop`; arg-count ≠ binder-count →
+`RecurArityMismatch`; per-arg subst-compare ≠ binder type →
+`RecurTypeMismatch` (Assign-style structural pre-check, NOT
+`unify`-propagate — see Boss call 1); `recur`'s own result is a
+fresh metavar (it transfers control, never falls through). A NEW
+private `verify_loop_body` (sibling of the spec-frozen
+`verify_tail_positions`) enforces `recur` only in tail position of
+its enclosing loop body (`RecurNotInTailPosition`); it runs in
+`check_fn` *after* `synth`, so `RecurOutsideLoop`/arity/type (synth)
+take code-precedence over the tail-position code by construction.
+
+**Tech Stack:** `ailang-check` (lib.rs — `CheckError`, `code`,
+`ctx`, `synth`, `check_fn`, new `verify_loop_body`); `examples/`
+(4 negative `.ail.json` fixtures + 1 positive `.ail`);
+`ailang-core/tests/carve_out_inventory.rs`; new
+`ailang-check/tests/loop_recur_typecheck_pin.rs`;
+`ail/tests/ct1_check_cli.rs`.
+
+---
+
+## Boss design calls baked into this plan (settled — do not re-litigate)
+
+1. **`RecurTypeMismatch` is an Assign-style structural pre-check,
+   not a `unify`-propagate.** The recon found two in-file
+   precedents: mut.2 `Term::Mut`-init lets `unify(&v.ty,&init_ty,
+   subst)?` propagate its own `CheckError::TypeMismatch` (code
+   `type-mismatch`); mut.2 `Term::Assign` does NOT — it synths the
+   value, `subst.apply`s both sides, structurally compares
+   `applied_declared != applied_value`, and catch-wraps into the
+   dedicated `AssignTypeMismatch`. The spec §"Error handling" +
+   §"Acceptance criteria" mandate a dedicated `recur-type-mismatch`
+   code that fires *point-exactly* on its negative fixture. Only
+   the Assign-style mechanism satisfies that (a `unify`-propagate
+   would surface `type-mismatch`, failing the acceptance). So
+   `Term::Recur` per-arg checking mirrors the `Term::Assign` arm
+   (`lib.rs:3716-3730`) verbatim in mechanism: synth the arg,
+   `subst.apply` both the arg type and the binder type, structural
+   `!=`, on mismatch `Err(RecurTypeMismatch{position,expected,got})`.
+   Rationale is semantic (one in-repo mechanism for "declared-vs-
+   actual at a binding site with its own point-exact code",
+   consistent with `AssignTypeMismatch`), not effort.
+
+2. **`loop_stack` element type is `Vec<Type>` (ordered binder
+   types), NOT `IndexMap<String,Type>`.** mut.2's
+   `mut_scope_stack: Vec<IndexMap<String,Type>>` is name-keyed
+   because `assign`/`var` resolve mut-vars *by name*. `recur` has
+   no by-name rebinding — it rebinds binders *positionally*. The
+   frame must model exactly what `Term::Recur` consumes: the
+   ordered binder types, for arity (`.len()`) and per-position type
+   checks. Binder *names* enter the ordinary `locals: &mut
+   IndexMap<String,Type>` exactly as `Term::Let` binds its name
+   (`lib.rs:3205-3218` is the verbatim precedent) so later inits
+   and the body resolve them through the normal locals/globals
+   chain. The spec phrase "threaded exactly as mut.2's
+   `mut_scope_stack`" governs the *threading discipline* (a
+   `&mut Vec<…>` pushed/popped around the body, passed through
+   every recursive `synth`), not the element type. Semantic, not
+   effort.
+
+3. **Diagnostic-code precedence is by pass ordering, already
+   correct.** `RecurOutsideLoop` / `RecurArityMismatch` /
+   `RecurTypeMismatch` are raised in `synth` (runs at
+   `check_fn:1970`); `RecurNotInTailPosition` is raised in the new
+   `verify_loop_body` (runs after, analogous to
+   `verify_tail_positions` at `check_fn:1980`). A `recur` outside
+   any loop therefore fires `RecurOutsideLoop` (synth, first), not
+   `RecurNotInTailPosition` — exactly the spec-correct code. No
+   explicit ordering logic is needed; the pass sequence is the
+   mechanism. `verify_loop_body` is entered only on synth success,
+   so by then every `recur` is known to be inside a loop with
+   matching arity/types; the pass adds only the tail rule.
+
+---
+
+## Files this plan creates or modifies
+
+- Modify: `crates/ailang-check/src/lib.rs`
+  - `:705`-area — 4 new `CheckError` variants (after
+    `MutVarCapturedByLambda` `:697`, before `Internal` `:703`).
+  - `:751`-area — 4 new `code()` arms (after
+    `MutVarCapturedByLambda` `:750`).
+  - `:824`-area — 2 new `ctx()` arms (after
+    `MutVarCapturedByLambda` `:822-824`, before the `_ =>`
+    catch-all `:825`).
+  - `:2772` — `synth` signature: add `loop_stack` param.
+  - 22 internal recursive `synth(...)` call sites + `:1970`
+    (check_fn) + `:2748` (check_const) + test-module callers —
+    thread `loop_stack` (build-gated; see Task 2).
+  - `:3740-3742` — replace the iter-1 Loop/Recur `Internal` stub
+    with the two real arms.
+  - `:1969`-adjacent + `:1970` + after `:1980` (check_fn) —
+    declare `loop_stack`, thread into the synth call, invoke
+    `verify_loop_body`.
+  - new private `fn verify_loop_body` (place immediately after
+    `verify_tail_positions`, which ends `:2725`).
+- Create: `examples/test_recur_outside_loop.ail.json`
+- Create: `examples/test_recur_arity_mismatch.ail.json`
+- Create: `examples/test_recur_type_mismatch.ail.json`
+- Create: `examples/test_recur_not_in_tail_position.ail.json`
+- Reuse (no new file): `examples/loop_sum_to.ail` (shipped iter-1
+  as the round-trip fixture) — now also the positive `ail check`
+  evidence: it returned the `Internal` stub in iter-1, must
+  typecheck clean in iter-2. One fixture, two properties
+  (round-trips AND typechecks); no near-duplicate is created.
+- Create: `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`
+  (mirror of `mut_typecheck_pin.rs`).
+- Modify: `crates/ailang-core/tests/carve_out_inventory.rs:6-40`
+  (header prose refresh + 4 `EXPECTED` entries; 13 → 17).
+- Modify: `crates/ail/tests/ct1_check_cli.rs` — add a sibling
+  `check_human_mode_renders_recur_diagnostic_code_exactly_once`.
+- No edit: `verify_tail_positions` (`:2607-2725`, spec-frozen
+  tail-app role — its iter-1 Loop/Recur descent arms stay);
+  the drift trio (`design_schema_drift`/`spec_drift`/
+  `schema_coverage` — iter-2 adds no schema); `round_trip.rs`
+  (auto-discovers `.ail` only; negatives are `.ail.json` carve-
+  outs, exempt by construction).
+
+---
+
+## Task 1: The four `Recur*` `CheckError` variants + `code()` + `ctx()`
+
+**Files:** Modify `crates/ailang-check/src/lib.rs`
+
+- [ ] **Step 1: Write the failing code() unit test**
+
+In `crates/ailang-check/src/lib.rs`, in the `#[cfg(test)] mod
+tests` (near the mut-family unit tests), add:
+
+```rust
+    #[test]
+    fn recur_checkerror_codes_are_exact() {
+        assert_eq!(CheckError::RecurOutsideLoop.code(), "recur-outside-loop");
+        assert_eq!(
+            CheckError::RecurArityMismatch { expected: 2, got: 1 }.code(),
+            "recur-arity-mismatch"
+        );
+        assert_eq!(
+            CheckError::RecurTypeMismatch {
+                position: 0,
+                expected: "Int".into(),
+                got: "Bool".into(),
+            }
+            .code(),
+            "recur-type-mismatch"
+        );
+        assert_eq!(
+            CheckError::RecurNotInTailPosition.code(),
+            "recur-not-in-tail-position"
+        );
+    }
+```
+
+- [ ] **Step 2: Run test to verify it fails to compile**
+
+Run: `cargo test -p ailang-check --lib recur_checkerror_codes_are_exact 2>&1 | tail -5`
+Expected: FAIL — `error[E0599]: no variant ... RecurOutsideLoop` etc.
+
+- [ ] **Step 3: Add the four variants**
+
+In `crates/ailang-check/src/lib.rs`, immediately after the
+`MutVarCapturedByLambda { name: String }` variant (ends `:697`),
+before the `/// Iter 22b.3 …` doc + `Internal(String)` (`:699-704`),
+add (bracket-`[code]`-free `#[error(...)]`, F2 convention,
+mirroring the mut.2 variant style at `:661-697`):
+
+```rust
+    /// loop-recur iter 2: `Term::Recur` reached typecheck with no
+    /// lexically-enclosing `Term::Loop` (the `loop_stack` was empty).
+    #[error("`recur` is only valid inside a `loop` — there is no enclosing loop here")]
+    RecurOutsideLoop,
+
+    /// loop-recur iter 2: `Term::Recur`'s argument count differs from
+    /// the enclosing loop's binder count. `recur` rebinds every loop
+    /// binder positionally, so the counts must match exactly.
+    #[error("`recur` passes {got} argument(s) but the enclosing loop has {expected} binder(s) — recur must rebind every binder positionally")]
+    RecurArityMismatch { expected: usize, got: usize },
+
+    /// loop-recur iter 2: a `recur` argument's type differs from the
+    /// corresponding loop binder's declared type (0-based position).
+    #[error("`recur` argument {position} has type `{got}` but the enclosing loop's binder at that position is `{expected}` — every recur argument must match its binder's type")]
+    RecurTypeMismatch {
+        position: usize,
+        expected: String,
+        got: String,
+    },
+
+    /// loop-recur iter 2: `Term::Recur` appears somewhere other than
+    /// the tail position of its enclosing loop body. `recur` is a
+    /// structural back-jump; it cannot be a sub-expression.
+    #[error("`recur` must be in tail position of its enclosing `loop` body — it is a back-jump, not a value-producing sub-expression")]
+    RecurNotInTailPosition,
+```
+
+- [ ] **Step 4: Add the four `code()` arms**
+
+In `pub fn code(&self)`'s `match self`, immediately after
+`CheckError::MutVarCapturedByLambda { .. } => "mut-var-captured-by-lambda",`
+(`:750`), before `CheckError::Internal(_) => "internal",` (`:751`),
+add:
+
+```rust
+            CheckError::RecurOutsideLoop => "recur-outside-loop",
+            CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch",
+            CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch",
+            CheckError::RecurNotInTailPosition => "recur-not-in-tail-position",
+```
+
+- [ ] **Step 5: Add the two `ctx()` arms**
+
+In `pub fn ctx(&self)`'s `match self`, immediately after
+`CheckError::MutVarCapturedByLambda { name } => { … }` (ends
+`:824`), before the `_ => serde_json::Value::Object(...)`
+catch-all (`:825`), add (arity mirrors the `ArityMismatch`
+`{expected, actual}` precedent at `:763-765`; type mirrors
+`AssignTypeMismatch`'s `{name?,expected,actual}` shape at
+`:816-818` but positional; `RecurOutsideLoop` /
+`RecurNotInTailPosition` deliberately use the `{}` catch-all —
+no actionable structured context beyond the message):
+
+```rust
+            CheckError::RecurArityMismatch { expected, got } => {
+                serde_json::json!({"expected": expected, "actual": got})
+            }
+            CheckError::RecurTypeMismatch { position, expected, got } => {
+                serde_json::json!({"position": position, "expected": expected, "actual": got})
+            }
+```
+
+- [ ] **Step 6: Run the code() test to verify it passes**
+
+Run: `cargo test -p ailang-check --lib recur_checkerror_codes_are_exact 2>&1 | tail -5`
+Expected: PASS — `test result: ok. 1 passed`. (The crate compiles:
+`code()` is exhaustive and now has all four arms; the `synth`
+Loop/Recur stub still returns `Internal` and does not yet use the
+new variants — that is Task 3.)
+
+---
+
+## Task 2: `synth` signature + `loop_stack` threading
+
+**Files:** Modify `crates/ailang-check/src/lib.rs`
+
+Pure mechanical param threading. The `synth` Loop/Recur arm is
+still the iter-1 `Internal` stub after this task (it does not
+reference `loop_stack`), so the crate compiles once threading is
+complete. The compiler is the exhaustive completeness oracle: a
+missed caller is a hard `error[E0061] this function takes N
+arguments`.
+
+- [ ] **Step 1: Add the `loop_stack` parameter to `synth`**
+
+In `pub(crate) fn synth(`, immediately after the
+`mut_scope_stack: &mut Vec<IndexMap<String, Type>>,` parameter
+(`:2772`), add:
+
+```rust
+    // loop-recur iter 2: per-walk loop-binder-type stack. Each frame
+    // is one `Term::Loop`'s binder types in declaration order
+    // (positional — `recur` rebinds binders by position, not name,
+    // so this is `Vec<Type>` not name-keyed like `mut_scope_stack`).
+    // Pushed on `Term::Loop` body entry, popped on exit; consulted
+    // innermost-first by `Term::Recur` for arity + per-position type.
+    // Position: mut_scope_stack-adjacent — both are per-fn-body
+    // lexical-control scope state threaded identically.
+    loop_stack: &mut Vec<Vec<Type>>,
+```
+
+- [ ] **Step 2: Thread `loop_stack` at every recursive call site**
+
+The threading rule is uniform: in every `synth(...)` call, insert
+the `loop_stack` argument **immediately after the `mut_scope_stack`
+argument** (positionally matching the signature). For the 22
+recursive call sites inside `fn synth` (the in-scope `loop_stack`
+param is threaded through): `:3161`, `:3197`, `:3206`, `:3208`,
+`:3220`, `:3222`, `:3223`, `:3241`, `:3336`, `:3345`, `:3363`,
+`:3438`, `:3440`, `:3474`, `:3562`, `:3589`, `:3605`, `:3619`,
+`:3649`, and the three multi-line calls headed at `:3674`,
+`:3683`, `:3717`. Example transform (the `Term::Let` arm at
+`:3206`/`:3208`):
+
+```rust
+// before:
+let v = synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+// after:
+let v = synth(value, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+```
+
+- [ ] **Step 3: Thread `loop_stack` at the external (non-recursive) callers**
+
+- `check_fn` `:1970`: handled in Task 4 Step 4 (it declares its
+  own fresh `loop_stack`).
+- `check_const` `:2748`: a const value has no enclosing loop.
+  Immediately before the `synth(&c.value, …)` call, add
+  `let mut loop_stack: Vec<Vec<Type>> = Vec::new();` and pass
+  `&mut loop_stack` immediately after `&mut mut_scope_stack` in
+  that call. (Any `recur` in a const value then correctly fires
+  `RecurOutsideLoop`.)
+
+- [ ] **Step 4: Build-gated completeness sweep**
+
+Run: `cargo build -p ailang-check 2>&1 | grep -E 'this function takes|error\[E0061\]' | sort -u`
+Expected first run: a list of remaining `synth(...)` callers in
+the `#[cfg(test)]` module (the `let err = synth(`/`let ty = synth(`/
+`let _ = synth(` sites the recon located at `:4123`, `:4165`,
+`:4208`, `:4313`, `:4353`, `:4392`, `:4494`, `:7233`). For each:
+these are loop-free unit-test call sites — insert a
+`let mut loop_stack: Vec<Vec<Type>> = Vec::new();` before the call
+(or reuse one already in scope) and pass `&mut loop_stack`
+immediately after the `mut_scope_stack`/`&mut mut_scope_stack`
+argument, exactly as Step 3.
+
+Re-run the command until it prints nothing.
+Then run: `cargo build -p ailang-check 2>&1 | tail -2`
+Expected: PASS — `Finished` (0 errors). The threading is
+complete iff the crate compiles; this is the exhaustive gate.
+
+- [ ] **Step 5: Confirm the suite still green (stub intact)**
+
+Run: `cargo test -p ailang-check --lib 2>&1 | grep -E '^test result:' | tail -1`
+Expected: PASS — the `synth` Loop/Recur arm is still the iter-1
+`Internal` stub (unchanged); no behaviour changed, only an unused
+threaded param was added.
+
+---
+
+## Task 3: Real `synth` `Term::Loop` + `Term::Recur` arms
+
+**Files:** Modify `crates/ailang-check/src/lib.rs`
+
+- [ ] **Step 1: Write the failing positive-typecheck pin**
+
+Create `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`
+with the harness mirrored verbatim from `mut_typecheck_pin.rs`
+(same `examples_dir()` + `check_fixture()` helpers) and this first
+test:
+
+```rust
+//! loop-recur iter 2: pin tests that the loop/recur typecheck
+//! fixtures produce the expected diagnostic codes (or zero
+//! diagnostics for the positive sum_to-class case). Mirrors
+//! `mut_typecheck_pin.rs`; negative fixtures live as `.ail.json`
+//! so the diagnostic code is the load-bearing assertion.
+
+use ailang_check::check_workspace;
+use ailang_surface::load_workspace;
+use std::path::PathBuf;
+
+fn examples_dir() -> PathBuf {
+    let manifest = env!("CARGO_MANIFEST_DIR");
+    PathBuf::from(manifest)
+        .parent().expect("crates/ailang-check parent")
+        .parent().expect("crates/ parent")
+        .join("examples")
+}
+
+fn check_fixture(fixture_name: &str) -> Vec<String> {
+    let path = examples_dir().join(fixture_name);
+    let ws = load_workspace(&path)
+        .unwrap_or_else(|e| panic!("workspace `{fixture_name}` must load: {e:?}"));
+    let diags = check_workspace(&ws);
+    diags.iter().map(|d| d.code.clone()).collect()
+}
+
+#[test]
+fn loop_sum_to_typechecks_clean() {
+    // examples/loop_sum_to.ail shipped in iter-1 as the round-trip
+    // fixture; in iter-2 it must ALSO typecheck clean (it returned
+    // the synth Internal stub in iter-1). One fixture, two
+    // properties — no near-duplicate corpus file.
+    let codes = check_fixture("loop_sum_to.ail");
+    assert!(codes.is_empty(), "expected zero diagnostics, got {codes:?}");
+}
+```
+
+(The four negative tests are added in Task 5 Step 4 — same file.)
+
+- [ ] **Step 2: Run the positive pin RED (no fixture creation — reuse iter-1's)**
+
+`examples/loop_sum_to.ail` already exists (shipped iter-1,
+commit `a179ec3`); do NOT create a new fixture.
+
+Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin loop_sum_to_typechecks_clean 2>&1 | tail -6`
+Expected: FAIL — `codes == ["internal"]` (the iter-1 `synth`
+Loop/Recur stub returns `CheckError::Internal`; `ail check`
+surfaces it as code `internal`, so the list is non-empty).
+
+- [ ] **Step 3: Replace the `Internal` stub with the real arms**
+
+In `crates/ailang-check/src/lib.rs`, replace the iter-1 stub
+(`:3740-3742`, verbatim):
+
+```rust
+        Term::Loop { .. } | Term::Recur { .. } => Err(CheckError::Internal(
+            "Term::Loop/Term::Recur typecheck lands in loop-recur iter 2".into(),
+        )),
+```
+
+with the two real arms (binder-name scoping mirrors the
+`Term::Let` arm `:3205-3218` verbatim; per-arg type check mirrors
+the `Term::Assign` arm `:3716-3730` verbatim per Boss call 1;
+fresh metavar via `Subst::fresh(counter)` per `:57-61` /
+`:3038`):
+
+```rust
+        // loop-recur iter 2: each binder init is synthed in the
+        // outer scope plus already-declared binder names of THIS
+        // loop (declaration order; later inits + body see earlier
+        // binders via `locals`, exactly as `Term::Let` binds its
+        // name). The loop's static type is the body's type. The
+        // ordered binder types are pushed onto `loop_stack` for the
+        // body walk so an inner `Term::Recur` can position-check
+        // against them; popped on exit. Binder names are NOT in
+        // `loop_stack` (recur is positional, not by-name).
+        Term::Loop { binders, body } => {
+            let mut binder_tys: Vec<Type> = Vec::new();
+            let mut restore: Vec<(String, Option<Type>)> = Vec::new();
+            for b in binders {
+                let init_ty = synth(
+                    &b.init, env, locals, mut_scope_stack, loop_stack, effects,
+                    in_def, subst, counter, residuals, free_fn_calls, warnings,
+                )?;
+                unify(&b.ty, &init_ty, subst)?;
+                binder_tys.push(b.ty.clone());
+                let prev = locals.insert(b.name.clone(), b.ty.clone());
+                restore.push((b.name.clone(), prev));
+            }
+            loop_stack.push(binder_tys);
+            let body_result = synth(
+                body, env, locals, mut_scope_stack, loop_stack, effects,
+                in_def, subst, counter, residuals, free_fn_calls, warnings,
+            );
+            loop_stack.pop();
+            for (name, prev) in restore.into_iter().rev() {
+                match prev {
+                    Some(p) => {
+                        locals.insert(name, p);
+                    }
+                    None => {
+                        locals.shift_remove(&name);
+                    }
+                }
+            }
+            body_result
+        }
+        // loop-recur iter 2: recur re-enters the innermost enclosing
+        // loop, rebinding its binders positionally. RecurOutsideLoop
+        // when `loop_stack` is empty; RecurArityMismatch on count
+        // disagreement; RecurTypeMismatch via the Assign-style
+        // subst-apply-then-structural-compare (Boss call 1) so the
+        // dedicated code fires point-exactly. recur's OWN type is a
+        // fresh metavar — it transfers control and never falls
+        // through, so it unifies with whatever sibling branch the
+        // enclosing if/match requires.
+        Term::Recur { args } => {
+            let binder_tys = match loop_stack.last() {
+                None => return Err(CheckError::RecurOutsideLoop),
+                Some(tys) => tys.clone(),
+            };
+            if args.len() != binder_tys.len() {
+                return Err(CheckError::RecurArityMismatch {
+                    expected: binder_tys.len(),
+                    got: args.len(),
+                });
+            }
+            for (i, a) in args.iter().enumerate() {
+                let arg_ty = synth(
+                    a, env, locals, mut_scope_stack, loop_stack, effects,
+                    in_def, subst, counter, residuals, free_fn_calls, warnings,
+                )?;
+                let applied_binder = subst.apply(&binder_tys[i]);
+                let applied_arg = subst.apply(&arg_ty);
+                if applied_binder != applied_arg {
+                    return Err(CheckError::RecurTypeMismatch {
+                        position: i,
+                        expected: ailang_core::pretty::type_to_string(&applied_binder),
+                        got: ailang_core::pretty::type_to_string(&applied_arg),
+                    });
+                }
+            }
+            Ok(Subst::fresh(counter))
+        }
+```
+
+- [ ] **Step 4: Run the positive pin to verify it passes**
+
+Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin loop_sum_to_typechecks_clean 2>&1 | tail -6`
+Expected: PASS — zero diagnostics (binder typing succeeds; `recur`
+arity 2 == 2 binders, both `Int`, fresh-metavar result unifies
+with the `if`'s `acc` branch which is `Int`).
+
+---
+
+## Task 4: `verify_loop_body` private pass + `check_fn` wiring
+
+**Files:** Modify `crates/ailang-check/src/lib.rs`
+
+- [ ] **Step 1: Write the failing tail-position fixture + pin**
+
+Create `examples/test_recur_not_in_tail_position.ail.json` (the
+spec §"Concrete code shapes" `bad_recur` program, canonical JSON;
+envelope mirrors `examples/test_mut_assign_outside_mut.ail.json`):
+
+```json
+{
+  "schema": "ailang/v0",
+  "name": "test_recur_not_in_tail_position",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "bad_recur",
+      "type": {
+        "k": "fn",
+        "params": [ { "k": "con", "name": "Int" } ],
+        "ret": { "k": "con", "name": "Int" },
+        "effects": []
+      },
+      "params": [ "n" ],
+      "doc": "loop-recur iter 2: recur as an argument to + is NOT in tail position -> recur-not-in-tail-position.",
+      "body": {
+        "t": "loop",
+        "binders": [
+          { "name": "i", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } }
+        ],
+        "body": {
+          "t": "app",
+          "fn": { "t": "var", "name": "+" },
+          "args": [
+            { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+            { "t": "recur", "args": [ { "t": "app", "fn": { "t": "var", "name": "+" }, "args": [ { "t": "var", "name": "i" }, { "t": "lit", "lit": { "kind": "int", "value": 1 } } ] } ] }
+          ]
+        }
+      }
+    }
+  ]
+}
+```
+
+Add to `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`:
+
+```rust
+#[test]
+fn recur_not_in_tail_position_emits_recur_not_in_tail_position() {
+    let codes = check_fixture("test_recur_not_in_tail_position.ail.json");
+    assert_eq!(codes, vec!["recur-not-in-tail-position".to_string()]);
+}
+```
+
+Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin recur_not_in_tail_position 2>&1 | tail -6`
+Expected: FAIL — synth accepts it (arity 1 == 1, type `Int`),
+returns a fresh metavar; nothing yet checks tail-position, so
+`codes` is empty (or carries an unrelated code), not
+`["recur-not-in-tail-position"]`.
+
+- [ ] **Step 2: Add the `verify_loop_body` private pass**
+
+In `crates/ailang-check/src/lib.rs`, immediately after
+`pub fn verify_tail_positions` ends (`:2725`), add (structure
+mirrors `verify_tail_positions`; `in_loop_tail` = "this position
+is a tail position of the innermost enclosing loop body", false
+outside any loop or in a non-tail sub-position; runs after synth so
+every `Recur` reached here is already inside a valid loop):
+
+```rust
+/// loop-recur iter 2: enforces that every `Term::Recur` occurs in
+/// tail position of its lexically-innermost enclosing `Term::Loop`
+/// body. A NEW private pass — a *sibling* of
+/// `verify_tail_positions` (which is spec-frozen for its tail-app
+/// role and unchanged). Invoked from `check_fn` *after* `synth`, so
+/// `RecurOutsideLoop`/arity/type (raised in `synth`) take code-
+/// precedence; by the time a `Recur` is reached here it is known to
+/// be inside a loop with matching arity/types — this pass adds only
+/// the tail-position rule. `in_loop_tail` is the loop analogue of
+/// `verify_tail_positions`' `is_tail`, scoped to the innermost loop.
+fn verify_loop_body(t: &Term, in_loop_tail: bool) -> Result<()> {
+    match t {
+        Term::Lit { .. } | Term::Var { .. } => Ok(()),
+        Term::Recur { args } => {
+            if !in_loop_tail {
+                return Err(CheckError::RecurNotInTailPosition);
+            }
+            // recur args are evaluated in non-tail position; a recur
+            // nested inside a recur arg is itself non-tail.
+            for a in args {
+                verify_loop_body(a, false)?;
+            }
+            Ok(())
+        }
+        Term::Loop { binders, body } => {
+            // Binder inits run once on loop entry — not in the
+            // loop's tail scope. The loop body opens a FRESH
+            // innermost-loop tail scope (independent of where the
+            // loop itself sits — the loop's tail scope is intrinsic).
+            for b in binders {
+                verify_loop_body(&b.init, false)?;
+            }
+            verify_loop_body(body, true)
+        }
+        Term::App { callee, args, .. } => {
+            verify_loop_body(callee, false)?;
+            for a in args {
+                verify_loop_body(a, false)?;
+            }
+            Ok(())
+        }
+        Term::Do { args, .. } => {
+            for a in args {
+                verify_loop_body(a, false)?;
+            }
+            Ok(())
+        }
+        Term::Let { value, body, .. } => {
+            verify_loop_body(value, false)?;
+            verify_loop_body(body, in_loop_tail)
+        }
+        Term::If { cond, then, else_ } => {
+            verify_loop_body(cond, false)?;
+            verify_loop_body(then, in_loop_tail)?;
+            verify_loop_body(else_, in_loop_tail)
+        }
+        Term::Seq { lhs, rhs } => {
+            verify_loop_body(lhs, false)?;
+            verify_loop_body(rhs, in_loop_tail)
+        }
+        Term::Match { scrutinee, arms } => {
+            verify_loop_body(scrutinee, false)?;
+            for arm in arms {
+                verify_loop_body(&arm.body, in_loop_tail)?;
+            }
+            Ok(())
+        }
+        Term::Ctor { args, .. } => {
+            for a in args {
+                verify_loop_body(a, false)?;
+            }
+            Ok(())
+        }
+        Term::Lam { body, .. } => {
+            // A `recur` cannot cross a lambda boundary (different
+            // control frame). Reset: a recur inside a lam is outside
+            // every enclosing loop's tail scope — and synth's
+            // loop_stack likewise does not cross the lam, so such a
+            // recur is already a synth `RecurOutsideLoop`.
+            verify_loop_body(body, false)
+        }
+        Term::LetRec { body, in_term, .. } => {
+            verify_loop_body(body, false)?;
+            verify_loop_body(in_term, in_loop_tail)
+        }
+        Term::Clone { value } => verify_loop_body(value, in_loop_tail),
+        Term::ReuseAs { source, body } => {
+            verify_loop_body(source, false)?;
+            verify_loop_body(body, in_loop_tail)
+        }
+        Term::Mut { vars, body } => {
+            for v in vars {
+                verify_loop_body(&v.init, false)?;
+            }
+            verify_loop_body(body, in_loop_tail)
+        }
+        Term::Assign { value, .. } => verify_loop_body(value, false),
+    }
+}
+```
+
+- [ ] **Step 3: Declare `loop_stack` in `check_fn`**
+
+In `check_fn`, immediately after the `mut_scope_stack`
+declaration (`:1969`,
+`let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();`),
+add:
+
+```rust
+    // loop-recur iter 2: fresh per-fn-body loop-binder-type stack.
+    // Empty at fn entry; pushed/popped by `Term::Loop` arms during
+    // the synth walk; discarded after the body type-checks.
+    let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+```
+
+- [ ] **Step 4: Thread `loop_stack` into the `check_fn` synth call + invoke `verify_loop_body`**
+
+In `check_fn`, the `synth(&f.body, …)` call (`:1970`): insert
+`&mut loop_stack,` immediately after `&mut mut_scope_stack,`:
+
+```rust
+// before:
+let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
+// after:
+let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
+```
+
+Immediately after `verify_tail_positions(&f.body, true)?;`
+(`:1980`), add (sibling pass; fn body is not itself inside any
+loop → `false`):
+
+```rust
+    // loop-recur iter 2: recur-in-tail-position verification. Runs
+    // after synth (so RecurOutsideLoop/arity/type take code-
+    // precedence) and alongside verify_tail_positions (sibling, not
+    // a repurpose — verify_tail_positions' tail-app role is frozen).
+    verify_loop_body(&f.body, false)?;
+```
+
+- [ ] **Step 5: Run the tail-position pin to verify it passes**
+
+Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin recur_not_in_tail_position 2>&1 | tail -6`
+Expected: PASS — `codes == ["recur-not-in-tail-position"]` (the
+`recur` is an argument to `+`, a non-tail position).
+
+Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin loop_sum_to_typechecks_clean 2>&1 | tail -3`
+Expected: PASS — the positive `sum_to` loop still clean (its
+`recur` IS in the `if` else-branch tail).
+
+---
+
+## Task 5: Three remaining negative fixtures + carve-out + ct1 F2 + pin completion
+
+**Files:** Create 3 `.ail.json`; modify
+`carve_out_inventory.rs`, `ct1_check_cli.rs`,
+`loop_recur_typecheck_pin.rs`.
+
+- [ ] **Step 1: Create `test_recur_outside_loop.ail.json`**
+
+```json
+{
+  "schema": "ailang/v0",
+  "name": "test_recur_outside_loop",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" }, "effects": [] },
+      "params": [],
+      "doc": "loop-recur iter 2: recur with no enclosing loop -> recur-outside-loop.",
+      "body": { "t": "recur", "args": [ { "t": "lit", "lit": { "kind": "int", "value": 1 } } ] }
+    }
+  ]
+}
+```
+
+- [ ] **Step 2: Create `test_recur_arity_mismatch.ail.json`**
+
+```json
+{
+  "schema": "ailang/v0",
+  "name": "test_recur_arity_mismatch",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "bad_arity",
+      "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" }, "effects": [] },
+      "params": [],
+      "doc": "loop-recur iter 2: 2 binders, recur passes 1 arg -> recur-arity-mismatch.",
+      "body": {
+        "t": "loop",
+        "binders": [
+          { "name": "a", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } },
+          { "name": "b", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 1 } } }
+        ],
+        "body": { "t": "recur", "args": [ { "t": "var", "name": "a" } ] }
+      }
+    }
+  ]
+}
+```
+
+- [ ] **Step 3: Create `test_recur_type_mismatch.ail.json`**
+
+```json
+{
+  "schema": "ailang/v0",
+  "name": "test_recur_type_mismatch",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "bad_type",
+      "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" }, "effects": [] },
+      "params": [],
+      "doc": "loop-recur iter 2: binder is Int, recur arg is Bool -> recur-type-mismatch.",
+      "body": {
+        "t": "loop",
+        "binders": [
+          { "name": "i", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } }
+        ],
+        "body": { "t": "recur", "args": [ { "t": "lit", "lit": { "kind": "bool", "value": true } } ] }
+      }
+    }
+  ]
+}
+```
+
+- [ ] **Step 4: Complete the pin file**
+
+Append to `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`:
+
+```rust
+#[test]
+fn recur_outside_loop_emits_recur_outside_loop() {
+    let codes = check_fixture("test_recur_outside_loop.ail.json");
+    assert_eq!(codes, vec!["recur-outside-loop".to_string()]);
+}
+
+#[test]
+fn recur_arity_mismatch_emits_recur_arity_mismatch() {
+    let codes = check_fixture("test_recur_arity_mismatch.ail.json");
+    assert_eq!(codes, vec!["recur-arity-mismatch".to_string()]);
+}
+
+#[test]
+fn recur_type_mismatch_emits_recur_type_mismatch() {
+    let codes = check_fixture("test_recur_type_mismatch.ail.json");
+    assert_eq!(codes, vec!["recur-type-mismatch".to_string()]);
+}
+```
+
+Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin 2>&1 | grep -E '^test result:'`
+Expected: PASS — all 5 tests green (1 positive + 4 negatives,
+each code point-exact via `assert_eq!`, non-vacuous).
+
+- [ ] **Step 5: Extend `carve_out_inventory.rs` (13 → 17 + refresh stale header)**
+
+In `crates/ailang-core/tests/carve_out_inventory.rs`, in
+`const EXPECTED`, immediately after the
+`"test_mut_var_captured_by_lambda.ail.json",` line (the
+`// Iter mut.4-tidy` entry), add:
+
+```rust
+    // loop-recur iter 2 — negative typecheck fixtures
+    "test_recur_arity_mismatch.ail.json",
+    "test_recur_not_in_tail_position.ail.json",
+    "test_recur_outside_loop.ail.json",
+    "test_recur_type_mismatch.ail.json",
+```
+
+In the module doc-comment header (`:6-19`), replace the stale
+line `//! Twelve carve-outs post iter mut.2 (2026-05-15):` with:
+
+```
+//! Seventeen carve-outs post iter loop-recur.2 (2026-05-17):
+```
+
+and immediately after the `//! - §C4 (b) compile-time-embed: …`
+bullet block (ends `:19`), add a new bullet:
+
+```
+//! - loop-recur iter 2: 4 negative typecheck fixtures for the
+//!   four `Recur*` diagnostics (recur-outside-loop /
+//!   recur-arity-mismatch / recur-type-mismatch /
+//!   recur-not-in-tail-position) — the diagnostic code is the
+//!   load-bearing assertion, mirroring the §C4(a) / mut.2
+//!   negative-fixture convention.
+```
+
+(The pre-existing "Twelve"-vs-13 mut.4-tidy drift is corrected by
+this same refresh to the true post-iter-2 count of 17.)
+
+Run: `cargo test -p ailang-core --test carve_out_inventory 2>&1 | tail -3`
+Expected: PASS — `examples/*.ail.json` inventory == EXPECTED (17).
+
+- [ ] **Step 6: Add the ct1 F2 human-mode sibling test**
+
+In `crates/ail/tests/ct1_check_cli.rs`, immediately after
+`fn check_human_mode_renders_mut_diagnostic_code_exactly_once`
+(ends ~`:252`), add a sibling (verbatim same body shape, recur
+cases, recur-appropriate name):
+
+```rust
+/// loop-recur iter 2: the four `Recur*` Display bodies must be
+/// bracket-`[code]`-free (F2 convention) — the human-mode
+/// formatter supplies `[<code>]` exactly once. Same observable
+/// property as the mut sibling, over the four recur negatives.
+#[test]
+fn check_human_mode_renders_recur_diagnostic_code_exactly_once() {
+    let cases = [
+        ("test_recur_outside_loop.ail.json", "recur-outside-loop"),
+        ("test_recur_arity_mismatch.ail.json", "recur-arity-mismatch"),
+        ("test_recur_type_mismatch.ail.json", "recur-type-mismatch"),
+        (
+            "test_recur_not_in_tail_position.ail.json",
+            "recur-not-in-tail-position",
+        ),
+    ];
+    for (fixture_name, code) in cases {
+        let fixture = examples_dir().join(fixture_name);
+        let output = Command::new(ail_bin())
+            .args(["check", fixture.to_str().unwrap()])
+            .output()
+            .expect("ail binary must launch");
+        assert!(
+            !output.status.success(),
+            "ail check (human mode) must fail on {fixture_name}"
+        );
+        let stderr = String::from_utf8(output.stderr).expect("stderr is utf-8");
+        let needle = format!("[{code}]");
+        let occurrences = stderr.matches(&needle).count();
+        assert_eq!(
+            occurrences, 1,
+            "expected `[{code}]` exactly once in human stderr, found {occurrences}; \
+             full stderr:\n{stderr}"
+        );
+    }
+}
+```
+
+Run: `cargo test -p ail --test ct1_check_cli check_human_mode_renders_recur 2>&1 | tail -4`
+Expected: PASS — each recur Display body is bracket-free; the
+formatter prefixes `[<code>]` exactly once. (If FAIL with
+"found 2": a Display `#[error(...)]` string in Task 1 Step 3
+wrongly embedded the bracket — it must not; the bodies as
+specified are bracket-free, so this stays green.)
+
+---
+
+## Task 6: Infinite-loop acceptance + full suite + tail-app non-regression
+
+**Files:** Create `examples/loop_forever.ail`; no source changes.
+
+- [ ] **Step 1: Infinite-loop typechecks (no termination claim)**
+
+Create `examples/loop_forever.ail` (a `loop` whose only path is
+`recur` — no non-`recur` exit; must typecheck, asserting the spec
+"no termination claim is made or enforced"):
+
+```
+(module loop_forever
+  (fn spin
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params n)
+    (body
+      (loop (i (con Int) 0)
+        (recur (app + i 1))))))
+```
+
+Add to `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`:
+
+```rust
+#[test]
+fn infinite_loop_typechecks_clean_no_termination_claim() {
+    let codes = check_fixture("loop_forever.ail");
+    assert!(codes.is_empty(), "infinite loop must typecheck (no totality claim), got {codes:?}");
+}
+```
+
+Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin infinite_loop 2>&1 | tail -4`
+Expected: PASS — zero diagnostics. (`recur` is the loop body's
+sole expression = tail position; arity 1 == 1; type `Int`;
+`verify_loop_body` accepts; no guardedness/totality pass exists,
+per spec deliberate boundary. The fn return type `Int` unifies
+with `recur`'s fresh metavar.)
+
+- [ ] **Step 2: Full workspace suite**
+
+Run: `cargo test --workspace 2>&1 | grep -E '^test result: ok' | awk '{p+=$4} END {print p" passed"}'; cargo test --workspace 2>&1 | grep -E 'FAILED|error\[|^test result: FAILED' | head`
+Expected: passed count ≥ the loop-recur.1 baseline (608) + the new
+loop-recur.2 tests; zero `FAILED`/`error[`.
+
+- [ ] **Step 3: `tail-app` non-regression (Boss-call-1 carryover evidence)**
+
+Run: `cargo test --workspace tail 2>&1 | grep -E '^test result:' | tail -4`
+Expected: PASS — every `tail-app`/`tail-do`/`verify_tail_positions`
+test byte-identical (iter-2 added a *sibling* `verify_loop_body`
+and did not touch `verify_tail_positions`; this re-confirms the
+spec's frozen-tail-app-role acceptance criterion).
+
+---
+
+## Acceptance criteria (this iteration)
+
+- `synth` types `Term::Loop` (binder typing; loop type = body type;
+  binder names in `locals` scope for later inits + body) and
+  `Term::Recur` (positional rebinding; fresh-metavar result);
+  the iter-1 `CheckError::Internal` stub is gone.
+- The four `Recur*` codes fire **point-exactly** on their negative
+  fixtures (`assert_eq!`, non-vacuous): `recur-outside-loop`,
+  `recur-arity-mismatch`, `recur-type-mismatch`,
+  `recur-not-in-tail-position`. `recur` outside tail position is a
+  compile error.
+- A `sum_to`-class loop passes `ail check` (it did not in iter-1);
+  an infinite `loop` (no non-`recur` exit) typechecks — **no
+  termination claim is made or enforced**.
+- `verify_tail_positions` / `tail-app` / `tail-do` / Decision 8
+  byte-unchanged (verify_loop_body is a sibling, not a repurpose);
+  NO `Diverge`, NO `verify_structural_recursion`, NO
+  `NonStructuralRecursion`; codegen still the iter-1 `lower_term`
+  `CodegenError::Internal` stub (real lowering = iter 3).
+- The four Display bodies are bracket-`[code]`-free (F2);
+  `carve_out_inventory` is 17 and its header prose is truthful
+  (the pre-existing "Twelve"-vs-13 drift corrected in passing).
+- `cargo test --workspace` green.
+
+## Cross-references
+
+- Parent spec `docs/specs/2026-05-17-loop-recur.md`
+  (Component 4 = this iter; Component 5 codegen + the positive
+  RUN-to-a-value / deep-`n` E2E = iter 3).
+- iter-1 (`a179ec3`) shipped the additive nodes + the `synth` /
+  `lower_term` `Internal` stubs this iter's `synth` arm replaces
+  (codegen stub stays).
+- mut.2 (`docs/specs/2026-05-15-mut-local.md`) is the structural
+  precedent: `mut_scope_stack` threading discipline, the
+  variant/`code()`/`ctx()`/bracket-free-Display pattern, the
+  `.ail.json` negative-fixture + `carve_out_inventory` +
+  `*_typecheck_pin.rs` + ct1-F2 convention. loop-recur.2 mirrors
+  the *mechanics*; the *frame element type* differs by Boss
+  call 2 (positional `Vec<Type>`, not name-keyed).
+- Boss calls 1-3 (RecurTypeMismatch mechanism; loop_stack element
+  type; diagnostic-code precedence by pass ordering) are recorded
+  here and must be mirrored into the per-iter journal at iter
+  close.