design: feature-acceptance criterion clause 3 + iteration-discipline roadmap milestone

Sharpen the feature-acceptance criterion (DESIGN.md, mirrored in the
brainstorm gate) with a third conjunctive-necessary clause: a feature
reintroduces no bug class the core constraint exists to eliminate.
Criterion 1 ("an LLM reaches for it") does not discriminate — an LLM
reaches for every construct native to its imperative training
distribution, so utility alone would launder the imperative paradigm
back in one construct at a time. Clause 3 is the discriminator; a
documentation note is not a reshape (the gate is whether the wrong
code fails to typecheck).

Record the decided iteration story as a P1 milestone: structural
recursion permitted (total-by-construction under Decision 10's
acyclic-ADT invariant) + named loop/recur as the only other
repetition + tail-app retired. Discharges fieldtest finding F1 without
introducing an imperative construct; closes the residual "forgot to
mark tail" trap completely; unifies with Decision 10 (acyclic values
AND acyclic implicit call graph). Supersedes the "while-loops legal"
scope bullet of the Stateful-islands milestone, which is amended for
internal consistency. The escaping-state path (ref/MutArray/Stateful)
is unaffected and stays in Stateful-islands.

docs/DESIGN.md

@@ -70,7 +70,7 @@ is the default.
 
 ## Feature-acceptance criterion
 
-A proposed feature ships only if both hold:
+A proposed feature ships only if all three hold:
 
 1. **An LLM author naturally produces code that uses it.** Without
    prompting toward the feature, the LLM reaches for it as the clean
@@ -86,10 +86,35 @@ A proposed feature ships only if both hold:
    edits. Aesthetic appeal — "feels elegant", "is idiomatic" — does
    not count.
 
+3. **The feature reintroduces no bug class the core constraint exists
+   to eliminate.** Criterion 1 is necessary but does *not*
+   discriminate: an LLM reaches for *every* construct native to its
+   imperative training distribution, so "the LLM reaches for it" is
+   satisfied by exactly the constructs AILang most deliberately
+   refuses. A feature can pass 1 and 2 — LLMs reach for it unprompted,
+   and it removes redundancy — and still be a regression, because it
+   reinstates the error surface the pure core, local-reasoning, and
+   RC-acyclicity guarantees were built to remove. The decisive
+   question is whether the construct re-opens a class of mistakes
+   (iterated-mutable-state reasoning, silently-unbounded recursion,
+   reference cycles) that a foundational invariant closes. If it does,
+   it is cut even when 1 and 2 hold — *or* it must be reshaped until
+   the bug class is structurally impossible rather than merely
+   discouraged. A documentation note is not a reshape; the
+   discriminator is whether the wrong code fails to typecheck, not
+   whether a guideline advises against it. 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).
+
 This is the positive complement to the CLAUDE.md rule that
 implementation effort is not a rationale: cost is not a reason *for* a
-feature, and neither is human aesthetic preference. The only thing
-that is, is LLM-author utility.
+feature, and neither is human aesthetic preference. LLM-author utility
+(1, 2) is necessary; criterion 3 is the discriminator that keeps
+utility from laundering the imperative paradigm back in one construct
+at a time.
 
 Two corollaries:
 

docs/roadmap.md

@@ -40,6 +40,76 @@ clean. Pick the next milestone from P2.)_
 
 ## P1 — Next
 
+- [ ] **\[milestone\]** Iteration discipline — structural recursion +
+  named `loop`/`recur`; recursion-by-call restricted; `tail-app`
+  retired. The iteration story of the language, decided in principle
+  2026-05-15. Two constructs survive, one is removed:
+  - **Structural recursion stays — and becomes total-by-construction.**
+    A recursive call is permitted iff it is structurally guarded:
+    each recursive call is on a constructor-smaller component of an
+    algebraic argument. Decision 10 already guarantees ADTs are
+    acyclic, so a structurally-guarded recursion terminates *by the
+    invariant the language already holds* — permitting it costs
+    nothing on the provability pillar and it stays locally checkable.
+    This is the most LLM-natural correct pattern (tree / AST / JSON /
+    list `match`-and-recurse, saturated in every FP corpus) and must
+    not be amputated.
+  - **All other repetition must go through a named `(loop ...)` head +
+    `recur`.** `recur` is the single explicit backward jump; it
+    targets a lexically-enclosing named loop, never an implicit fn
+    head (Clojure permits the implicit form — AILang does not, for
+    the same no-outward-inference reason that motivated explicit
+    `tail-app`). Accumulator loops, counted iteration, streaming,
+    state machines — none are structurally decreasing, so all are
+    forced into the explicit named-loop form.
+  - **`tail-app` is retired.** `Term::App { tail: bool }` and the
+    `musttail`-lowering surface go away: a call is either structural
+    recursion (a plain call, checked total) or it is `loop`/`recur`
+    (the only loop). No marked-tail-call concept survives.
+
+  **Motivation.** Discharges fieldtest finding F1 — the most
+  consequential mut-local finding: mut-local's own motivation
+  ("removes friction from accumulators that today need tail-recursive
+  helpers") was structurally unmet, because without a loop the only
+  iteration mechanism remained the very tail-rec helper. `loop`/`recur`
+  closes that honestly without introducing an imperative construct
+  (it is pure: no mutable loop variable, no effect, composes into pure
+  contexts freely). It also closes the residual "forgot to mark tail"
+  trap *completely* — a recursive call that is not structurally
+  guarded is a compile error that names itself, not a silent
+  stack-overflow. And it unifies with Decision 10: acyclic values
+  *and* an acyclic implicit call graph; the only cycles anywhere in a
+  program are explicit, named, typed `loop` points. Both surviving
+  constructs pass all three feature-acceptance clauses including the
+  2026-05-15 clause 3 (structural recursion and named loop/recur are
+  LLM-natural *and* their bug class is closed by construction; a bare
+  `while` is exactly what clause 3 rejects).
+
+  **The open spec question (the real brainstorm work).** Not "whether"
+  but the precise definition of "structurally smaller" / the
+  guardedness check. Two hard points: (1) *mutual* structural
+  recursion (needs a measure / size over the ADT, not just a
+  one-argument syntactic decrease); (2) the accumulator-carrying
+  structural walk — `foldl`-shaped, simultaneously structural *and*
+  tail-shaped — the spec must decide whether it counts as structural
+  recursion (a plain call) or must be expressed as `loop`/`recur`.
+  This is the load-bearing spec decision; brainstorm + grounding-check
+  own it.
+
+  **Relation to Stateful islands.** This entry owns the iteration
+  story and *supersedes* the "while-loops legal" scope bullet of the
+  Stateful-islands milestone below. The genuinely-escaping
+  mutable-state path (`ref a` / `MutArray a` / `Stateful a b` /
+  `pipe`) is unaffected and stays in Stateful-islands — that is the
+  deliberately-fenced streaming escape hatch for *escaping* state,
+  not the default iteration story, and F1 no longer motivates it.
+
+  - context: 2026-05-15 chat — design convergence from the
+    mut-local fieldtest (F1) through the fenced-`while` /
+    `!Mut`-visibility dead end to the structural-recursion +
+    named-loop synthesis. Pending brainstorm produces
+    `docs/specs/<date>-iteration-discipline.md`.
+
 - [x] **\[milestone\]** Heap-`Str` ABI — runtime infrastructure for
   malloc-backed, refcounted `Str` values alongside the existing
   static `@.str_*` globals. Today the `Str` path is static-only
@@ -319,8 +389,11 @@ clean. Pick the next milestone from P2.)_
   - `!Mut` effect, the first non-IO / non-Diverge effect; forces
     the effect-handler infrastructure forward.
   - `mut` block as the syntactic boundary in Form A — outside,
-    AILang's pure self; inside, `var` / `assign` / mutable arrays /
-    while-loops legal.
+    AILang's pure self; inside, `var` / `assign` / mutable arrays
+    legal. (Iteration is *not* part of this boundary: the "Iteration
+    discipline" P1 milestone supersedes the earlier "while-loops
+    legal" scope here — repetition is structural recursion or named
+    `loop`/`recur`, never a `while` over mutable state.)
   - `var x = expr` + `assign x expr` AST nodes, legal only inside
     `mut`.
   - Mutable array primitive (`MutArray a`, O(1) index/update under