diff --git a/docs/plans/2026-05-16-iter-revert.md b/docs/plans/2026-05-16-iter-revert.md
new file mode 100644
index 0000000..00a9b93
--- /dev/null
+++ b/docs/plans/2026-05-16-iter-revert.md
@@ -0,0 +1,521 @@
+# Iteration-discipline revert — Implementation Plan
+
+> **Parent spec:** `docs/specs/2026-05-16-iteration-discipline-revert.md`
+>
+> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
+> to run this plan. Steps use `- [ ]` checkboxes for tracking.
+
+**Goal:** Surgically revert the Iteration-discipline milestone (it.1
+`96db54d` + it.2 `a4be1e5`) forward against the `1ff7e81` tree as byte
+oracle, keeping feature-acceptance clause 3 and the F3 todo, and add
+one honest F1/F4 DESIGN.md note.
+
+**Architecture:** One forward iteration. `main` is sacrosanct — NO
+`git revert`/`git reset`. For every *restored* region the byte oracle
+is `git show 1ff7e81:<path>`; the implementer makes the region
+byte-identical to the oracle and verifies with a targeted `diff`.
+Net-new it.1/it.2 surface is deleted outright. DESIGN.md is edited
+hunk-by-hunk in place (NEVER wholesale-restored — `1ff7e81` has no
+clause 3). Tasks are clustered on the recon's lockstep-invariant
+pairs so each task leaves the workspace compiling.
+
+**Tech Stack:** `ailang-core`, `ailang-check`, `ailang-surface`,
+`ailang-prose`, `ailang-codegen`, `ail` CLI; `cargo test --workspace`;
+`git show 1ff7e81:` as the restoration oracle.
+
+**Oracle convention (used by every task):** to restore a region,
+`git show 1ff7e81:<path> > /tmp/oracle_<name>` and diff the edited
+file's region against it; "matches oracle" means
+`diff <(sed -n 'A,Bp' <file>) <(sed -n 'C,Dp' /tmp/oracle_<name>)`
+is empty for the corresponding regions, OR the symbol is absent in
+both. The recon line-map (below, per task) is the *map* of what/where;
+the oracle is the *authority* on every byte. Line numbers drift as
+edits land — always re-locate symbols by name, not by frozen line.
+
+---
+
+## Task 1: AST node family + lockstep drift anchors + DESIGN.md §Data-model
+
+Removing `Term::Loop`/`Term::Recur` from the enum forces the
+exhaustive-match arms in three drift tests and the DESIGN.md
+§Data-model anchors to move in the same change (recon cross-ref #1,
+#2), else the crate is non-exhaustive / a drift test asserts a
+missing anchor.
+
+**Files:**
+- Modify: `crates/ailang-core/src/ast.rs` (`Term::Loop` ~540-546, `Term::Recur` ~547-552, `struct LoopBinder` ~596-605, serde units `term_loop_round_trips_through_json` ~974-998, `term_recur_empty_args_round_trips` ~1000-1009)
+- Modify: `crates/ailang-core/tests/design_schema_drift.rs` (loop tuple ~156-160, recur tuple ~161-164, match arms ~186-187)
+- Modify: `crates/ailang-core/tests/spec_drift.rs` (loop tuple ~133-139, recur tuple ~140, arms ~165-166)
+- Modify: `crates/ailang-core/tests/schema_coverage.rs` (Loop arm ~251-258, Recur arm ~259)
+- Modify: `docs/DESIGN.md` (§Data-model loop/recur JSON ~2422-2436 AND prose ~2452-2465)
+
+- [ ] **Step 1: Capture the AST oracle**
+
+Run: `git show 1ff7e81:crates/ailang-core/src/ast.rs > /tmp/oracle_ast.rs`
+Expected: file written; `grep -c 'Term::Loop\|Loop {' /tmp/oracle_ast.rs` prints `0`.
+
+- [ ] **Step 2: Remove `Term::Loop`, `Term::Recur`, `struct LoopBinder` + serde units**
+
+Delete the `Loop { binders, body }` and `Recur { args }` variants from the `Term` enum, the `struct LoopBinder { ... }` definition, and the two `#[cfg(test)]` serde units (`term_loop_round_trips_through_json`, `term_recur_empty_args_round_trips`). The enum's last variant returns to `Assign` exactly as in `/tmp/oracle_ast.rs`.
+
+- [ ] **Step 3: Verify the `Term` enum + serde region is byte-identical to oracle**
+
+Run: `diff <(grep -n 'enum Term' -A120 crates/ailang-core/src/ast.rs) <(grep -n 'enum Term' -A120 /tmp/oracle_ast.rs)`
+Expected: empty (the enum body matches `1ff7e81`).
+Run: `grep -nc 'Loop\|Recur\|LoopBinder' crates/ailang-core/src/ast.rs`
+Expected: `0`.
+
+- [ ] **Step 4: Remove loop/recur exemplars + match arms in the three drift tests**
+
+In `design_schema_drift.rs`, `spec_drift.rs`, `schema_coverage.rs`: delete the loop/recur exemplar tuples and the `Term::Loop => "loop"` / `Term::Recur => "recur"` exhaustive-match arms. Oracle each test file region against `git show 1ff7e81:crates/ailang-core/tests/<file>`.
+
+- [ ] **Step 5: Remove the DESIGN.md §Data-model loop/recur hunks**
+
+Delete `docs/DESIGN.md` lines covering the it.1 loop/recur JSON block (~2422-2436) and the it.1/it.2 prose paragraphs (~2452-2465: "`loop`/`recur` are additive as of iter it.1 … through it.2."). Do NOT touch anything else in DESIGN.md (clause 3, Decision 3 — later tasks). Re-locate by the literal strings `"t": "loop"` / "additive as of iter it.1", not by frozen line.
+
+- [ ] **Step 6: Compile + drift tests green for the AST surface**
+
+Run: `cargo build -p ailang-core 2>&1 | tail -3`
+Expected: builds (no non-exhaustive-match error).
+Run: `cargo test -p ailang-core --test design_schema_drift --test spec_drift --test schema_coverage 2>&1 | tail -5`
+Expected: PASS; no assertion referencing `"t": "loop"`/`"t": "recur"`.
+
+---
+
+## Task 2: `CheckError` variant + `code()` + the three dedicated `ctx()` arms
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs` (variants `RecurOutsideLoop` ~706, `RecurArityMismatch` ~711, `RecurTypeMismatch` ~716-721, `RecurNotInTailPosition` ~727, `NonStructuralRecursion` ~737 incl. doc lines; `code()` arms ~791-795; dedicated `ctx()` arms `RecurArityMismatch` ~870-872 / `RecurTypeMismatch` ~873-875 / `NonStructuralRecursion` ~876-878)
+- Verify-only: `crates/ailang-check/src/diagnostic.rs` (no loop/recur entries — confirm, no edit)
+
+- [ ] **Step 1: Capture the check oracle**
+
+Run: `git show 1ff7e81:crates/ailang-check/src/lib.rs > /tmp/oracle_check.rs`
+Expected: written; `grep -c 'RecurOutsideLoop\|NonStructuralRecursion' /tmp/oracle_check.rs` prints `0`.
+
+- [ ] **Step 2: Delete the five `CheckError` variants (with their doc comments)**
+
+Remove `RecurOutsideLoop`, `RecurArityMismatch`, `RecurTypeMismatch`, `RecurNotInTailPosition`, `NonStructuralRecursion` from the `CheckError` enum, including their `///` doc lines. Re-locate by variant name.
+
+- [ ] **Step 3: Delete their five `code()` arms**
+
+In `fn code(&self)`, delete the five contiguous arms returning the loop/recur/non-structural code strings (~791-795). The enum + `code()` must remain exhaustive over the *remaining* variants.
+
+- [ ] **Step 4: Delete the three dedicated `ctx()` arms (non-uniform — only three)**
+
+In `fn ctx(&self)`, delete ONLY the `RecurArityMismatch`, `RecurTypeMismatch`, `NonStructuralRecursion` arms (~870-878). Do NOT touch the `_ =>` catch-all (~879) — `RecurOutsideLoop`/`RecurNotInTailPosition` correctly fell into it and now simply no longer exist.
+
+- [ ] **Step 5: Confirm `diagnostic.rs` is a genuine no-op**
+
+Run: `grep -nE 'recur|loop|non-structural' crates/ailang-check/src/diagnostic.rs`
+Expected: no output (the `//!` "Stable codes" list ends at mq.3; nothing to revert here — confirms spec/recon).
+
+- [ ] **Step 6: Verify variants gone (build will still fail until Task 4 — expected)**
+
+Run: `grep -nc 'RecurOutsideLoop\|RecurArityMismatch\|RecurTypeMismatch\|RecurNotInTailPosition\|NonStructuralRecursion' crates/ailang-check/src/lib.rs`
+Expected: `0`.
+Note: `cargo build -p ailang-check` is NOT expected to pass yet — the `synth`/walker arms that *raise* these variants are removed in Tasks 3-5. This task's gate is the grep, not a build.
+
+---
+
+## Task 3: Remove the it.2 guardedness pass + `Diverge`-injection (restore effect reconcile to `1ff7e81`)
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs` — `verify_structural_recursion` (~3175-3268), its raise of `NonStructuralRecursion` (~3264), helpers `mutual_structural_group` (~3373) / `adt_families` (~3336) / `referenced_con_names` (~3310) **iff absent at `1ff7e81`**, `term_contains_loop` (~2871-2917) + its three callers / Diverge-injection sites (FnDef body ~2074-2077, lam-arrow ~4314/4331-4334, LetRec ~4412/4431-4432), the `verify_structural_recursion` call site (~2063).
+
+- [ ] **Step 1: Determine helper provenance against the oracle**
+
+Run: `for s in verify_structural_recursion term_contains_loop verify_loop_body mutual_structural_group adt_families referenced_con_names; do echo -n "$s @1ff7e81: "; grep -c "fn $s" /tmp/oracle_check.rs; done`
+Expected: `verify_structural_recursion`, `term_contains_loop`, `verify_loop_body`, `mutual_structural_group` print `0` (it.2-net-new → delete). `adt_families`/`referenced_con_names`: whatever the oracle prints — `0` ⇒ delete, `≥1` ⇒ KEEP (pre-existing; do not remove). Record the verdict for each in the iter journal.
+
+- [ ] **Step 2: Delete `verify_structural_recursion` and its it.2-only helpers**
+
+Delete the whole `fn verify_structural_recursion` and every helper Step 1 proved absent at `1ff7e81`. Keep any helper Step 1 proved pre-existing. Delete the call site of `verify_structural_recursion` (the line `verify_structural_recursion(...)?;` ~2063).
+
+- [ ] **Step 3: Delete `term_contains_loop` and restore the three Diverge-injection sites to `1ff7e81`**
+
+Delete `fn term_contains_loop`. At each of its three call sites (FnDef-body effect reconcile, lam-arrow, LetRec), restore the effect-reconciliation code to its `1ff7e81` form using `/tmp/oracle_check.rs` as the per-region oracle (the `1ff7e81` code has NO `Diverge` antecedent — no `term_contains_loop` call, no `Diverge` push). Diff each region against the oracle.
+
+- [ ] **Step 4: Verify the guardedness/Diverge surface is gone and effect-reconcile matches oracle**
+
+Run: `grep -nc 'verify_structural_recursion\|term_contains_loop' crates/ailang-check/src/lib.rs`
+Expected: `0`.
+Run: `diff <(grep -n 'fn reconcile\|effects.*Diverge\|declared.*effect' crates/ailang-check/src/lib.rs) <(grep -n 'fn reconcile\|effects.*Diverge\|declared.*effect' /tmp/oracle_check.rs)` (anchor the comparison on the reconcile fn the implementer identified in Step 3)
+Expected: empty for the reconcile region (no residual `Diverge` injection).
+
+---
+
+## Task 4: Remove it.1 check surface — `synth` `loop_stack`, Loop/Recur arms, `verify_loop_body`, `verify_tail_positions` it.1 arms
+
+`verify_tail_positions` is pre-it.1 (oracle `fn verify_tail_positions` at `1ff7e81:2590`) — the function SURVIVES; only its it.1 `Term::Loop`/`Term::Recur` arms are deleted. `synth` loses the it.1 `loop_stack` parameter, forcing every threaded call site + local decl back to the `1ff7e81` signature (recon cross-ref #4).
+
+**Files:**
+- Modify: `crates/ailang-check/src/lib.rs` — `synth` signature (`loop_stack` param ~3612) + ~30 threaded call sites + `let mut loop_stack` local decls (recon list: ~2045-2046, 3579-3580, 4001-4654 cluster, 5043/5082/5124/5239/5280/5320/5423/8163); synth `Term::Loop` arm ~4599-4628, synth `Term::Recur` arm ~4641-; `clone_term` rebuild arms ~267-289; post-mono walker arms ~3131-3145 / 3491 / 3549 / 4494-4495; `verify_loop_body` ~2819-2869 (whole it.1 helper); `verify_tail_positions` it.1 arms ~2798-2815.
+
+- [ ] **Step 1: Confirm the `1ff7e81` `synth` signature**
+
+Run: `grep -n 'fn synth' /tmp/oracle_check.rs | head -1`
+Expected: prints the `1ff7e81` `synth` signature (no `loop_stack` parameter). Record it; it is the target signature.
+
+- [ ] **Step 2: Delete the synth `Term::Loop` / `Term::Recur` arms and `verify_loop_body`**
+
+Delete both synth match arms for `Term::Loop`/`Term::Recur` (incl. the `loop_stack.push/.pop` lines) and the whole `fn verify_loop_body`.
+
+- [ ] **Step 3: Remove the it.1 arms from `verify_tail_positions` (function survives)**
+
+Delete ONLY the `Term::Loop`/`Term::Recur` arms inside `verify_tail_positions`. Then diff the whole function against the oracle: `diff <(sed -n '/fn verify_tail_positions/,/^}/p' crates/ailang-check/src/lib.rs) <(sed -n '/fn verify_tail_positions/,/^}/p' /tmp/oracle_check.rs)` — Expected: empty (the function is byte-identical to its `1ff7e81` form).
+
+- [ ] **Step 4: Drop the `loop_stack` parameter from `synth` and every call/decl**
+
+Restore `fn synth` to the Step-1 signature. Remove the `loop_stack` argument from every `synth(...)` call and delete every `let mut loop_stack: Vec<Vec<Type>> = ...` local. Remove `clone_term` Loop/Recur arms and the post-mono Loop/Recur walker arms (incl. the `"loop"`/`"recur"` name-string arms ~4494-4495).
+
+- [ ] **Step 5: `ailang-check` compiles**
+
+Run: `cargo build -p ailang-check 2>&1 | tail -3`
+Expected: builds clean.
+Run: `grep -nc 'Term::Loop\|Term::Recur\|loop_stack\|verify_loop_body' crates/ailang-check/src/lib.rs`
+Expected: `0`.
+
+---
+
+## Task 5: Remove Loop/Recur walker arms from the remaining `ailang-check` + `ailang-core` modules
+
+**Files:**
+- Modify: `crates/ailang-check/src/lift.rs` (~400-419, 749-750, 787-790)
+- Modify: `crates/ailang-check/src/mono.rs` (~717-725, 1247-1257, 1362-1369, 1635-1645)
+- Modify: `crates/ailang-check/src/linearity.rs` (~612-620, 809-810, 953-958)
+- Modify: `crates/ailang-check/src/uniqueness.rs` (~355-361)
+- Modify: `crates/ailang-check/src/reuse_shape.rs` (~268-274)
+- Modify: `crates/ailang-check/src/pre_desugar_validation.rs` (~136-142)
+- Modify: `crates/ailang-check/src/builtins.rs` (~346-358, 591-603)
+- Modify: `crates/ailang-core/src/desugar.rs` (~366-373, 605-628, 1275-1287, 1485-1519, 1663-1674, 1755-1759, 1807-1810, 1841-1844, 2966-2969)
+- Modify: `crates/ailang-core/src/workspace.rs` (~1262-1272, 1411-1417)
+
+- [ ] **Step 1: Capture oracles for the walker files**
+
+Run: `for f in lift mono linearity uniqueness reuse_shape pre_desugar_validation builtins; do git show 1ff7e81:crates/ailang-check/src/$f.rs > /tmp/oracle_$f.rs; done; for f in desugar workspace; do git show 1ff7e81:crates/ailang-core/src/$f.rs > /tmp/oracle_core_$f.rs; done`
+Expected: written; `grep -lc 'Term::Loop' /tmp/oracle_*.rs /tmp/oracle_core_*.rs` prints nothing (none contain Loop arms at `1ff7e81`).
+
+- [ ] **Step 2: Delete every Loop/Recur arm + `loop_stack` decl in the seven check modules**
+
+For each `ailang-check` file above: delete the `Term::Loop`/`Term::Recur` match arms and any `let mut loop_stack` decl. Diff each file against its `/tmp/oracle_<f>.rs` and make it match.
+
+- [ ] **Step 3: Delete every Loop/Recur arm in `desugar.rs` and `workspace.rs`**
+
+Same, for `crates/ailang-core/src/desugar.rs` and `workspace.rs`, against `/tmp/oracle_core_<f>.rs`.
+
+- [ ] **Step 4: Workspace-wide grep is clean for check+core**
+
+Run: `grep -rnc 'Term::Loop\|Term::Recur' crates/ailang-check/src crates/ailang-core/src | grep -v ':0'`
+Expected: no output.
+Run: `cargo build -p ailang-check -p ailang-core 2>&1 | tail -3`
+Expected: builds clean.
+
+---
+
+## Task 6: Surface + Prose + Form-A grammar
+
+**Files:**
+- Modify: `crates/ailang-surface/src/parse.rs` (`parse_loop` ~1656-1706, `parse_recur` ~1712-1721, dispatch arms ~1217-1218, keyword-list entry ~1227, EBNF `//!` block lines ~43/71/73-74, surface units `parses_loop_with_one_binder_and_recur_body` ~2665-2680, `parses_recur_zero_args` ~2682-2688)
+- Modify: `crates/ailang-surface/src/print.rs` (`Term::Loop` arm ~597-633, `Term::Recur` arm ~634-644)
+- Modify: `crates/ailang-prose/src/lib.rs` (`write_term` Loop/Recur ~938-968, `count_free_var` ~1170-1186, `subst_var_with_term` ~1339-1371, lockstep unit ~2188-2220)
+- Modify: `crates/ailang-core/specs/form_a.md` (grammar ~287-288, semantics ~327-342)
+
+- [ ] **Step 1: Capture oracles**
+
+Run: `git show 1ff7e81:crates/ailang-surface/src/parse.rs > /tmp/oracle_parse.rs; git show 1ff7e81:crates/ailang-surface/src/print.rs > /tmp/oracle_print.rs; git show 1ff7e81:crates/ailang-prose/src/lib.rs > /tmp/oracle_prose.rs; git show 1ff7e81:crates/ailang-core/specs/form_a.md > /tmp/oracle_forma.md`
+Expected: written.
+
+- [ ] **Step 2: parse.rs — remove parse_loop/parse_recur, dispatch, keyword list, EBNF, units**
+
+Delete `fn parse_loop`, `fn parse_recur`, their dispatch arms, the `loop`/`recur` entries in the error keyword list (oracle line ~1222-1223: `…, `mut`, `assign`, `lit-unit``), the EBNF `//!` lines for `loop-term`/`recur-term`, and the two surface units. Diff parse.rs against `/tmp/oracle_parse.rs`.
+
+- [ ] **Step 3: print.rs + prose lib.rs — remove the Loop/Recur arms + prose lockstep unit**
+
+Delete the `Term::Loop`/`Term::Recur` arms in `print.rs::write_term` and in `prose/src/lib.rs` (`write_term`, `count_free_var`, `subst_var_with_term`) plus the prose lockstep unit test. Diff both against their oracles.
+
+- [ ] **Step 4: form_a.md — remove loop/recur grammar + semantics**
+
+Delete the loop/recur grammar entries (~287-288) and the semantics block (~327-342). Diff against `/tmp/oracle_forma.md`.
+
+- [ ] **Step 5: Surface + prose build + grep clean**
+
+Run: `cargo build -p ailang-surface -p ailang-prose 2>&1 | tail -3`
+Expected: builds clean.
+Run: `grep -rnc 'Term::Loop\|Term::Recur\|parse_loop\|parse_recur' crates/ailang-surface/src crates/ailang-prose/src | grep -v ':0'`
+Expected: no output.
+
+---
+
+## Task 7: Codegen — remove the loop lowering, keep the tail-driven seam
+
+The it.1 parallel `block_terminated` setter is the ONLY setter removed (`lib.rs:1996`, inside the Recur arm; the in-code comment ~1976-1978 is the authoritative boundary). The four tail-driven setters (`~2430` emit_call, `~2511` emit_indirect_call, `~2652`/`~2724` lower_effect_op) and the four control-flow terminators (`~1401/1625/2816/2862`) are pre-existing and STAY (recon cross-ref #7).
+
+**Files:**
+- Modify: `crates/ailang-codegen/src/lib.rs` (`loop_frames` field ~746, `struct LoopFrame` ~755-760, init ~880, clear ~1086, `Term::Loop` arm ~1873-1972, `Term::Recur` arm ~1979-1997 incl. the it.1 setter at ~1996, synth-shim arms ~3258-3259)
+- Modify: `crates/ailang-codegen/src/escape.rs` (~204-214, 409-417, 549-562)
+- Modify: `crates/ailang-codegen/src/lambda.rs` (`loop_frames` save ~152, restore ~267, arms ~518, ~531)
+- Modify: `crates/ail/src/main.rs` (Loop/Recur arms ~1549-1562, ~2811-2838)
+
+- [ ] **Step 1: Capture oracles**
+
+Run: `git show 1ff7e81:crates/ailang-codegen/src/lib.rs > /tmp/oracle_cg.rs; git show 1ff7e81:crates/ailang-codegen/src/escape.rs > /tmp/oracle_escape.rs; git show 1ff7e81:crates/ailang-codegen/src/lambda.rs > /tmp/oracle_cglam.rs; git show 1ff7e81:crates/ail/src/main.rs > /tmp/oracle_main.rs`
+Expected: written.
+
+- [ ] **Step 2: codegen lib.rs — remove loop lowering + the it.1 setter only**
+
+Delete the `Term::Loop` and `Term::Recur` lowering arms, the `loop_frames` field, `struct LoopFrame`, its init and clear, and the synth-shim Loop/Recur arms. The it.1 `self.block_terminated = true` at the old ~1996 (inside the deleted Recur arm) goes with the arm. Verify the four tail-driven setters survive: `grep -nc 'block_terminated = true' crates/ailang-codegen/src/lib.rs` must equal the `1ff7e81` count → Run: `grep -c 'block_terminated = true' /tmp/oracle_cg.rs` first and record it; the post-edit count must equal it.
+
+- [ ] **Step 3: escape.rs + lambda.rs + main.rs — remove Loop/Recur arms + loop_frames save/restore**
+
+Delete the escape-walk Loop/Recur arms, the `lambda.rs` `loop_frames` save/restore + arms, and the `ail/src/main.rs` Loop/Recur arms. Diff each against its oracle.
+
+- [ ] **Step 4: Whole workspace builds; codegen grep clean**
+
+Run: `grep -rnc 'Term::Loop\|Term::Recur\|loop_frames\|LoopFrame' crates/ailang-codegen/src crates/ail/src | grep -v ':0'`
+Expected: no output.
+Run: `cargo build --workspace 2>&1 | tail -3`
+Expected: builds clean (entire workspace now compiles post-revert).
+
+---
+
+## Task 8: Delete pin files, surgical e2e/pin-arm removal, carve_out_inventory, fixtures, bench
+
+**Files:**
+- Delete: `crates/ailang-check/tests/loop_recur_pin.rs`, `crates/ailang-check/tests/structural_recursion_pin.rs`
+- Modify: `crates/ail/tests/e2e.rs` (it.1 cases ~2831-2845+), `crates/ail/tests/codegen_import_map_fallback_pin.rs` (arms ~104-110)
+- Modify: `crates/ailang-core/tests/carve_out_inventory.rs` (doc ~17-23, `EXPECTED` entries+comments ~48-56 — **string-set, NOT a count**: remove the 7 it.1/it.2 `test_*.ail.json` entries + 2 comment lines)
+- Delete (16 net-new fixtures): `examples/loop_counter.ail`, `examples/loop_in_lambda_e2e.ail`, `examples/loop_needs_diverge.ail`, `examples/loop_nested_in_lambda.ail`, `examples/loop_smoke.ail`, `examples/struct_rec_foldl_sum.ail`, `examples/struct_rec_list_len.ail`, `examples/struct_rec_sum_e2e.ail`, `examples/struct_rec_tree_forest.ail`, `examples/test_loop_missing_diverge.ail.json`, `examples/test_mutual_cross_family.ail.json`, `examples/test_non_structural_recursion.ail.json`, `examples/test_recur_arity_mismatch.ail.json`, `examples/test_recur_not_in_tail_position.ail.json`, `examples/test_recur_outside_loop.ail.json`, `examples/test_recur_type_mismatch.ail.json`
+- Restore: `examples/rc_pin_recurse_implicit.ail`, `examples/rc_let_alias_implicit_param.ail` (to `git show 1ff7e81:`)
+- Delete: `bench/it3-oracle/` (MANIFEST.tsv + 40 `.out`)
+- KEEP (explicit no-op): `bench/orchestrator-stats/2026-05-15-iter-it.{1,2,3}.json` — historical record like journals/plans (Boss decision)
+
+- [ ] **Step 1: Re-verify the net-new vs modified fixture split against the live diff**
+
+Run: `git diff --stat 1ff7e81 HEAD -- examples/ bench/ | grep -E 'examples/|bench/'`
+Expected: the 16 named fixtures + every `bench/it3-oracle/*` show as net-new (`| N +` only); `rc_pin_recurse_implicit.ail`/`rc_let_alias_implicit_param.ail` show partial-modify (deletions present); `mut_counter.ail`/`mut_sum_floats.ail` absent (already `1ff7e81`). If any file contradicts this, STOP and report (do not guess).
+
+- [ ] **Step 2: Delete the two whole pin files + the 16 fixtures + bench/it3-oracle/**
+
+Run: `rm -f crates/ailang-check/tests/loop_recur_pin.rs crates/ailang-check/tests/structural_recursion_pin.rs examples/loop_counter.ail examples/loop_in_lambda_e2e.ail examples/loop_needs_diverge.ail examples/loop_nested_in_lambda.ail examples/loop_smoke.ail examples/struct_rec_foldl_sum.ail examples/struct_rec_list_len.ail examples/struct_rec_sum_e2e.ail examples/struct_rec_tree_forest.ail examples/test_loop_missing_diverge.ail.json examples/test_mutual_cross_family.ail.json examples/test_non_structural_recursion.ail.json examples/test_recur_arity_mismatch.ail.json examples/test_recur_not_in_tail_position.ail.json examples/test_recur_outside_loop.ail.json examples/test_recur_type_mismatch.ail.json && rm -rf bench/it3-oracle`
+Expected: exit 0.
+(Note: plain `rm` only — the implementer never touches the git index. These tracked-file deletions stay as working-tree changes; the Boss's `git add -A` at iter-commit time captures them. NOT a commit.)
+
+- [ ] **Step 3: Restore the two modified RC fixtures to `1ff7e81`**
+
+Run: `git show 1ff7e81:examples/rc_pin_recurse_implicit.ail > examples/rc_pin_recurse_implicit.ail && git show 1ff7e81:examples/rc_let_alias_implicit_param.ail > examples/rc_let_alias_implicit_param.ail && git diff --stat 1ff7e81 -- examples/rc_pin_recurse_implicit.ail examples/rc_let_alias_implicit_param.ail`
+Expected: empty (both now byte-identical to `1ff7e81`).
+
+- [ ] **Step 4: Surgically revert e2e.rs + codegen_import_map_fallback_pin.rs to `1ff7e81`**
+
+Diff `crates/ail/tests/e2e.rs` against `git show 1ff7e81:crates/ail/tests/e2e.rs` and remove exactly the it.1 added cases (loop_counter / loop-in-lambda / loop_frames E2E). Diff `crates/ail/tests/codegen_import_map_fallback_pin.rs` against its `1ff7e81` oracle and remove the `Term::Loop`/`Term::Recur` arms in `contains_xmod_show_var`. Verify each region matches the oracle.
+
+- [ ] **Step 5: carve_out_inventory.rs — remove the 7 string entries + 2 comment lines**
+
+Capture oracle: `git show 1ff7e81:crates/ailang-core/tests/carve_out_inventory.rs > /tmp/oracle_carve.rs`. Edit `EXPECTED` so its entry set + the doc comment is byte-identical to the oracle (last entry returns to `test_mut_var_captured_by_lambda.ail.json`). Diff against `/tmp/oracle_carve.rs` — Expected: empty.
+
+- [ ] **Step 6: Confirm bench/orchestrator-stats kept; full suite green**
+
+Run: `ls bench/orchestrator-stats/2026-05-15-iter-it.1.json bench/orchestrator-stats/2026-05-15-iter-it.2.json bench/orchestrator-stats/2026-05-15-iter-it.3.json && ls bench/it3-oracle 2>&1`
+Expected: the three stats json exist; `ls bench/it3-oracle` → "No such file or directory".
+Run: `cargo test --workspace 2>&1 | tail -8`
+Expected: PASS (whole suite green — the pinned-surface tests are gone, no orphan refs).
+
+---
+
+## Task 9: DESIGN.md Decision 3 + clause-3 de-claim + F1/F4 note + brainstorm SKILL.md de-claim + doc-presence test
+
+**Files:**
+- Modify: `docs/DESIGN.md` (Decision 3 it.2 prose ~168-176 → `1ff7e81` placeholder; clause-3 worked-example sentence ~105-110 de-claim; F1/F4 note added in §"Local mutable state" vicinity ~2918)
+- Modify: `skills/brainstorm/SKILL.md` (~107 worked-example reference de-claim)
+- Create: doc-presence test (a new `#[test]` in `crates/ailang-core/tests/design_schema_drift.rs`)
+
+- [ ] **Step 1: Restore Decision 3 to the `1ff7e81` placeholder (hunk-only)**
+
+Run: `git show 1ff7e81:docs/DESIGN.md | sed -n '/## Decision 3/,/## Decision 4/p' > /tmp/oracle_d3.md`
+Replace the current Decision 3 body (the it.2 paragraph "As of iter it.2 … unbounded `loop`.") with the `1ff7e81` placeholder text from `/tmp/oracle_d3.md` (the placeholder is the single sentence: `In the MVP only the effects IO and Diverge (for infinite loops) are wired up.`). Edit ONLY between `## Decision 3` and `## Decision 4`. Verify: `diff <(sed -n '/## Decision 3/,/## Decision 4/p' docs/DESIGN.md) /tmp/oracle_d3.md` → empty.
+
+- [ ] **Step 2: De-claim the clause-3 worked example (KEEP the block, de-claim the sentence)**
+
+Locate the clause-3 sentence at DESIGN.md ~105-110: *"The canonical worked example is the iteration story: a bare `while` over mutable state passes 1 and 2 yet fails 3 (it reinstates iterated-mutable-state reasoning); structural recursion over an acyclic ADT and a named loop/recur point pass all three (the bug class is closed by construction, not by advice)."*
+Replace with (hypothetical-illustration form — the `loop`/`recur` machinery no longer exists, so it must not read as shipped):
+
+> The criterion's discriminator is whether the wrong code fails to typecheck, not whether a guideline advises against it. Worked example: a bare `while` over mutable state would pass clauses 1 and 2 yet fail clause 3 (it reinstates iterated-mutable-state reasoning the pure core exists to remove); a hypothetical "all repetition is either structurally-decreasing recursion over an acyclic ADT or an explicit named loop" iteration story would, *if it could be built without a documented-unenforced precondition*, pass all three — and the fact that the 2026-05 attempt could not (it forced a silent-divergence precondition; see `docs/specs/2026-05-16-iteration-discipline-revert.md`) is itself the clause-3 mechanism working as intended.
+
+- [ ] **Step 3: De-claim the brainstorm SKILL.md reference in lockstep**
+
+In `skills/brainstorm/SKILL.md` ~107, change "(with the canonical worked example — the iteration story)" to "(with the canonical worked example — see the criterion text)" so it no longer asserts the iteration story shipped. Verify: `grep -n 'iteration story' skills/brainstorm/SKILL.md` → no line claims it as a shipped example.
+
+- [ ] **Step 4: Add the F1/F4 documentation note**
+
+In `docs/DESIGN.md`, in the §"Local mutable state" vicinity (after the bullet ending `Spec: docs/specs/2026-05-15-mut-local.md.` ~line 2918, before "Pipeline regression smoke tests:"), insert verbatim:
+
+> **Accumulator-over-iteration shape (documented idiom, not an enforced rule).** `mut`/`var`/`assign` removes friction from *straight-line* and *cascade-of-if* accumulators, but does **not** by itself express the "one running total updated once per loop iteration" shape: a `var` cannot be captured into a lambda (the seal) and there is no loop construct in the language. Until a future iteration-totality milestone lands (gated behind `Nat`/refinement types — see the deferred roadmap entry), the canonical pattern for the per-iteration accumulator is a tail-recursive helper that threads the running total as an explicit parameter; `examples/mut_counter.ail` is the reference. This is a documented authoring idiom, not a typecheck-enforced constraint — wrong code here does not fail to compile, it is merely less ergonomic, which is exactly why this is documentation and not a language rule.
+
+- [ ] **Step 5: Add the doc-presence guard test**
+
+In `crates/ailang-core/tests/design_schema_drift.rs` add:
+
+```rust
+#[test]
+fn design_md_documents_the_accumulator_over_iteration_idiom() {
+    let design = std::fs::read_to_string(
+        concat!(env!("CARGO_MANIFEST_DIR"), "/../../docs/DESIGN.md"),
+    )
+    .expect("read DESIGN.md");
+    assert!(
+        design.contains("Accumulator-over-iteration shape (documented idiom, not an enforced rule)"),
+        "the F1/F4 documented-idiom note must not be silently dropped from DESIGN.md"
+    );
+    assert!(
+        design.contains("examples/mut_counter.ail is the reference")
+            || design.contains("`examples/mut_counter.ail` is the reference"),
+        "the F1/F4 note must keep pointing at the canonical fallback fixture"
+    );
+}
+```
+
+- [ ] **Step 6: Verify clause 3 still present, Decision 3 reverted, note guarded**
+
+Run: `grep -c 'clauses 1 and 2 yet fail clause 3\|fails clause 3\|fail 3' docs/DESIGN.md`
+Expected: `≥1` (clause-3 block retained, only de-claimed).
+Run: `cargo test -p ailang-core --test design_schema_drift design_md_documents_the_accumulator_over_iteration_idiom 2>&1 | tail -3`
+Expected: PASS.
+
+---
+
+## Task 10: Roadmap + superseded spec header + journal
+
+**Files:**
+- Modify: `docs/roadmap.md` (remove the Iteration-discipline `[~]` entry + blocking-fork sub-section, contiguous ~43-178; add one deferred entry; KEEP F3 ~375-382 + Stateful-islands untouched)
+- Modify: `docs/specs/2026-05-15-iteration-discipline.md` (add superseded header — file is already clean; the A1 discard was done Boss-side pre-plan, so this is the ONLY edit to this file)
+- Create: `docs/journals/2026-05-16-iter-revert.md` (the iter journal — written by the implement skill at iter close)
+- Modify: `docs/journals/INDEX.md` (append the new journal line)
+
+- [ ] **Step 1: Remove the Iteration-discipline roadmap block, add the deferred entry**
+
+Delete the contiguous `- [~] **[milestone]** Iteration discipline …` entry and its "blocking fork" sub-section (recon: roadmap.md ~43-178, ending just before `- [x] **[milestone]** Heap-Str ABI`). In its place under **P2 — Medium-term** (or P3 if judged not decision-ready — Boss/implementer keeps it P2 as a decided-but-deferred direction), insert verbatim:
+
+```markdown
+- [ ] **\[milestone\]** Iteration-totality story — structural +
+  Int-bounded total recursion with *enforced* non-negativity.
+  AILang's iteration story stays as-is (structural / tail recursion;
+  `tail-app` intact). The genuine ambition — make `f(n-1)`-family
+  recursion (incl. branching tree builders) total *by construction*
+  with the non-negative-entry precondition **enforced**, not merely
+  documented — is deferred here because doing it without a purity-
+  pillar concession requires refinement/`Nat` type machinery the
+  language has not built (Decision 4 keeps refinements opaque, no
+  SMT). Not abandoned; correctly sequenced after the type machinery.
+  - depends on: a future `Nat`/refinement-types milestone (no spec
+    yet).
+  - context: `docs/specs/2026-05-16-iteration-discipline-revert.md`
+    (why the 2026-05 attempt was reverted) and
+    `docs/journals/2026-05-15-iter-it.3.md` (the branching-builder
+    counter-example that surfaced the gap).
+```
+
+- [ ] **Step 2: Verify F3 + Stateful-islands untouched**
+
+Run: `grep -n 'zero-arg\|(app f)\|Stateful islands\|Stateful-islands' docs/roadmap.md | head`
+Expected: the F3 todo and the Stateful-islands milestone entry are still present and unchanged (the only roadmap removal is the Iteration-discipline block; the deleted block's internal "supersedes the while-loops-legal scope bullet" cross-reference disappears with it, which is correct).
+
+- [ ] **Step 3: Add the superseded header to the old spec**
+
+At the very top of `docs/specs/2026-05-15-iteration-discipline.md` (before `# Iteration discipline — Design Spec`), insert verbatim:
+
+```markdown
+> **SUPERSEDED 2026-05-16 by
+> `docs/specs/2026-05-16-iteration-discipline-revert.md`.** This
+> milestone was reverted in full (it.1 + it.2 backed out forward;
+> it.3 never ran). It is retained as a historical record of the
+> attempt and the design-thesis gap it surfaced; it is **not** the
+> current iteration-story design. Do not plan or implement from this
+> file.
+
+```
+
+- [ ] **Step 4: Confirm working tree of the old spec is otherwise clean**
+
+Run: `git diff --stat 1ff7e81 -- docs/specs/2026-05-15-iteration-discipline.md`
+Expected: shows ONLY the spec's committed history relative to `1ff7e81` plus the new header line as a working-tree change — i.e. there is no residual A1 amendment (it was discarded Boss-side pre-plan). If unexpected uncommitted body changes appear, STOP and report.
+
+---
+
+## Task 11: Behavioural-equivalence sweep + whole-suite gate (the correctness gate)
+
+The structural revert is necessary but not sufficient; this task
+proves the *compiler behaviour* returned to `1ff7e81` for the
+surviving corpus.
+
+**Files:** none modified — verification only.
+
+- [ ] **Step 1: Build the `1ff7e81` reference compiler in a throwaway worktree**
+
+Run: `git worktree add /tmp/ail-1ff7e81 1ff7e81 && (cd /tmp/ail-1ff7e81 && cargo build -p ail 2>&1 | tail -1)`
+Expected: a built `ail` at `/tmp/ail-1ff7e81/target/debug/ail`.
+
+- [ ] **Step 2: Capture the `1ff7e81` corpus behaviour oracle**
+
+Run:
+```
+mkdir -p /tmp/eqv_old
+for f in $(cd /tmp/ail-1ff7e81 && ls examples/*.ail); do
+  base=$(basename "$f")
+  (cd /tmp/ail-1ff7e81 && ./target/debug/ail check "examples/$base" > "/tmp/eqv_old/$base.check" 2>&1; \
+   ./target/debug/ail run "examples/$base" > "/tmp/eqv_old/$base.run" 2>&1; echo "$? " > "/tmp/eqv_old/$base.rc")
+done
+ls /tmp/eqv_old | wc -l
+```
+Expected: a non-zero count of captured `.check`/`.run`/`.rc` triples (the `1ff7e81` corpus).
+
+- [ ] **Step 3: Run the post-revert compiler over the same corpus and diff**
+
+Run:
+```
+cargo build -p ail 2>&1 | tail -1
+fail=0
+for f in $(ls examples/*.ail); do
+  base=$(basename "$f")
+  [ -f "/tmp/eqv_old/$base.check" ] || continue   # only fixtures that existed at 1ff7e81
+  ./target/debug/ail check "examples/$base" > "/tmp/new.check" 2>&1
+  ./target/debug/ail run "examples/$base" > "/tmp/new.run" 2>&1
+  diff -q "/tmp/eqv_old/$base.check" "/tmp/new.check" >/dev/null 2>&1 || { echo "CHECK DRIFT: $base"; fail=1; }
+  diff -q "/tmp/eqv_old/$base.run"   "/tmp/new.run"   >/dev/null 2>&1 || { echo "RUN DRIFT: $base"; fail=1; }
+done
+echo "fail=$fail"
+```
+Expected: `fail=0`, no "DRIFT" lines (every surviving fixture behaves byte-identically to `1ff7e81`). Any drift is a revert defect — fix it before the task closes (do NOT ratify; the spec mandates *pristine*, not ratified).
+
+- [ ] **Step 4: Whole-suite gate + worktree cleanup**
+
+Run: `cargo test --workspace 2>&1 | tail -8`
+Expected: PASS (all crates green).
+Run: `grep -rnc 'Term::Loop\|Term::Recur\|verify_structural_recursion\|term_contains_loop\|loop_stack\|loop_frames\|RecurOutsideLoop\|NonStructuralRecursion' crates/ docs/DESIGN.md crates/ailang-core/specs/form_a.md | grep -v ':0' | grep -v 'docs/specs\|docs/journals\|docs/plans'`
+Expected: no output (zero residual it.1/it.2 production surface; historical docs under specs/journals/plans legitimately still mention them).
+Run: `git worktree remove --force /tmp/ail-1ff7e81`
+Expected: worktree removed.
+
+---
+
+## Notes for the implement skill
+
+- This is a revert: for every *Modify-to-restore* step the oracle
+  `git show 1ff7e81:<path>` is the authority on every byte; the
+  line numbers in this plan are the recon map (drift as edits land —
+  re-locate by symbol name). For *Delete* and *net-add* steps the
+  plan gives the exact command / verbatim text (Iron Law satisfied:
+  nothing is undecided).
+- Tasks 2-7 will not individually `cargo build` green until the
+  whole check/codegen surface is removed (the variants are raised
+  before they are deleted); each such task's gate is its grep, and
+  the first full-workspace build gate is **Task 7 Step 4**. This is
+  intentional task clustering on the recon lockstep pairs, not a
+  plan defect.
+- No `git commit` anywhere. All deletions/edits stay in the working
+  tree (incl. `git rm` staged deletes); the Boss commits the whole
+  revert as one cohesive iter at the end.
+- The iter journal `docs/journals/2026-05-16-iter-revert.md` +
+  `INDEX.md` line are written by the implement skill at iter close
+  (Task 10 lists them so the file-map is complete; they are not a
+  numbered code step).