diff --git a/docs/specs/2026-05-16-iteration-discipline-revert.md b/docs/specs/2026-05-16-iteration-discipline-revert.md
new file mode 100644
index 0000000..c15dcc2
--- /dev/null
+++ b/docs/specs/2026-05-16-iteration-discipline-revert.md
@@ -0,0 +1,358 @@
+# Iteration-discipline revert — Design Spec
+
+**Date:** 2026-05-16
+**Status:** Draft — awaiting user spec review
+**Authors:** Brummel (orchestrator) + Claude
+
+## Goal
+
+Back the *Iteration-discipline* milestone out of the working language
+and restore the pre-milestone iteration story, by a single **forward**
+iteration (`main` is sacrosanct — no `git reset`/`git revert` of the
+shipped commits `96db54d`/`a4be1e5`).
+
+Why this is a milestone, not a tidy iteration: the milestone being
+removed was an *identity-level* change (a new AST node family, a new
+checker pass, a new effect, DESIGN.md Decision-3 prose). Reverting it
+is an equally identity-level decision about what AILang's iteration
+story *is*, and it touches DESIGN.md invariants. It earns a spec.
+
+Root cause being corrected (recorded so a future reader does not
+re-derive the same mistake):
+
+- The milestone was scoped from fieldtest finding **F1**
+  (`docs/specs/2026-05-15-fieldtest-mut-local.md`), which was tagged
+  `[friction]` and whose *own* summary table named the honest minimal
+  action: "tighten DESIGN.md to name the gap — less work, more
+  honest". It was instead escalated into "retire `tail-app`,
+  recursion is total-by-construction, add `Diverge`".
+- That thesis recognised exactly **one** total-by-construction
+  scheme (ADT-structural over an acyclic ADT). The it.3 corpus sweep
+  proved it incomplete: `build(d: Int) = if d==0 then Leaf else
+  Node(1, build(d-1), build(d-1))` — the single most LLM-natural
+  tree-builder — is neither ADT-structural nor `loop`/`recur`-able,
+  so the milestone *as specified* made a trivially-total,
+  maximally-natural function inexpressible (it.3 BLOCKED).
+- The only in-thesis escape (A1 / it.2b — Int-bounded recursion as a
+  second total class) requires conceding the language's **first**
+  documented-but-unenforced totality precondition (`build(-1)`
+  diverges silently; Decision 4 keeps refinements opaque with no SMT,
+  so `p >= 0` is unenforceable today *by construction*). That is a
+  dilution of a purity pillar the user personally co-designed.
+- `loop`/`recur` (it.1) was never run through the feature-acceptance
+  gate for LLM-naturalness in its own right; it rode in on the
+  thesis. it.2's `NonStructuralRecursion` checker is **not** a stable
+  additive stopping point: it rejects bare non-structural recursion
+  while *grandfathering* `tail`-marked calls, i.e. it half-enforces a
+  dichotomy the language only commits to once the *destructive* it.3
+  completes. "Mechanically additive" (nothing deleted) is not the
+  same as "a coherent end-state".
+
+User decision (2026-05-16): **full revert to the pre-milestone state.**
+Both it.1 and it.2 come out. `tail-app` / structural recursion remain
+the iteration mechanism exactly as before `9973546`. The genuine
+iteration-totality ambition is *not* abandoned — it is re-sequenced
+behind a future `Nat`/refinement-types milestone, because doing it
+*properly* (enforced non-negativity) requires type machinery the
+language has not built. Stateful-islands (P2, the real descendant of
+the user's `~/sma_factory.myc` streaming analysis) is untouched: that
+analysis motivates the *streaming* milestone, not the iteration story.
+
+The revert is gate-satisfied by **subtraction**: the milestone fails
+feature-acceptance clause 3 (via A1); the revert restores the
+pre-milestone state, which already passed all three clauses. The only
+*addition* is a DESIGN.md documentation note for F1/F4 — and the
+criterion states verbatim that "a documentation note is not a
+reshape", so it introduces no bug class and asserts nothing at the
+typecheck level.
+
+## Architecture
+
+One forward iteration. The target tree state for the
+**iteration/checker/codegen/AST/surface/fixture** surface is the
+state at commit `1ff7e81` (the last commit before milestone-start
+`9973546`). The revert is **surgical, not a range revert**, because
+three hunks landed *with* the milestone but are independently sound
+and are *kept*:
+
+| Landed in | Hunk | Disposition |
+|---|---|---|
+| `9973546` | DESIGN.md feature-acceptance **clause 3** | **KEEP** — independently sound; it is the very tool that diagnosed the over-escalation. |
+| `9973546` | `skills/brainstorm/SKILL.md` Step-4 clause-3 wording | **KEEP** — part of the clause-3 strengthening (see §Components for the worked-example caveat). |
+| `9973546` | `docs/roadmap.md` Iteration-discipline milestone entry | **REVERT** — replaced by a deferred future entry. |
+| `4079f09` | `docs/roadmap.md` F3 (zero-arg `(app f)`) P2 todo | **KEEP** — independent of the iteration story; stays a P2 todo. |
+
+`git revert 9973546..a4be1e5` is therefore **forbidden twice over**:
+(1) it is a history-rewind class operation on `main`; (2) it would
+also delete clause 3 and the F3 todo. The revert is reconstructed
+forward, file by file, against the `1ff7e81` tree as the reference,
+and committed as new `main` history.
+
+## Components
+
+The exact removal / restoration / addition surface. The planner turns
+this into bite-sized tasks; the implementer executes against
+`1ff7e81` as the byte reference (`git show 1ff7e81:<path>` is the
+oracle for every *restored* file).
+
+### Remove (it.1 + it.2 production surface)
+
+- **AST (`crates/ailang-core/src/ast.rs`).** `Term::Loop { binders,
+  body }`, `Term::Recur { args }`, `struct LoopBinder`, and their
+  serde round-trip unit tests. Restore the `Term` enum and its serde
+  to the `1ff7e81` shape.
+- **Schema-drift / coverage anchors.**
+  `crates/ailang-core/tests/design_schema_drift.rs`,
+  `schema_coverage.rs`, `spec_drift.rs`,
+  `crates/ailang-core/tests/carve_out_inventory.rs`: remove the
+  `Term::Loop → "loop"` / `Term::Recur → "recur"` anchors and the
+  it.2 carve-out additions; recompute the `EXPECTED` inventory count
+  back to its `1ff7e81` value.
+- **Surface (`crates/ailang-surface`).** `parse.rs`: `parse_loop` /
+  `parse_recur`, the dispatch arms, the keyword-list entries, the
+  EBNF block. `print.rs`: the `Term::Loop` / `Term::Recur` arms.
+- **Prose (`crates/ailang-prose/src/lib.rs`).** The read + rebuild
+  arms for `Term::Loop` / `Term::Recur`.
+- **Form-A grammar (`crates/ailang-core/specs/form_a.md`).** The
+  `loop` / `recur` grammar entries.
+- **Check (`crates/ailang-check/src/lib.rs`).** `Term::Loop` typing,
+  `Term::Recur` unification, the `loop_stack` threading,
+  `verify_loop_body`; the **whole** `verify_structural_recursion`
+  pass (it.2, ~772 lines) including `term_contains_loop`, the
+  `Diverge` injection at the `FnDef`/lam-arrow/`LetRec` effect-
+  reconciliation sites, the `tail==false` grandfather and the
+  no-ADT-candidate skip. `verify_tail_positions` is restored to its
+  pure pre-it.1 `tail-app` role (it.1 repurposed it to also enforce
+  `recur`-in-tail-position; that addition is removed — the function
+  itself stays, only the it.1 arms are deleted). Walker arms for
+  `Term::Loop` / `Term::Recur` removed from `desugar.rs`, `lift.rs`,
+  `mono.rs`, `linearity.rs`, `uniqueness.rs`, `reuse_shape.rs`,
+  `pre_desugar_validation.rs`, `builtins.rs` (~25 sites, the it.1
+  blast radius in reverse).
+- **`CheckError` (`crates/ailang-check`).** Remove the five
+  variants `RecurOutsideLoop`, `RecurArityMismatch`,
+  `RecurTypeMismatch`, `RecurNotInTailPosition`,
+  `NonStructuralRecursion`, including their `code()` arms **and their
+  `ctx()` arms**. The `ctx()` removal is **not** uniform (the
+  original draft wrongly said no `ctx()` arms exist — corrected here
+  after Step-7.5 grounding): `RecurArityMismatch`,
+  `RecurTypeMismatch`, and `NonStructuralRecursion` each carry a
+  *dedicated* `ctx()` arm (`crates/ailang-check/src/lib.rs` ~870–878)
+  which must be deleted; `RecurOutsideLoop` and
+  `RecurNotInTailPosition` fall into the `_ =>` catch-all (`lib.rs`
+  ~879) and need no `ctx()` edit. The diagnostic-code registry is
+  `CheckError::code()` itself; the `//!` "Stable codes" doc-list in
+  `crates/ailang-check/src/diagnostic.rs` ends at mq.3 and never
+  gained `loop`/`recur`/`non-structural-recursion` entries (it.1
+  already proved the "add codes to a doc-list" premise false — see
+  project memory `feedback_plan_pseudo_vs_reality`), so there is
+  **nothing in `diagnostic.rs` for the revert to touch**.
+- **Codegen (`crates/ailang-codegen`).** `lib.rs`: the loop-header
+  basic-block + per-binder `phi` lowering, the `Term::Recur`
+  back-edge `br`, and the **new parallel `block_terminated` setter**
+  it.1 added — the `block_terminated` seam returns to being solely
+  tail-driven (`emit_call` / `emit_indirect_call` / `lower_effect_op`
+  on `tail: true`), exactly as at `1ff7e81`. `escape.rs`: the
+  `Term::Loop` / `Term::Recur` escape-walk arms. `lambda.rs`: the
+  `loop_frames` save/restore. `crates/ail/src/main.rs`: any it.1
+  loop wiring. `crates/ailang-core/src/workspace.rs`: it.1 additions.
+- **CLI / e2e wiring.** `crates/ail/tests/e2e.rs`,
+  `crates/ail/tests/codegen_import_map_fallback_pin.rs`,
+  `crates/ailang-check/tests/loop_recur_pin.rs`,
+  `crates/ailang-check/tests/structural_recursion_pin.rs`: the it.1
+  and it.2 pin files are **deleted** (they pin the removed surface).
+
+### DESIGN.md
+
+> **Handling rule (forestalls the obvious failure mode).** DESIGN.md
+> is edited **in place, hunk by hunk** — it is *never* wholesale-
+> restored to `git show 1ff7e81:docs/DESIGN.md`, because the
+> `1ff7e81` DESIGN.md does **not** contain clause 3 (clause 3 landed
+> *with* the milestone in `9973546` and is explicitly KEPT). Only the
+> two named hunks below are reverted, using `1ff7e81` as the
+> *per-hunk* byte oracle for those hunks only.
+
+- **Decision 3** restored to its pre-`9973546` placeholder wording
+  (`Diverge` is nominal/wired-up-only, *not* "the real effect of
+  `loop`-bearing code"). Use the Decision-3 section of
+  `git show 1ff7e81:docs/DESIGN.md` as the per-hunk byte oracle —
+  diff-and-apply that one section, do not touch the rest of the file.
+- The §"Data model" `loop` / `recur` entries removed.
+- **Decision 8** is *untouched* — it.3 never ran, so `tail-app` /
+  Decision 8 are already exactly in their pre-milestone state.
+- **Feature-acceptance criterion clause 3** is **kept** (the
+  `9973546` DESIGN.md hunk for clause 3 stays). One caveat: the
+  clause-3 *canonical worked example* added in `9973546` uses "the
+  iteration story" (structural recursion + named `loop`/`recur`
+  passing all three clauses) as its illustration. After the revert
+  there is no `loop`/`recur` in the language, so any sentence that
+  reads as "we *shipped* X" must be rephrased to "consider X" /
+  hypothetical-illustration form. The example is retained as a
+  *teaching* illustration of the criterion (it does not depend on the
+  machinery existing); it is only de-claimed from "shipped" to
+  "illustrative". This is the one prose edit inside the kept clause-3
+  block; the brainstorm SKILL.md Step-4 wording that points at it
+  needs the same de-claiming pass.
+- **Add the F1/F4 note (the only net addition).** A short, honest
+  paragraph in the DESIGN.md §"Local mutable state" / iteration
+  vicinity: the accumulator-over-an-iteration shape from the
+  mut-local motivation is *not* achievable by `mut` alone; until a
+  future iteration-totality milestone (gated behind `Nat`/refinement
+  types) lands, the canonical pattern for that shape is the
+  tail-recursive accumulator-parameter helper, and
+  `examples/mut_counter.ail` is the reference. Phrased explicitly as
+  a documented idiom, **not** an enforced rule (gate-honest per the
+  criterion's "a documentation note is not a reshape"). This
+  discharges F1 and F4 by the fieldtester's own named minimal action.
+
+### Fixtures
+
+- **Delete** (it.1 / it.2 net-new): `examples/loop_counter.ail`,
+  `examples/loop_in_lambda_e2e.ail`, `examples/loop_nested_in_lambda.ail`,
+  `examples/loop_smoke.ail`, `examples/loop_needs_diverge.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_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`,
+  `examples/test_loop_missing_diverge.ail.json`,
+  `examples/test_non_structural_recursion.ail.json`,
+  `examples/test_mutual_cross_family.ail.json`.
+  (The planner's recon re-derives the exact file set off
+  `git diff --stat 1ff7e81 HEAD -- examples/`; this list is the
+  spec's best enumeration, not a substitute for that diff.)
+- **Restore** (pre-milestone fixtures that it.2 *modified* — must be
+  reverted to content, not deleted): `examples/rc_pin_recurse_implicit.ail`,
+  `examples/rc_let_alias_implicit_param.ail`. Byte oracle:
+  `git show 1ff7e81:examples/<file>`. `examples/mut_counter.ail` /
+  `examples/mut_sum_floats.ail` were *not* migrated by it.1/it.2
+  (migration was the never-run it.3) — verify they are already at
+  their `1ff7e81` content and leave them.
+- **Delete** `bench/it3-oracle/` in its entirety (40 `.out` files +
+  `MANIFEST.tsv`) — the it.3 Task-1 deliverable, dead weight once the
+  milestone is reverted. Forward delete (the revert commit moves
+  `main` forward; nothing is rewound).
+
+### Working tree / docs hygiene
+
+- Discard the uncommitted A1 amendment to
+  `docs/specs/2026-05-15-iteration-discipline.md`
+  (`git checkout -- docs/specs/2026-05-15-iteration-discipline.md`),
+  then add a **superseded header** to that committed spec pointing to
+  this one (specs are per-milestone historical records — superseded,
+  not deleted). The it.1/it.2/it.3 plans under `docs/plans/` and the
+  it.1/it.2/it.3 journals stay as historical record (append-only
+  discipline; they record what happened).
+- **Roadmap (`docs/roadmap.md`).** Remove the Iteration-discipline
+  P1 milestone entry *and* the "blocking fork" section. Add one
+  deferred entry: `[idea]`/`[milestone]` "Iteration-totality story —
+  structural + Int-bounded total recursion with *enforced*
+  non-negativity", `depends on:` a future `Nat`/refinement-types
+  milestone, `context:` this spec + the it.3 journal (so the genuine
+  ambition and *why it was deferred* are not lost). Stateful-islands
+  and the F3 P2 todo are left exactly as they are.
+
+## Data flow
+
+After the revert the pipeline is byte-for-byte the `1ff7e81` path:
+
+`.ail` → `ailang_surface::parse` → JSON-AST (no `Term::Loop` /
+`Term::Recur` node exists) → `ailang-check`: typecheck → the
+`verify_tail_positions` pass in its pre-it.1 `tail-app`-only role →
+effect reconciliation **without** any `Diverge`-injection (no
+guardedness pass at all) → desugar / lift / mono (walkers with no
+Loop/Recur arms) → `ailang-codegen` (no loop-header path; the
+`block_terminated` seam is solely `tail: true`-driven) → LLVM text →
+`clang -O2`. There is no new back-edge class; the only iteration in
+generated IR is tail-call / structural recursion exactly as before
+the milestone.
+
+## Error handling
+
+No new diagnostics — the revert *removes* six `CheckError` variants
+(five `Recur*` + `NonStructuralRecursion`), their `code()` arms, and
+the three dedicated `ctx()` arms for `RecurArityMismatch` /
+`RecurTypeMismatch` / `NonStructuralRecursion` (the other two
+`Recur*` variants use the `ctx()` catch-all and need no edit — see
+§Components/`CheckError` for the exact split). `UndeclaredEffect`
+returns to its pre-milestone behaviour (no `Diverge` antecedent
+path). `verify_tail_positions` emits exactly the
+diagnostics it emitted at `1ff7e81` (the `tail-app` tail-position
+checks). The schema-drift / diagnostic-code surface is validated by
+the existing drift tests once they are reverted to their `1ff7e81`
+anchor set.
+
+## Testing strategy
+
+- **Revert-completeness pins (RED → GREEN for the revert).**
+  - `crates/ailang-core/tests/design_schema_drift.rs` passes with
+    **no** `loop`/`recur` anchors and **with** the `1ff7e81` anchor
+    set. This is the structural proof the AST/schema surface is fully
+    reverted.
+  - `structural_recursion_pin.rs` and `loop_recur_pin.rs` are
+    *deleted*; their absence + a green `cargo test --workspace` is
+    the proof the pinned surface is gone (no orphan references).
+  - `carve_out_inventory` `EXPECTED` equals its `1ff7e81` value.
+- **Behavioural-equivalence pins (the correctness gate).** Every
+  example fixture that existed at `1ff7e81` and still exists must
+  `ail check` and `ail run` to **byte-identical** stdout vs. its
+  `1ff7e81` behaviour — in particular the two *restored* fixtures
+  (`rc_pin_recurse_implicit.ail`, `rc_let_alias_implicit_param.ail`)
+  and the RC-regression guards they exist for. This proves the
+  revert reintroduced no behavioural drift. Drive it off a corpus
+  `ail check` / `ail run` sweep, diffing against
+  `git show 1ff7e81:` behaviour (the planner scripts the exact
+  comparison; the `bench/it3-oracle/` snapshots are *not* the oracle
+  — they are deleted; `1ff7e81` is the oracle).
+- **Doc-presence anchor.** A test (mirroring the existing DESIGN.md
+  drift-anchor mechanism) asserts the F1/F4 note is present in
+  DESIGN.md, so a future careless edit cannot silently drop the
+  documented fallback the fieldtest finding required.
+- **Full suite.** `cargo test --workspace` green. Milestone-close
+  `audit` runs the three bench regression scripts; the baseline is
+  expected **pristine** (the revert returns codegen to the
+  `1ff7e81` path — any non-pristine result is a revert defect, not a
+  ratifiable delta).
+
+## Acceptance criteria
+
+- `Term::Loop` / `Term::Recur` / `LoopBinder` / `verify_structural_
+  recursion` / `term_contains_loop` / the `Diverge`-injection / the
+  five `Recur*` + `NonStructuralRecursion` `CheckError` variants /
+  the loop codegen path / the it.1 parallel `block_terminated`
+  setter are all absent; `verify_tail_positions` is byte-equivalent
+  to its `1ff7e81` role.
+- `design_schema_drift.rs` green with the `1ff7e81` anchor set and
+  no `loop`/`recur` anchors; `structural_recursion_pin.rs` /
+  `loop_recur_pin.rs` deleted; `cargo test --workspace` green.
+- DESIGN.md Decision 3 is back to its placeholder wording; the
+  §"Data model" loop/recur entries are gone; Decision 8 is unchanged;
+  feature-acceptance **clause 3 is retained**, with its worked
+  example de-claimed from "shipped" to "illustrative" (and the
+  matching brainstorm SKILL.md wording de-claimed in lockstep).
+- The F1/F4 documentation note is present in DESIGN.md, phrased as a
+  documented idiom (not an enforced rule), naming the tail-recursive
+  accumulator-parameter fallback and `examples/mut_counter.ail`; a
+  doc-presence test guards it.
+- Every `1ff7e81`-era fixture `ail check` + `ail run` byte-identical
+  to its `1ff7e81` behaviour; `rc_pin_recurse_implicit.ail` /
+  `rc_let_alias_implicit_param.ail` restored to `1ff7e81` content;
+  `bench/it3-oracle/` deleted.
+- The uncommitted A1 spec amendment is discarded; the
+  `2026-05-15-iteration-discipline.md` spec carries a superseded
+  header pointing here; the it.1/it.2/it.3 journals and plans remain
+  as historical record.
+- `docs/roadmap.md`: the Iteration-discipline milestone entry and
+  the blocking-fork section removed; one deferred entry added for the
+  iteration-totality ambition, `depends on:` a future `Nat`/
+  refinement milestone; Stateful-islands and the F3 P2 todo
+  untouched.
+- Milestone-close `audit`: bench baseline pristine (not ratified —
+  pristine), drift review clean against the restored DESIGN.md.
+- Net effect: AILang's iteration story is exactly the pre-`9973546`
+  state (structural / tail recursion; `tail-app` intact), plus one
+  honest documentation note, plus a retained-and-de-claimed
+  feature-acceptance clause 3. The genuine total-Int-recursion
+  ambition is preserved on the roadmap, correctly sequenced behind
+  the type machinery it needs, not diluted to fit today.