diff --git a/docs/plans/loop-recur.1.md b/docs/plans/loop-recur.1.md
new file mode 100644
index 0000000..395f1f3
--- /dev/null
+++ b/docs/plans/loop-recur.1.md
@@ -0,0 +1,1701 @@
+# loop-recur.1 — Additive AST-Node Foundation — 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:** `loop` / `recur` become real, parseable, printable,
+round-trippable, hash-stable, strictly-additive AST nodes; the whole
+workspace compiles and `cargo test --workspace` is green — with NO
+typecheck semantics and NO real codegen lowering yet.
+
+**Architecture:** Three additive items in `ailang-core::ast` —
+`Term::Loop { binders: Vec<LoopBinder>, body: Box<Term> }`,
+`Term::Recur { args: Vec<Term> }`, `struct LoopBinder { name, ty,
+init }` (the triple mirrors `MutVar` exactly). Every exhaustive
+`match`-on-`Term` in the workspace has NO `_` wildcard, so the two
+new variants force an arm at ~30 sites across all six crates plus the
+drift tests. Sites split into four classes: (a) structural
+pass-through arms (mirror the existing `Term::Mut`/`Term::Assign`
+arm shape, substituting `binders`/`init`/`body` and `args`); (b)
+head-name helpers (`"loop"` / `"recur"` string); (c) the two
+*semantic* dispatch points — typecheck `synth` and codegen
+`lower_term` — which get `CheckError::Internal` / `CodegenError::Internal`
+**stubs** in this iter exactly as mut.1 did (real semantics land in
+iter 2 / iter 3); (d) schema-drift / hash anchors.
+
+**Tech Stack:** `ailang-core` (ast, desugar, workspace, specs/form_a.md,
+drift+hash tests), `ailang-surface` (parse, print), `ailang-check`
+(lib, lift, mono, linearity, uniqueness, reuse_shape,
+pre_desugar_validation), `ailang-codegen` (lib, lambda, escape),
+`ailang-prose` (lib), `ail` (main), `docs/DESIGN.md`.
+
+---
+
+## Boss design calls baked into this plan (do not re-litigate at execution time)
+
+1. **`verify_tail_positions` "byte-unchanged" reading (spec Open
+   Q1).** The spec's "`verify_tail_positions` … byte-unchanged"
+   means its **tail-app verification role/behaviour** is unchanged,
+   NOT that the function's source text is frozen — the function is
+   an exhaustive `match`-on-`Term` with no `_` wildcard
+   (`crates/ailang-check/src/lib.rs:2672` is the existing
+   `Term::Mut` arm inside it), so the additive variant *requires*
+   two new arms there or `ailang-check` does not compile. The arms
+   added here (Task 5, Step 6) only define how the tail-app walker
+   *descends through two brand-new node kinds that no pre-existing
+   fixture contains*; they introduce zero behaviour change for any
+   pre-existing construct. The spec's own §"Testing strategy"
+   already operationalises "byte-unchanged" as
+   "`tail-app` non-regression — existing tail-app IR-snapshot and
+   e2e fixtures byte-identical" — that test (Task 7, Step 7) is the
+   acceptance evidence, not a frozen-source diff. mut.1 set the
+   exact precedent (it added `Term::Mut`/`Term::Assign` arms inside
+   the same function). This is settled; the executor does not
+   reopen it.
+
+2. **Codegen is in iter-1 scope as stubs/pass-throughs (recon
+   under-scoped it).** The brainstorm carrier said "no codegen in
+   iter 1", meaning *no real loop-header/phi/back-edge lowering*
+   (correct — that is iter 3). But `ailang-codegen` also carries
+   no-wildcard exhaustive `Term` matches (`lambda.rs:478`,
+   `escape.rs:197/389/506`, `lib.rs:1762`, `lib.rs:3094`); the
+   workspace will not compile — so `cargo test --workspace` (the
+   iter-1 goal) cannot be green — without arms there. mut.1
+   resolved exactly this by adding **`CodegenError::Internal`
+   stub** at the `lower_term` dispatch and **real structural
+   pass-through** at the pure analysis walkers + `synth_with_extras`.
+   Task 6 mirrors mut.1 site-for-site. No real loop lowering is
+   written in this iter.
+
+3. **`binders` has no `skip_serializing_if`.** Mirrors `Term::Mut.vars`
+   exactly (the field is part of the shape; empty stays `[]` in
+   canonical JSON). `recur`'s `args` likewise plain `Vec<Term>`.
+   Whether ≥1 binder is *required* is a typecheck question deferred
+   to iter 2; the parser here accepts zero-or-more binders (mirrors
+   `parse_mut`).
+
+---
+
+## Files this plan creates or modifies
+
+- Modify: `crates/ailang-core/src/ast.rs:543` — add `Term::Loop` /
+  `Term::Recur` variants; `:584` — add `struct LoopBinder`; `:952`
+  — two serde round-trip unit tests.
+- Modify: `crates/ailang-surface/src/parse.rs:1198` head dispatch +
+  unknown-head message; new `parse_loop` / `parse_recur` after
+  `parse_assign` (`:1643`); `:2551` parse unit tests.
+- Modify: `crates/ailang-surface/src/print.rs:596` — `Term::Loop` /
+  `Term::Recur` print arms.
+- Modify: `crates/ailang-core/specs/form_a.md:288` — grammar lines;
+  `:326` — notes paragraph.
+- Modify: `crates/ailang-prose/src/lib.rs:937` (write_term_prec),
+  `:1135` (count_free_var), `:1287` (subst_var_with_term).
+- Modify: `crates/ailang-core/src/desugar.rs` — 9 arm sites; 
+  `crates/ailang-core/src/workspace.rs` — 2 arm sites.
+- Modify: `crates/ailang-check/src/lib.rs` — substitute_rigids_in_term
+  (`:263`), verify_tail_positions (`:2681`), head-name helper
+  (`:3594`), synth STUB (`:3645`); `lift.rs` ×2; `mono.rs` ×2;
+  `linearity.rs` ×3; `uniqueness.rs` ×1; `reuse_shape.rs` ×1;
+  `pre_desugar_validation.rs` ×1.
+- Modify: `crates/ailang-codegen/src/lambda.rs` ×1; `escape.rs` ×3;
+  `lib.rs` — lower_term STUB (`:1762`-region) + synth_with_extras
+  (`:3095`).
+- Modify: `crates/ail/src/main.rs` — `:1534` (walk_term) + `:2754`
+  (rewrite_term) arm sites.
+- Modify: `docs/DESIGN.md:2422` — `"t":"loop"` / `"t":"recur"`
+  schema blocks.
+- Modify: `crates/ailang-core/tests/design_schema_drift.rs:153` +
+  `:174`; `spec_drift.rs:130` + `:153`; `schema_coverage.rs:51`,
+  `:98`, `:246`; `hash_pin.rs` — new pin test.
+- Create: `examples/loop_sum_to.ail` — the spec's worked `sum_to`
+  program (round-trip auto-covered by `round_trip.rs`).
+- No edit: `crates/ailang-surface/tests/round_trip.rs` (auto-discovers
+  `examples/*.ail`); `crates/ailang-core/tests/carve_out_inventory.rs`
+  (iter-1 adds no `.ail.json` negative fixtures — those are iter 2).
+
+---
+
+## Task 1: Core AST nodes + serde + round-trip unit tests
+
+**Files:**
+- Modify: `crates/ailang-core/src/ast.rs`
+
+- [ ] **Step 1: Write the two failing round-trip unit tests**
+
+In `crates/ailang-core/src/ast.rs`, inside `#[cfg(test)] mod tests`
+(after `term_assign_round_trips_through_json`, before the closing
+`}` at line 952), add:
+
+```rust
+    /// loop-recur iter 1: pin the canonical-bytes shape of a
+    /// `Term::Loop` with one binder. Mirrors the mut-empty-vars pin:
+    /// `binders` stays present (no `skip_serializing_if`).
+    #[test]
+    fn term_loop_one_binder_serialises_with_explicit_binders_field() {
+        let t = Term::Loop {
+            binders: vec![LoopBinder {
+                name: "i".into(),
+                ty: Type::int(),
+                init: Term::Lit {
+                    lit: Literal::Int { value: 0 },
+                },
+            }],
+            body: Box::new(Term::Var { name: "i".into() }),
+        };
+        let bytes = serde_json::to_string(&t).expect("serialise");
+        assert_eq!(
+            bytes,
+            r#"{"t":"loop","binders":[{"name":"i","type":{"t":"con","name":"Int","args":[]},"init":{"t":"lit","lit":{"kind":"int","value":0}}}],"body":{"t":"var","name":"i"}}"#,
+        );
+        let back: Term = serde_json::from_str(&bytes).expect("deserialise");
+        match back {
+            Term::Loop { binders, body } => {
+                assert_eq!(binders.len(), 1);
+                assert_eq!(binders[0].name, "i");
+                match *body {
+                    Term::Var { name } => assert_eq!(name, "i"),
+                    other => panic!("body mismatch: {other:?}"),
+                }
+            }
+            other => panic!("variant mismatch: {other:?}"),
+        }
+    }
+
+    /// loop-recur iter 1: round-trip a `Term::Recur` through JSON.
+    /// Pins `{ "t": "recur", "args": [...] }`.
+    #[test]
+    fn term_recur_round_trips_through_json() {
+        let t = Term::Recur {
+            args: vec![Term::Lit {
+                lit: Literal::Int { value: 1 },
+            }],
+        };
+        let bytes = serde_json::to_string(&t).expect("serialise");
+        assert_eq!(
+            bytes,
+            r#"{"t":"recur","args":[{"t":"lit","lit":{"kind":"int","value":1}}]}"#,
+        );
+        let back: Term = serde_json::from_str(&bytes).expect("deserialise");
+        match back {
+            Term::Recur { args } => assert_eq!(args.len(), 1),
+            other => panic!("variant mismatch: {other:?}"),
+        }
+    }
+```
+
+- [ ] **Step 2: Run tests to verify they fail to compile**
+
+Run: `cargo test -p ailang-core --lib term_loop_one_binder term_recur_round_trips 2>&1 | tail -5`
+Expected: FAIL — `error[E0599]: no variant ... Loop` / `Recur` /
+`cannot find struct ... LoopBinder` (the variants do not exist yet).
+
+- [ ] **Step 3: Add `Term::Loop` and `Term::Recur` variants**
+
+In `crates/ailang-core/src/ast.rs`, immediately after the
+`Term::Assign { name: String, value: Box<Term> }` variant (ends
+line 542), before the enum's closing `}` (line 543), add:
+
+```rust
+    /// loop-recur iter 1: a strict iteration block. `binders`
+    /// declares one or more loop parameters (name, type, init),
+    /// evaluated in order on loop entry; `body` is evaluated with
+    /// all binders in scope. The loop's value is `body`'s value on
+    /// the iteration that exits via a non-`recur` branch. Strictly
+    /// additive: pre-existing fixtures hash bit-identically because
+    /// none carry the `"t":"loop"` tag. `binders` has no
+    /// `skip_serializing_if` (mirrors `Term::Mut.vars` — the field
+    /// is part of the shape). Typecheck binder/recur semantics land
+    /// in loop-recur iter 2 (`synth` stubs with `CheckError::Internal`
+    /// in this iter); codegen (loop-header + per-binder phi +
+    /// back-edge) in iter 3 (`lower_term` stubs with
+    /// `CodegenError::Internal`). No totality claim — an infinite
+    /// loop is legal. See `docs/specs/2026-05-17-loop-recur.md`.
+    Loop {
+        binders: Vec<LoopBinder>,
+        body: Box<Term>,
+    },
+    /// loop-recur iter 1: re-enter the lexically innermost enclosing
+    /// `Term::Loop`, rebinding its binders positionally to `args`.
+    /// Transfers control (no fall-through); valid only in tail
+    /// position of its enclosing loop — enforced at typecheck in
+    /// iter 2 (`RecurNotInTailPosition`). Additive `"t":"recur"`
+    /// tag; pre-existing fixtures hash bit-identically.
+    Recur {
+        args: Vec<Term>,
+    },
+```
+
+- [ ] **Step 4: Add `struct LoopBinder`**
+
+In `crates/ailang-core/src/ast.rs`, immediately after the
+`struct MutVar { ... }` definition (ends line 584), add:
+
+```rust
+/// loop-recur iter 1: one binder of a [`Term::Loop`]. Mirrors
+/// [`MutVar`]'s `(name, type, init)` triple exactly so the Form-A
+/// surface vocabulary is shared (`(NAME TYPE INIT)`); it is a
+/// nested field of `Term::Loop`, not a first-class `Term` (loop
+/// binders cannot escape the enclosing loop). `recur` rebinds these
+/// positionally per iteration. The `ty` JSON field is `"type"`,
+/// matching `MutVar` and the spec schema.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct LoopBinder {
+    /// The binder's lexical name. Within the enclosing `Term::Loop`,
+    /// a `Term::Var { name }` resolves to this binding.
+    pub name: String,
+    /// The binder's declared type.
+    #[serde(rename = "type")]
+    pub ty: Type,
+    /// Initial value, evaluated once on loop entry in scope of the
+    /// outer environment plus already-declared binders of the same
+    /// `Term::Loop` (declaration order).
+    pub init: Term,
+}
+```
+
+- [ ] **Step 5: Run tests to verify they pass**
+
+Run: `cargo test -p ailang-core --lib term_loop_one_binder term_recur_round_trips 2>&1 | tail -5`
+Expected: PASS — `test result: ok. 2 passed`.
+
+(`ailang-core` itself now compiles; downstream crates still fail
+exhaustiveness — fixed in Tasks 2-7. Do not run `--workspace` yet.)
+
+---
+
+## Task 2: Surface parser + printer + grammar + parse unit tests
+
+**Files:**
+- Modify: `crates/ailang-surface/src/parse.rs`
+- Modify: `crates/ailang-surface/src/print.rs`
+- Modify: `crates/ailang-core/specs/form_a.md`
+
+- [ ] **Step 1: Write the failing parser unit test**
+
+In `crates/ailang-surface/src/parse.rs`, in the unit-tests module
+near the existing mut-family parse tests (after line 2551), add:
+
+```rust
+    #[test]
+    fn parse_loop_and_recur_round_trip_via_term() {
+        let src = "(loop (acc Int 0) (i Int 1) (if (app > i n) acc (recur (app + acc i) (app + i 1))))";
+        let mut p = Parser::new(lex(src).expect("lex"));
+        let t = p.parse_term().expect("parse loop");
+        match t {
+            ailang_core::ast::Term::Loop { binders, body } => {
+                assert_eq!(binders.len(), 2);
+                assert_eq!(binders[0].name, "acc");
+                assert_eq!(binders[1].name, "i");
+                // body is an `if` whose else-branch is a `recur` of 2 args
+                match *body {
+                    ailang_core::ast::Term::If { else_, .. } => match *else_ {
+                        ailang_core::ast::Term::Recur { args } => {
+                            assert_eq!(args.len(), 2)
+                        }
+                        other => panic!("else not recur: {other:?}"),
+                    },
+                    other => panic!("body not if: {other:?}"),
+                }
+            }
+            other => panic!("not a loop: {other:?}"),
+        }
+    }
+```
+
+(If `Parser::new` / `lex` are not the exact local test helpers,
+mirror the helper used by the adjacent `parse_mut` test verbatim —
+do not invent a new harness.)
+
+- [ ] **Step 2: Run test to verify it fails**
+
+Run: `cargo test -p ailang-surface --lib parse_loop_and_recur 2>&1 | tail -5`
+Expected: FAIL — unknown term head `loop` (parser has no arm yet).
+
+- [ ] **Step 3: Add head-dispatch arms + extend unknown-head message**
+
+In `crates/ailang-surface/src/parse.rs`, in the `match head { ... }`
+at line 1198: add two arms immediately after the
+`"assign" => self.parse_assign(),` line (1214):
+
+```rust
+                    "loop" => self.parse_loop(),
+                    "recur" => self.parse_recur(),
+```
+
+In the same `match`'s `other =>` error message (the `format!`
+string spanning lines 1219-1224), change the trailing
+`` `assign`, `lit-unit` `` to:
+
+```rust
+                                `assign`, `loop`, `recur`, `lit-unit`"
+```
+
+(The whole message string must read `… `mut`, `assign`, `loop`,
+`recur`, `lit-unit`"` contiguously on its closing line — the
+`spec_drift.rs` / unknown-head expectations key on substrings.)
+
+- [ ] **Step 4: Add `parse_loop` and `parse_recur`**
+
+In `crates/ailang-surface/src/parse.rs`, immediately after
+`fn parse_assign` (ends line 1643), add:
+
+```rust
+    /// loop-recur iter 1: `(loop (NAME TYPE INIT)* BODY_TERM+)` —
+    /// strict iteration block. Reads zero or more `(NAME TYPE INIT)`
+    /// binder triples (bare, no leading keyword — same triple as
+    /// `(var ...)`'s tail), then ≥ 1 trailing terms right-folded
+    /// into `Term::Seq` (mirrors `parse_mut`).
+    fn parse_loop(&mut self) -> Result<Term, ParseError> {
+        let head_pos = self.peek().map(|t| t.span.start).unwrap_or(0);
+        self.expect_lparen("loop-term")?;
+        self.expect_keyword("loop")?;
+
+        let mut binders: Vec<ailang_core::ast::LoopBinder> = Vec::new();
+        while matches!(self.peek(), Some(Token { tok: Tok::LParen, .. })) {
+            self.expect_lparen("loop-binder")?;
+            let name = self.expect_ident("loop-binder-name")?;
+            let ty = self.parse_type()?;
+            let init = self.parse_term()?;
+            self.expect_rparen("loop-binder")?;
+            binders.push(ailang_core::ast::LoopBinder { name, ty, init });
+        }
+
+        let mut body_stmts: Vec<Term> = Vec::new();
+        while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
+            body_stmts.push(self.parse_term()?);
+        }
+        if body_stmts.is_empty() {
+            return Err(ParseError::Production {
+                production: "loop-term",
+                message: "(loop ...) requires at least one body expression after binders".into(),
+                pos: head_pos,
+            });
+        }
+        self.expect_rparen("loop-term")?;
+
+        let mut body = body_stmts.pop().expect("non-empty after the check above");
+        while let Some(s) = body_stmts.pop() {
+            body = Term::Seq {
+                lhs: Box::new(s),
+                rhs: Box::new(body),
+            };
+        }
+        Ok(Term::Loop {
+            binders,
+            body: Box::new(body),
+        })
+    }
+
+    /// loop-recur iter 1: `(recur ARG*)` — re-enter the enclosing
+    /// loop. Positional args. The tail-position rule is enforced at
+    /// typecheck (iter 2, `recur-not-in-tail-position`); the parser
+    /// accepts the shape unconditionally.
+    fn parse_recur(&mut self) -> Result<Term, ParseError> {
+        self.expect_lparen("recur-term")?;
+        self.expect_keyword("recur")?;
+        let mut args: Vec<Term> = Vec::new();
+        while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
+            args.push(self.parse_term()?);
+        }
+        self.expect_rparen("recur-term")?;
+        Ok(Term::Recur { args })
+    }
+```
+
+(The binder loop reads a bare `(NAME TYPE INIT)` — note: unlike
+`parse_mut`'s `(var NAME TYPE INIT)`, the spec's surface is
+`(loop (NAME TYPE INIT) … BODY)` with no `var` keyword inside the
+binder. Confirm against the spec's worked example
+`(loop (acc Int 0) (i Int 1) …)` — there is no `var`. The
+`while matches! LParen` loop terminates when the next form is a
+non-parenthesised term or the closing `)`; a parenthesised *body*
+form like `(if …)` is correctly NOT consumed as a binder because a
+binder's first inner token is an ident NAME, whereas `(if …)`'s is
+a keyword — but the loop as written would mis-consume `(if …)` as a
+binder. Guard the binder loop with: only treat a leading `(` as a
+binder when its head is NOT a known term-head keyword. Implement the
+guard as: `while self.peek_is_lparen() && !self.peek_inner_is_term_head()`
+using the existing `peek_head_ident` helper —
+`while matches!(self.peek_lparen_inner_head(), Some(h) if !is_term_head(h))`.
+If no such helper exists, the robust shape mirrored from the spec is
+to require the binder list to be syntactically distinct; the
+**executor must verify** the spec's worked example parses to exactly
+2 binders + an `if` body via the Step-1 test and adjust the binder
+terminator predicate until it does. This is the one genuine parser
+judgement in the task; the Step-1 test is the oracle.)
+
+- [ ] **Step 5: Add printer arms**
+
+In `crates/ailang-surface/src/print.rs`, in `fn write_term`'s
+`match t { ... }`, immediately after the `Term::Assign { name,
+value } => { ... }` arm (ends line 596), before the match's closing
+`}` (line 597), add:
+
+```rust
+        Term::Loop { binders, body } => {
+            // loop-recur iter 1: print as
+            //   `(loop (NAME TYPE INIT)* STMT* FINAL_EXPR)`
+            // — inverse of parse_loop's binder read + Seq right-fold,
+            // mirroring the Term::Mut printer.
+            out.push_str("(loop");
+            for b in binders {
+                out.push_str(" (");
+                out.push_str(&b.name);
+                out.push(' ');
+                write_type(out, &b.ty);
+                out.push(' ');
+                write_term(out, &b.init, level);
+                out.push(')');
+            }
+            let mut cursor: &Term = body;
+            loop {
+                match cursor {
+                    Term::Seq { lhs, rhs } => {
+                        out.push(' ');
+                        write_term(out, lhs, level);
+                        cursor = rhs;
+                    }
+                    other => {
+                        out.push(' ');
+                        write_term(out, other, level);
+                        break;
+                    }
+                }
+            }
+            out.push(')');
+        }
+        Term::Recur { args } => {
+            out.push_str("(recur");
+            for a in args {
+                out.push(' ');
+                write_term(out, a, level);
+            }
+            out.push(')');
+        }
+```
+
+- [ ] **Step 6: Add grammar lines + notes to `form_a.md`**
+
+In `crates/ailang-core/specs/form_a.md`, in the parenthesised-forms
+code block, immediately after the `(assign NAME VALUE-TERM)` line
+(288), add:
+
+```
+(loop (NAME TYPE INIT)* BODY-TERM+)     ; strict iteration block (loop-recur)
+(recur ARG*)                            ; re-enter enclosing loop (loop-recur)
+```
+
+In the `Notes:` list, immediately after the `(assign …)` note
+paragraph (ends line 326), add:
+
+```
+- `loop` opens a strict iteration block. `(NAME TYPE INIT)` binder
+  triples (zero or more) are followed by a body of zero or more
+  Unit-typed statements and exactly one final expression (right-
+  folded into `Term::Seq` like `mut`). `recur` re-enters the
+  lexically innermost enclosing `loop`, rebinding its binders
+  positionally; `(recur ARG*)`'s arg count must equal the binder
+  count and `recur` must be in tail position of the loop body —
+  both enforced at typecheck (`recur-arity-mismatch`,
+  `recur-not-in-tail-position`). `loop`/`recur` make no termination
+  claim: a `loop` with no non-`recur` exit runs forever. See
+  `docs/specs/2026-05-17-loop-recur.md`.
+```
+
+- [ ] **Step 7: Run the parser test + surface build**
+
+Run: `cargo test -p ailang-surface --lib parse_loop_and_recur 2>&1 | tail -5`
+Expected: PASS. (Other crates still fail exhaustiveness; continue.)
+
+---
+
+## Task 3: Prose projection arms
+
+**Files:**
+- Modify: `crates/ailang-prose/src/lib.rs`
+
+- [ ] **Step 1: Add `write_term_prec` arms**
+
+In `crates/ailang-prose/src/lib.rs`, in `fn write_term_prec`'s
+`match t`, immediately after the `Term::Assign { name, value } =>
+{ ... }` arm (ends line 937), before the match's closing `}`
+(line 938), add:
+
+```rust
+        Term::Loop { binders, body } => {
+            // loop-recur iter 1: minimal-correctness Form-B render.
+            // Prose surface for loop is not yet designed; render the
+            // shape so a reader sees it without overcommitting.
+            out.push_str("loop {\n");
+            for b in binders {
+                indent(out, level + 1);
+                out.push_str(&b.name);
+                out.push_str(" = ");
+                write_term(out, &b.init, level + 1, owning_module);
+                out.push_str(";\n");
+            }
+            indent(out, level + 1);
+            write_term(out, body, level + 1, owning_module);
+            out.push('\n');
+            indent(out, level);
+            out.push('}');
+        }
+        Term::Recur { args } => {
+            out.push_str("recur(");
+            for (i, a) in args.iter().enumerate() {
+                if i > 0 {
+                    out.push_str(", ");
+                }
+                write_term(out, a, level, owning_module);
+            }
+            out.push(')');
+        }
+```
+
+- [ ] **Step 2: Add `count_free_var` arms**
+
+In `crates/ailang-prose/src/lib.rs`, in `fn count_free_var`'s
+`match`, immediately after the `Term::Assign { name: assign_name,
+value } => { ... }` arm (ends line 1135), before the match closing
+`}` (line 1136), add:
+
+```rust
+        // loop-recur iter 1: a binder named `name` shadows the outer
+        // binding for later binder inits and the body. Inits before
+        // the shadowing binder still see the outer `name`.
+        Term::Loop { binders, body } => {
+            let mut total = 0usize;
+            let mut shadowed = false;
+            for b in binders {
+                if !shadowed {
+                    total += count_free_var(name, &b.init);
+                }
+                if b.name == name {
+                    shadowed = true;
+                }
+            }
+            if !shadowed {
+                total += count_free_var(name, body);
+            }
+            total
+        }
+        Term::Recur { args } => {
+            args.iter().map(|a| count_free_var(name, a)).sum()
+        }
+```
+
+- [ ] **Step 3: Add `subst_var_with_term` arms**
+
+In `crates/ailang-prose/src/lib.rs`, in `fn subst_var_with_term`'s
+`match t`, immediately after the `Term::Assign { name: assign_name,
+value } => Term::Assign { ... }` arm (ends line 1287), before the
+match closing `}` (line 1288), add:
+
+```rust
+        // loop-recur iter 1: lexical-shadow semantics symmetric to
+        // count_free_var — once a binder named `name` is declared,
+        // later inits and the body are not rewritten.
+        Term::Loop { binders, body } => {
+            let mut shadowed = false;
+            let new_binders: Vec<ailang_core::ast::LoopBinder> = binders
+                .iter()
+                .map(|b| {
+                    let init = if shadowed {
+                        b.init.clone()
+                    } else {
+                        subst_var_with_term(&b.init, name, replacement)
+                    };
+                    if b.name == name {
+                        shadowed = true;
+                    }
+                    ailang_core::ast::LoopBinder {
+                        name: b.name.clone(),
+                        ty: b.ty.clone(),
+                        init,
+                    }
+                })
+                .collect();
+            let body_rw = if shadowed {
+                (**body).clone()
+            } else {
+                subst_var_with_term(body, name, replacement)
+            };
+            Term::Loop {
+                binders: new_binders,
+                body: Box::new(body_rw),
+            }
+        }
+        Term::Recur { args } => Term::Recur {
+            args: args
+                .iter()
+                .map(|a| subst_var_with_term(a, name, replacement))
+                .collect(),
+        },
+```
+
+- [ ] **Step 4: Build prose crate**
+
+Run: `cargo build -p ailang-prose 2>&1 | tail -3`
+Expected: prose-crate-local exhaustiveness satisfied (it may still
+fail building due to its dep on `ailang-check`; that is expected
+until Task 5 — the acceptance gate for this task is that
+`prose/src/lib.rs` has no `non-exhaustive patterns` error; grep the
+output for `prose/src/lib.rs` — there must be none).
+
+---
+
+## Task 4: ailang-core walker arms (desugar + workspace)
+
+**Files:**
+- Modify: `crates/ailang-core/src/desugar.rs`
+- Modify: `crates/ailang-core/src/workspace.rs`
+
+Each step below adds two arms immediately after the existing
+`Term::Assign` arm at the cited line. The arm shape mirrors the
+adjacent `Term::Mut` arm at that site (substitute
+`binders`/`b.init`/`body` for `vars`/`v.init`/`body`, and `args`
+for the Recur form). The literal arm is given per site.
+
+- [ ] **Step 1: `desugar.rs` `collect_used_in_term` (after `:360`)**
+
+`collect_used_in_term` is a free fn (`fn collect_used_in_term(t:
+&Term, used: &mut BTreeSet<String>)` at `:283`), not a method.
+After the `Term::Assign { name, value } => { ... }` arm following
+`Term::Mut` at `:349` (the Assign arm starts `:360`), add:
+
+```rust
+        Term::Loop { binders, body } => {
+            for b in binders {
+                used.insert(b.name.clone());
+                collect_used_in_term(&b.init, used);
+            }
+            collect_used_in_term(body, used);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                collect_used_in_term(a, used);
+            }
+        }
+```
+
+- [ ] **Step 2: `desugar.rs` `desugar_term` (after `:588`)**
+
+The `Term::Mut` arm at `:559-588` extends scope per-var via
+`inner.insert(v.name.clone(), ScopeEntry::LetBound)` (a
+`BTreeMap`-style `scope` clone, `scope` is the second param of
+`desugar_term`). After the `Term::Assign { name, value } =>
+Term::Assign { ... }` arm following it (Assign starts `:589`), add:
+
+```rust
+            Term::Loop { binders, body } => {
+                // loop-recur iter 1: structural recursion mirroring
+                // the Term::Mut arm. Each binder's init is desugared
+                // in scope of the outer env plus already-declared
+                // binders; the body sees all binders. The LetBound
+                // sentinel keeps generated fresh names off binder
+                // names.
+                let mut inner = scope.clone();
+                let new_binders: Vec<ailang_core::ast::LoopBinder> = binders
+                    .iter()
+                    .map(|b| {
+                        let init = self.desugar_term(&b.init, &inner);
+                        inner.insert(b.name.clone(), ScopeEntry::LetBound);
+                        ailang_core::ast::LoopBinder {
+                            name: b.name.clone(),
+                            ty: b.ty.clone(),
+                            init,
+                        }
+                    })
+                    .collect();
+                Term::Loop {
+                    binders: new_binders,
+                    body: Box::new(self.desugar_term(body, &inner)),
+                }
+            }
+            Term::Recur { args } => Term::Recur {
+                args: args
+                    .iter()
+                    .map(|a| self.desugar_term(a, scope))
+                    .collect(),
+            },
+```
+
+- [ ] **Step 3: `desugar.rs` `free_vars_in_term` (after `:1228`)**
+
+`free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut
+BTreeSet<String>)` (`:1138`). The `Term::Mut` arm at `:1214-1227`
+clones `bound` into a local `b`, walks each init under the growing
+`b`, inserts each var name into `b`, then walks the body under `b`.
+After the `Term::Assign` arm following it (Assign starts `:1228`),
+add:
+
+```rust
+        Term::Loop { binders, body } => {
+            // loop-recur iter 1: binder names bind inside the loop —
+            // each init sees the outer env plus already-declared
+            // binders; the body sees all. Mirrors the Term::Mut arm.
+            let mut b = bound.clone();
+            for bd in binders {
+                free_vars_in_term(&bd.init, &b, out);
+                b.insert(bd.name.clone());
+            }
+            free_vars_in_term(body, &b, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                free_vars_in_term(a, bound, out);
+            }
+        }
+```
+
+- [ ] **Step 4: `desugar.rs` `subst_var` (after `:1416`)**
+
+`pub fn subst_var(t: &Term, from: &str, to: &str) -> Term`
+(`:1272`). The `Term::Mut` arm at `:1381-1414` is shadow-aware
+(stop substituting once a var named `from` is declared). After the
+`Term::Assign { name, value } => Term::Assign { ... }` arm
+following it (Assign starts `:1416`), add:
+
+```rust
+        Term::Loop { binders, body } => {
+            // loop-recur iter 1: binders lexically shadow outer
+            // names, symmetric to the Term::Mut arm — once a binder
+            // named `from` is declared, later inits and the body
+            // stop being substituted.
+            let mut shadowed = false;
+            let new_binders: Vec<ailang_core::ast::LoopBinder> = binders
+                .iter()
+                .map(|b| {
+                    let init = if shadowed {
+                        b.init.clone()
+                    } else {
+                        subst_var(&b.init, from, to)
+                    };
+                    if b.name == from {
+                        shadowed = true;
+                    }
+                    ailang_core::ast::LoopBinder {
+                        name: b.name.clone(),
+                        ty: b.ty.clone(),
+                        init,
+                    }
+                })
+                .collect();
+            let body_rw = if shadowed {
+                (**body).clone()
+            } else {
+                subst_var(body, from, to)
+            };
+            Term::Loop {
+                binders: new_binders,
+                body: Box::new(body_rw),
+            }
+        }
+        Term::Recur { args } => Term::Recur {
+            args: args.iter().map(|a| subst_var(a, from, to)).collect(),
+        },
+```
+
+- [ ] **Step 5: `desugar.rs` `subst_call_with_extras` (after `:1567`)**
+
+After the `Term::Assign` arm following the `Term::Mut` rebuild at
+`:1551`, add:
+
+```rust
+        Term::Loop { binders, body } => Term::Loop {
+            binders: binders
+                .iter()
+                .map(|b| ailang_core::ast::LoopBinder {
+                    name: b.name.clone(),
+                    ty: b.ty.clone(),
+                    init: subst_call_with_extras(&b.init, target, extras),
+                })
+                .collect(),
+            body: Box::new(subst_call_with_extras(body, target, extras)),
+        },
+        Term::Recur { args } => Term::Recur {
+            args: args
+                .iter()
+                .map(|a| subst_call_with_extras(a, target, extras))
+                .collect(),
+        },
+```
+
+(Match `subst_call_with_extras`'s real param names from its
+signature — mirror the local `Term::Mut` arm at `:1551`.)
+
+- [ ] **Step 6: `desugar.rs` `find_non_callee_use` (after `:1636`)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:1629`, add:
+
+```rust
+        Term::Loop { binders, body } => binders
+            .iter()
+            .find_map(|b| find_non_callee_use(&b.init, name))
+            .or_else(|| find_non_callee_use(body, name)),
+        Term::Recur { args } => {
+            args.iter().find_map(|a| find_non_callee_use(a, name))
+        }
+```
+
+- [ ] **Step 7: `desugar.rs` `any_nested_ctor` (after `:1689`)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:1686`, add:
+
+```rust
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| any_nested_ctor(&b.init)) || any_nested_ctor(body)
+            }
+            Term::Recur { args } => args.iter().any(any_nested_ctor),
+```
+
+- [ ] **Step 8: `desugar.rs` `any_let_rec` (after `:1719`)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:1716`, add:
+
+```rust
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| any_let_rec(&b.init)) || any_let_rec(body)
+            }
+            Term::Recur { args } => args.iter().any(any_let_rec),
+```
+
+- [ ] **Step 9: `desugar.rs` `any_lit_pattern` (after `:2840`)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:2837`, add:
+
+```rust
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| any_lit_pattern(&b.init)) || any_lit_pattern(body)
+            }
+            Term::Recur { args } => args.iter().any(any_lit_pattern),
+```
+
+- [ ] **Step 10: `workspace.rs` `walk_term_embedded_types` (after `:1260`)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:1254`, add:
+
+```rust
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_type(&b.ty, f)?;
+                walk_term_embedded_types(&b.init, f)?;
+            }
+            walk_term_embedded_types(body, f)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term_embedded_types(a, f)?;
+            }
+            Ok(())
+        }
+```
+
+- [ ] **Step 11: `workspace.rs` `walk_term` (after `:1394`)**
+
+After the `Term::Assign { value, .. } => walk_term(value, f)` arm
+following `Term::Mut` at `:1388`, add:
+
+```rust
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_term(&b.init, f)?;
+            }
+            walk_term(body, f)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a, f)?;
+            }
+            Ok(())
+        }
+```
+
+- [ ] **Step 12: Build ailang-core**
+
+Run: `cargo build -p ailang-core 2>&1 | tail -3`
+Expected: PASS — `ailang-core` compiles (all its exhaustive
+`Term` matches now have arms).
+
+---
+
+## Task 5: ailang-check walker arms + verify_tail_positions pass-through + synth STUB
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs`
+- Modify: `crates/ailang-check/src/lift.rs`
+- Modify: `crates/ailang-check/src/mono.rs`
+- Modify: `crates/ailang-check/src/linearity.rs`
+- Modify: `crates/ailang-check/src/uniqueness.rs`
+- Modify: `crates/ailang-check/src/reuse_shape.rs`
+- Modify: `crates/ailang-check/src/pre_desugar_validation.rs`
+
+- [ ] **Step 1: `lib.rs` `substitute_rigids_in_term` (after `:263`)**
+
+After the `Term::Assign { name, value } => Term::Assign { ... }`
+arm following `Term::Mut` at `:249`, add:
+
+```rust
+        Term::Loop { binders, body } => Term::Loop {
+            binders: binders
+                .iter()
+                .map(|b| ailang_core::ast::LoopBinder {
+                    name: b.name.clone(),
+                    ty: substitute_rigids(&b.ty, mapping),
+                    init: substitute_rigids_in_term(&b.init, mapping),
+                })
+                .collect(),
+            body: Box::new(substitute_rigids_in_term(body, mapping)),
+        },
+        Term::Recur { args } => Term::Recur {
+            args: args
+                .iter()
+                .map(|a| substitute_rigids_in_term(a, mapping))
+                .collect(),
+        },
+```
+
+- [ ] **Step 2: `lift.rs` `lift_in_term` (after the `Term::Mut` rebuild at `:383`)**
+
+The `Term::Mut` arm at `:383-395` is a method that threads
+`self.lift_in_term(&v.init, locals, in_def)?`. After the
+`Term::Assign { name, value } => Ok(Term::Assign { ... })` arm
+following it (Assign at `:396-399`), add:
+
+```rust
+            Term::Loop { binders, body } => Ok(Term::Loop {
+                binders: binders
+                    .iter()
+                    .map(|b| {
+                        Ok(ailang_core::ast::LoopBinder {
+                            name: b.name.clone(),
+                            ty: b.ty.clone(),
+                            init: self.lift_in_term(&b.init, locals, in_def)?,
+                        })
+                    })
+                    .collect::<Result<Vec<_>>>()?,
+                body: Box::new(self.lift_in_term(body, locals, in_def)?),
+            }),
+            Term::Recur { args } => Ok(Term::Recur {
+                args: args
+                    .iter()
+                    .map(|a| self.lift_in_term(a, locals, in_def))
+                    .collect::<Result<Vec<_>>>()?,
+            }),
+```
+
+- [ ] **Step 3: `lift.rs` `term_has_letrec` (after `:763`)**
+
+After `Term::Assign { value, .. } => term_has_letrec(value)`
+(`:763`) following `Term::Mut` at `:760`, add:
+
+```rust
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| term_has_letrec(&b.init)) || term_has_letrec(body)
+            }
+            Term::Recur { args } => args.iter().any(term_has_letrec),
+```
+
+- [ ] **Step 4: `mono.rs` `rewrite_mono_calls` (after `:1243`)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:1237`
+(in-place `&mut` walk), add (mirror the Mut arm's full call list
+verbatim from `:1237-1242`):
+
+```rust
+        Term::Loop { binders, body } => {
+            for b in binders.iter_mut() {
+                rewrite_mono_calls(&mut b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+            }
+            rewrite_mono_calls(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+        }
+        Term::Recur { args } => {
+            for a in args.iter_mut() {
+                rewrite_mono_calls(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+            }
+        }
+```
+
+- [ ] **Step 5: `mono.rs` `interleave_slots` (after `:1617`)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:1611`, add
+(mirror the Mut arm's full call list from `:1611-1616`):
+
+```rust
+        Term::Loop { binders, body } => {
+            for b in binders {
+                interleave_slots(&b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+            interleave_slots(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                interleave_slots(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+        }
+```
+
+- [ ] **Step 6: `lib.rs` `verify_tail_positions` (after `:2681`) — the Boss-call-1 site**
+
+After `Term::Assign { value, .. } => verify_tail_positions(value,
+false)` (`:2681`) following `Term::Mut` at `:2672`, before the
+match closing `}` (`:2682`), add:
+
+```rust
+        // loop-recur iter 1: binder inits are evaluated once on loop
+        // entry, NOT in tail position (mirror the Term::Mut arm
+        // above). The loop body inherits the enclosing tail position
+        // (the loop's value is the body's value on the exiting
+        // iteration). This arm only defines tail-app descent through
+        // the new node; it makes NO claim about recur tail-position
+        // (that is loop-recur iter 2's `verify_loop_body`). The
+        // tail-app verification role is unchanged — no pre-existing
+        // fixture contains a `loop`/`recur` node.
+        Term::Loop { binders, body } => {
+            for b in binders {
+                verify_tail_positions(&b.init, false)?;
+            }
+            verify_tail_positions(body, is_tail)
+        }
+        // recur transfers control and does not fall through, so there
+        // is no tail position to propagate. Its args are evaluated in
+        // non-tail position (call-argument-like). Introduces no
+        // tail-app violation.
+        Term::Recur { args } => {
+            for a in args {
+                verify_tail_positions(a, false)?;
+            }
+            Ok(())
+        }
+```
+
+- [ ] **Step 7: `lib.rs` head-name helper (after `:3594`)**
+
+In the `match` whose arms map a `Term` to its tag string (the
+`Term::Mut { .. } => "mut"` / `Term::Assign { .. } => "assign"`
+arms at `:3593-3594`, ending with `Term::Ctor { .. } | Term::Lam
+{ .. } => unreachable!()`), add immediately after the
+`Term::Assign { .. } => "assign",` line (`:3594`):
+
+```rust
+                        Term::Loop { .. } => "loop",
+                        Term::Recur { .. } => "recur",
+```
+
+- [ ] **Step 8: `lib.rs` `synth` STUB (after `:3645`) — Boss-call-2 site**
+
+In `pub(crate) fn synth` (`:2719`), after the `Term::Assign { name,
+value } => { ... }` arm following the `Term::Mut` arm at `:3614`
+(the Assign arm ends around `:3680`; locate the arm immediately
+before `synth`'s match closing brace), add:
+
+```rust
+        // loop-recur iter 1: typecheck semantics (binder typing,
+        // recur arity/type unification, verify_loop_body
+        // tail-position, the four Recur* CheckError variants) land
+        // in loop-recur iter 2. This iter stubs the dispatch so the
+        // workspace compiles and round-trips; no loop/recur fixture
+        // is typechecked in iter 1. Mirrors mut.1's synth stub.
+        Term::Loop { .. } | Term::Recur { .. } => Err(CheckError::Internal(
+            "Term::Loop/Term::Recur typecheck lands in loop-recur iter 2".into(),
+        )),
+```
+
+(`CheckError::Internal(String)` is defined at `lib.rs:687`
+`#[error("internal: {0}")]`. `synth` returns `Result<Type>` over
+`CheckError` — `Err(CheckError::Internal(...))` is the correct
+stub return.)
+
+- [ ] **Step 9: `linearity.rs` `walk` (after `:607`)**
+
+After the `Term::Assign { value, .. } => { ... }` arm following
+`Term::Mut` at `:601`, add (mirror the Mut arm's `self.walk(...,
+Position::...)` calls verbatim from `:601-606`):
+
+```rust
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a, Position::Consume);
+                }
+            }
+```
+
+- [ ] **Step 10: `linearity.rs` head-name helper (after `:797`)**
+
+After `Term::Assign { .. } => "assign",` (`:797`) following
+`Term::Mut { .. } => "mut"` (`:796`), add:
+
+```rust
+        Term::Loop { .. } => "loop",
+        Term::Recur { .. } => "recur",
+```
+
+- [ ] **Step 11: `linearity.rs` `any_sub_binder_consumed_for` (after `:935`)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:929`, add
+(mirror the Mut arm's full call signature from `:929-933`):
+
+```rust
+        Term::Loop { binders, body } => {
+            binders.iter().any(|b| {
+                any_sub_binder_consumed_for(&b.init, pname, uniq, def_name, ctors)
+            }) || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors)
+        }
+        Term::Recur { args } => args.iter().any(|a| {
+            any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors)
+        }),
+```
+
+- [ ] **Step 12: `uniqueness.rs` `walk` (after `:352`)**
+
+After the `Term::Assign { value, .. } => { ... }` arm following
+`Term::Mut` at `:346`, add (mirror the Mut arm's `self.walk`
+calls + the `pos`/`Position::Consume` choice verbatim from
+`:346-351`):
+
+```rust
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a, Position::Consume);
+                }
+            }
+```
+
+- [ ] **Step 13: `reuse_shape.rs` `walk` (after `:267`)**
+
+After `Term::Assign { value, .. } => self.walk(value)` (`:267`)
+following `Term::Mut` at `:261`, add:
+
+```rust
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init);
+                }
+                self.walk(body);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a);
+                }
+            }
+```
+
+- [ ] **Step 14: `pre_desugar_validation.rs` `walk_term` (after `:135`)**
+
+After `Term::Assign { value, .. } => walk_term(value)` (`:135`)
+following `Term::Mut` at `:129`, add:
+
+```rust
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_term(&b.init)?;
+            }
+            walk_term(body)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a)?;
+            }
+            Ok(())
+        }
+```
+
+- [ ] **Step 15: Build ailang-check**
+
+Run: `cargo build -p ailang-check 2>&1 | tail -3`
+Expected: PASS — `ailang-check` compiles.
+
+---
+
+## Task 6: ailang-codegen arms (stub + pass-through) + ail/main.rs arms
+
+**Files:**
+- Modify: `crates/ailang-codegen/src/lambda.rs`
+- Modify: `crates/ailang-codegen/src/escape.rs`
+- Modify: `crates/ailang-codegen/src/lib.rs`
+- Modify: `crates/ail/src/main.rs`
+
+- [ ] **Step 1: `lambda.rs` `collect_captures` (after `:478` Mut arm)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:478`
+(newly-bound roll-back pattern), add (mirror the Mut arm's
+`Self::collect_captures(...)` signature + `bound.insert` /
+`newly_bound` roll-back verbatim from `:478-`):
+
+```rust
+            Term::Loop { binders, body } => {
+                let mut newly_bound: Vec<String> = Vec::new();
+                for b in binders {
+                    Self::collect_captures(&b.init, bound, captures, captures_set, builtins, top_level);
+                    if bound.insert(b.name.clone()) {
+                        newly_bound.push(b.name.clone());
+                    }
+                }
+                Self::collect_captures(body, bound, captures, captures_set, builtins, top_level);
+                for n in newly_bound {
+                    bound.remove(&n);
+                }
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
+                }
+            }
+```
+
+- [ ] **Step 2: `escape.rs` `walk` (after `:203` Mut arm)**
+
+After `Term::Assign { value, .. } => walk(value, out)` (`:203`)
+following `Term::Mut` at `:197`, add:
+
+```rust
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk(&b.init, out);
+            }
+            walk(body, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk(a, out);
+            }
+        }
+```
+
+- [ ] **Step 3: `escape.rs` `escapes` (after `:395` Mut arm)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:389`, add:
+
+```rust
+        Term::Loop { binders, body } => {
+            for b in binders {
+                if escapes(&b.init, tainted, false) {
+                    return true;
+                }
+            }
+            escapes(body, tainted, in_tail)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                if escapes(a, tainted, false) {
+                    return true;
+                }
+            }
+            false
+        }
+```
+
+- [ ] **Step 4: `escape.rs` `collect_free_vars` (after `:506` Mut arm)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:506`
+(add-then-walk-then-remove `newly` pattern), add (mirror the Mut
+arm's `bound.insert`/`newly`/restore verbatim):
+
+```rust
+        Term::Loop { binders, body } => {
+            let mut newly: Vec<String> = Vec::new();
+            for b in binders {
+                collect_free_vars(&b.init, bound, out);
+                if bound.insert(b.name.clone()) {
+                    newly.push(b.name.clone());
+                }
+            }
+            collect_free_vars(body, bound, out);
+            for n in newly {
+                bound.remove(&n);
+            }
+        }
+        Term::Recur { args } => {
+            for a in args {
+                collect_free_vars(a, bound, out);
+            }
+        }
+```
+
+- [ ] **Step 5: `lib.rs` `lower_term` STUB (after the `Term::Mut` arm at `:1762`)**
+
+The `Term::Mut { vars, body } =>` arm at `:1762` has real mut.3
+lowering and ends with the saved-binding restore loop (around
+`:1804`+) followed by a `Term::Assign` arm. After that
+`Term::Assign` arm, before the `lower_term` match's closing brace,
+add the iter-1 STUB (real loop-header/phi/back-edge lowering is
+loop-recur iter 3):
+
+```rust
+            // loop-recur iter 1: real codegen (loop-header block,
+            // per-binder phi, back-edge br) lands in iter 3. This
+            // iter stubs the dispatch so the workspace compiles; no
+            // loop/recur program is codegen'd in iter 1. Mirrors
+            // mut.1's lower_term stub.
+            Term::Loop { .. } | Term::Recur { .. } => Err(CodegenError::Internal(
+                "Term::Loop/Term::Recur lowering lands in loop-recur iter 3".into(),
+            )),
+```
+
+(`CodegenError::Internal(String)` is the same constructor used at
+`lib.rs:1779` and `:3069`.)
+
+- [ ] **Step 6: `lib.rs` `synth_with_extras` (after `:3095`)**
+
+After `Term::Assign { .. } => Ok(Type::unit())` (`:3095`) following
+`Term::Mut { body, .. } => self.synth_with_extras(body, extras)`
+(`:3094`), before the match closing `}` (`:3096`), add:
+
+```rust
+            // loop-recur iter 1: a Term::Loop's static type is the
+            // body's type (mirror Term::Mut). Term::Recur does not
+            // fall through; a Unit stub is safe — this arm is never
+            // hit on the shipping path because lower_term stubs
+            // Loop/Recur, and iter 1 codegens no loop/recur program.
+            Term::Loop { body, .. } => self.synth_with_extras(body, extras),
+            Term::Recur { .. } => Ok(Type::unit()),
+```
+
+- [ ] **Step 7: `main.rs` `walk_term` (after `:1534` Mut arm)**
+
+After the `Term::Assign` arm following `Term::Mut` at `:1520`
+(newly-bound `scope` roll-back), add (mirror the Mut arm's
+`scope.insert`/`newly`/`scope.remove` verbatim from `:1520-1534`):
+
+```rust
+        Term::Loop { binders, body } => {
+            let mut newly = Vec::new();
+            for b in binders {
+                walk_term(&b.init, out, builtins, scope);
+                if scope.insert(b.name.clone()) {
+                    newly.push(b.name.clone());
+                }
+            }
+            walk_term(body, out, builtins, scope);
+            for n in newly {
+                scope.remove(&n);
+            }
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a, out, builtins, scope);
+            }
+        }
+```
+
+- [ ] **Step 8: `main.rs` `rewrite_term` (after the `Term::Mut` arm at `:2754`)**
+
+The `Term::Mut { vars, body } =>` arm at `:2754` rewrites each
+`v.ty` via `rewrite_type` and each `v.init` + `body` via
+`rewrite_term` (in-place `&mut`). After the `Term::Assign` arm
+that follows it, add (mirror that arm's `rewrite_type` /
+`rewrite_term` argument lists verbatim):
+
+```rust
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    rewrite_type(
+                        &mut b.ty,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                    rewrite_term(
+                        &mut b.init,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                }
+                rewrite_term(
+                    body,
+                    owning_module,
+                    local_types,
+                    import_names,
+                    changed,
+                );
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    rewrite_term(
+                        a,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                }
+            }
+```
+
+- [ ] **Step 9: Build the whole workspace**
+
+Run: `cargo build --workspace 2>&1 | tail -3`
+Expected: PASS — every crate compiles (no `non-exhaustive
+patterns` errors anywhere).
+
+---
+
+## Task 7: Schema/drift anchors + DESIGN.md + hash pin + positive fixture + full suite
+
+**Files:**
+- Modify: `docs/DESIGN.md`
+- Modify: `crates/ailang-core/tests/design_schema_drift.rs`
+- Modify: `crates/ailang-core/tests/spec_drift.rs`
+- Modify: `crates/ailang-core/tests/schema_coverage.rs`
+- Modify: `crates/ailang-core/tests/hash_pin.rs`
+- Create: `examples/loop_sum_to.ail`
+
+- [ ] **Step 1: Add `"t":"loop"` / `"t":"recur"` schema blocks to DESIGN.md**
+
+In `docs/DESIGN.md`, immediately after the `{ "t": "assign",
+"name": "<id>", "value": Term }` block (the `"value": Term }` line
+is 2422), before the closing ```` ``` ```` fence (line 2423), add:
+
+```
+// loop-recur iter 1: strict iteration block. `binders` declares
+// one or more loop parameters (name, type, init), evaluated in
+// order on loop entry; `body` is in scope of all binders. The
+// loop's value is `body`'s value on the iteration that exits via a
+// non-`recur` branch. Strictly additive (no `skip_serializing_if`;
+// pre-existing fixtures hash bit-identically — none carry the tag).
+// No totality claim — an infinite loop is legal. See
+// `docs/specs/2026-05-17-loop-recur.md`.
+{ "t": "loop",
+  "binders": [ { "name": "<id>", "type": Type, "init": Term }, ... ],
+  "body": Term }
+
+// loop-recur iter 1: re-enter the lexically innermost enclosing
+// `loop`, rebinding its binders positionally to `args`. Transfers
+// control (no fall-through); valid only in tail position of its
+// enclosing loop (enforced at typecheck, `recur-not-in-tail-position`).
+{ "t": "recur",
+  "args": [ Term, ... ] }
+```
+
+(The literal substrings `"t": "loop"` and `"t": "recur"` each
+appear contiguously on one line — the `design_schema_drift.rs`
+exemplar anchors `r#""t": "loop""#` / `r#""t": "recur""#` are
+matched by `data_model_section().contains(...)`; no soft-wrap may
+split them. This is the planner self-review item-6 pin/replacement
+contiguity check, satisfied here.)
+
+- [ ] **Step 2: Extend `design_schema_drift.rs`**
+
+In `crates/ailang-core/tests/design_schema_drift.rs`, in the
+`exemplars` vec, immediately after the `assign` tuple (ends `:153`),
+add:
+
+```rust
+        (
+            r#""t": "loop""#,
+            Term::Loop {
+                binders: Vec::new(),
+                body: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
+        (
+            r#""t": "recur""#,
+            Term::Recur { args: vec![] },
+        ),
+```
+
+In the exhaustive tag `match term { ... }` (`:159-175`), after
+`Term::Assign { .. } => "assign",` (`:174`), add:
+
+```rust
+            Term::Loop { .. } => "loop",
+            Term::Recur { .. } => "recur",
+```
+
+- [ ] **Step 3: Extend `spec_drift.rs`**
+
+In `crates/ailang-core/tests/spec_drift.rs`, in the `exemplars`
+vec, immediately after the `(assign` tuple (ends `:130`), add:
+
+```rust
+        (
+            "(loop",
+            Term::Loop {
+                binders: Vec::new(),
+                body: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
+        (
+            "(recur",
+            Term::Recur { args: vec![] },
+        ),
+```
+
+In the exhaustive `match term { ... }` (`:138-154`), after
+`Term::Assign { .. } => "assign",` (`:153`), add:
+
+```rust
+            Term::Loop { .. } => "loop",
+            Term::Recur { .. } => "recur",
+```
+
+(The anchors `(loop` / `(recur` are the grammar lines added to
+`form_a.md` in Task 2 Step 6 — `FORM_A_SPEC.contains("(loop")`
+passes because `(loop (NAME TYPE INIT)* …` is present contiguously.)
+
+- [ ] **Step 4: Extend `schema_coverage.rs`**
+
+In `crates/ailang-core/tests/schema_coverage.rs`:
+(a) in `enum VariantTag`, after `TermAssign,` (`:51`), add:
+
+```rust
+    TermLoop,
+    TermRecur,
+```
+
+(b) in `const EXPECTED_VARIANTS`, after `VariantTag::TermAssign,`
+(`:98`), add:
+
+```rust
+    VariantTag::TermLoop,
+    VariantTag::TermRecur,
+```
+
+(c) in `fn visit_term`, after the `Term::Assign { value, .. } =>
+{ ... }` arm (`:243-246`), before the match closing `}` (`:247`),
+add:
+
+```rust
+        Term::Loop { binders, body } => {
+            observed.insert(VariantTag::TermLoop);
+            for b in binders {
+                visit_type(&b.ty, observed);
+                visit_term(&b.init, observed);
+            }
+            visit_term(body, observed);
+        }
+        Term::Recur { args } => {
+            observed.insert(VariantTag::TermRecur);
+            for a in args {
+                visit_term(a, observed);
+            }
+        }
+```
+
+- [ ] **Step 5: Add the hash-stability pin to `hash_pin.rs`**
+
+In `crates/ailang-core/tests/hash_pin.rs`, immediately after the
+`fn iter13a_schema_extension_preserves_pre_13a_hashes` test
+(ends ~`:88`), add:
+
+```rust
+/// loop-recur iter 1 regression: adding `Term::Loop` / `Term::Recur`
+/// (and `struct LoopBinder`) must NOT change canonical-JSON hashes
+/// of any pre-loop-recur definition. The additive variant carries a
+/// new `"t"` tag absent from every pre-existing fixture, so the
+/// recorded hashes below must stay byte-identical. If this fires,
+/// the extension is non-additive (a `skip_serializing_if` is missing
+/// or an existing variant's shape drifted).
+#[test]
+fn loop_recur_schema_extension_preserves_pre_loop_recur_hashes() {
+    let examples = examples_dir();
+
+    let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
+        .expect("examples/sum.ail loads");
+    let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
+    assert_eq!(def_hash(sum_def), "db33f57cb329935e");
+
+    let list_mod = ailang_surface::load_module(&examples.join("list.ail"))
+        .expect("examples/list.ail loads");
+    let int_list_def = list_mod.defs.iter().find(|d| d.name() == "IntList").unwrap();
+    assert_eq!(def_hash(int_list_def), "b082192bd0c99202");
+}
+```
+
+- [ ] **Step 6: Create the positive round-trip fixture**
+
+Create `examples/loop_sum_to.ail` with exactly the spec's worked
+clause-1 program:
+
+```
+(module loop_sum_to
+  (fn sum_to
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params n)
+    (body
+      (loop (acc Int 0) (i Int 1)
+        (if (app > i n)
+            acc
+            (recur (app + acc i) (app + i 1)))))))
+```
+
+(If the local `examples/*.ail` convention has no explicit
+`(module …)` wrapper, mirror an existing sibling fixture's header
+shape verbatim — e.g. `examples/sum.ail` — do not invent one. The
+fixture must `ail parse`-round-trip; it is NOT typechecked in
+iter 1, so `ail check` failing with the iter-1 `synth`
+`CheckError::Internal` stub is expected and is NOT this fixture's
+gate. The gate is `round_trip.rs` idempotency only.)
+
+- [ ] **Step 7: Run the full workspace suite + tail-app non-regression**
+
+Run: `cargo test --workspace 2>&1 | tail -15`
+Expected: PASS — all tests green, including
+`design_schema_drift`, `spec_drift`, `schema_coverage`,
+`hash_pin::loop_recur_schema_extension_preserves_pre_loop_recur_hashes`,
+`hash_pin::iter13a_schema_extension_preserves_pre_13a_hashes`
+(still green — proves additivity), and
+`round_trip::parse_then_print_then_parse_is_idempotent_on_every_ail_fixture`
+(auto-covers the new `examples/loop_sum_to.ail`).
+
+Run: `cargo test --workspace tail 2>&1 | tail -8`
+Expected: PASS — every existing `tail-app` / `tail-do` test
+byte-identical (this is the spec §"Testing strategy"
+"`tail-app` non-regression" gate and the operational evidence for
+Boss-call-1: `verify_tail_positions`' tail-app role is unchanged).
+
+---
+
+## Acceptance criteria (this iteration)
+
+- `Term::Loop` / `Term::Recur` / `struct LoopBinder` exist as
+  strictly-additive nodes with canonical JSON `"t":"loop"` /
+  `"t":"recur"`; `binders` has no `skip_serializing_if`.
+- `(loop …)` / `(recur …)` parse, print, and round-trip; the spec's
+  worked `sum_to` program is a green `examples/*.ail` fixture under
+  `round_trip.rs` auto-discovery.
+- Every exhaustive `match`-on-`Term` in all six crates + the three
+  drift tests has loop/recur arms; `cargo build --workspace` and
+  `cargo test --workspace` are green.
+- Pre-existing canonical-JSON hashes are bit-stable
+  (`iter13a` + the new `loop_recur` hash pin both green).
+- NO typecheck semantics (`synth` returns the `CheckError::Internal`
+  stub for Loop/Recur) and NO real codegen (`lower_term` returns
+  the `CodegenError::Internal` stub) — those are iters 2 and 3.
+- `tail-app` / `tail-do` / Decision-8 tests byte-identical; no
+  `Diverge`, no `verify_structural_recursion`, no
+  `NonStructuralRecursion`, no `verify_loop_body` (iter 2).
+- `verify_tail_positions`' tail-app verification role is unchanged
+  (operational evidence: the tail-app non-regression test in
+  Task 7 Step 7), satisfying the spec's "byte-unchanged"
+  acceptance criterion under the Boss-call-1 reading.
+
+## Cross-references
+
+- Parent spec: `docs/specs/2026-05-17-loop-recur.md`
+  (Components 1/2/3/6 = this iter; Component 4 = iter 2;
+  Component 5 = iter 3).
+- mut.1 precedent for the additive-node-across-no-wildcard-workspace
+  pattern + the `Internal`-stub-at-the-two-dispatch-points shape:
+  `docs/specs/2026-05-15-mut-local.md` §"Iteration mut.1".
+- Boss-call-1 (`verify_tail_positions` byte-unchanged reading) and
+  Boss-call-2 (codegen in iter-1 as stubs) are recorded in the
+  plan header above and must be mirrored into the per-iter journal
+  at iter close.