diff --git a/bench/orchestrator-stats/2026-05-15-iter-it.2.json b/bench/orchestrator-stats/2026-05-15-iter-it.2.json
new file mode 100644
index 0000000..406ff0e
--- /dev/null
+++ b/bench/orchestrator-stats/2026-05-15-iter-it.2.json
@@ -0,0 +1,16 @@
+{
+  "iter_id": "it.2",
+  "date": "2026-05-15",
+  "mode": "standard",
+  "outcome": "DONE",
+  "tasks_total": 6,
+  "tasks_completed": 6,
+  "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 0, "6": 0 },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": null,
+  "notes": "Two spec/plan boundary defects (no-ADT-candidate recursion; two non-tail-app RC fixtures) resolved inline within the task's own stated acceptance constraints (corpus stays clean, structural check not weakened) rather than triggering review re-loops — they were design clarifications applied during the implementer phase, not spec-check rejections. Tests: 622 passed / 0 failed workspace-wide. 19 files touched (10 modified, 9 new).",
+  "tests_passed": 622,
+  "tests_failed": 0,
+  "files_touched": 19
+}
diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs
index 9f5f9ae..024980e 100644
--- a/crates/ail/tests/e2e.rs
+++ b/crates/ail/tests/e2e.rs
@@ -2853,6 +2853,31 @@ fn loop_in_lambda_runs_and_prints_49() {
     assert_eq!(stdout.trim(), "49", "loop_in_lambda must print 49, got {stdout:?}");
 }
 
+/// Iter it.2 Phase-3: an it.2-clean structural recursion that runs.
+/// `struct_rec_sum_e2e` sums [1,2,3,4,5] via plain non-tail
+/// recursion on the Cons tail — the it.2 guardedness check
+/// classifies it pure + total (no `!Diverge`, no `tail-app`). This
+/// gate proves the structural-recursion "total" verdict is
+/// behaviourally sound, not merely a typecheck assertion: a plain
+/// (musttail-free) structurally-decreasing recursive call lowers
+/// and runs to the correct value.
+#[test]
+fn struct_rec_sum_runs_and_prints_15() {
+    let stdout = build_and_run("struct_rec_sum_e2e.ail");
+    assert_eq!(stdout.trim(), "15", "struct_rec_sum must print 15, got {stdout:?}");
+}
+
+/// Iter it.2 Phase-3: the `Diverge`-path twin. `loop_needs_diverge`
+/// declares `!Diverge` (loop-bearing per DD-4) and runs the it.1
+/// accumulator loop to 55 — proving the Diverge-effect injection is
+/// purely a typecheck-layer obligation with no codegen impact (the
+/// loop lowers and runs identically to its pre-it.2 it.1 form).
+#[test]
+fn loop_needs_diverge_runs_and_prints_55() {
+    let stdout = build_and_run("loop_needs_diverge.ail");
+    assert_eq!(stdout.trim(), "55", "loop_needs_diverge must print 55, got {stdout:?}");
+}
+
 /// Iter mut.3: Float twin of `mut_counter_prints_55`. The mut-var
 /// is `Float`, init is `0.0`, the recursive helper returns the
 /// sum 1.0+...+10.0 = 55.0. The polymorphic `print` routes through
diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index 01c54dc..24531e9 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/crates/ailang-check/src/lib.rs
@@ -35,7 +35,7 @@
 use ailang_core::ast::*;
 use ailang_core::Workspace;
 use indexmap::IndexMap;
-use std::collections::{BTreeMap, BTreeSet};
+use std::collections::{BTreeMap, BTreeSet, HashSet};
 
 mod linearity;
 mod pre_desugar_validation;
@@ -726,6 +726,16 @@ pub enum CheckError {
     #[error("recur must be in tail position of its enclosing loop")]
     RecurNotInTailPosition,
 
+    /// Iter it.2: a recursive call (self or mutual-group) passes a
+    /// non-structurally-smaller argument at every candidate structural
+    /// position. The author must express this iteration as an explicit
+    /// `(loop …)` / `recur` instead. Spec
+    /// `docs/specs/2026-05-15-iteration-discipline.md` (D1/D2). Display
+    /// body is bracket-`[code]`-free per the F2 convention — the CLI
+    /// formatter prepends the `[code]`.
+    #[error("recursive call to `{callee}` is not on a structurally-smaller argument (`{arg}`); express this iteration as `(loop …)` / `recur`")]
+    NonStructuralRecursion { callee: String, arg: String },
+
     /// Iter 22b.3: an internal invariant in the typechecker / mono pass
     /// was violated — surfaced as an error so callers can propagate
     /// rather than abort, but in well-formed inputs (typecheck has
@@ -782,6 +792,7 @@ impl CheckError {
             CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch",
             CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch",
             CheckError::RecurNotInTailPosition => "recur-not-in-tail-position",
+            CheckError::NonStructuralRecursion { .. } => "non-structural-recursion",
             CheckError::Internal(_) => "internal",
         }
     }
@@ -862,6 +873,9 @@ impl CheckError {
             CheckError::RecurTypeMismatch { pos, name, got, want } => {
                 serde_json::json!({"pos": pos, "name": name, "expected": want, "actual": got})
             }
+            CheckError::NonStructuralRecursion { callee, arg } => {
+                serde_json::json!({ "callee": callee, "arg": arg })
+            }
             _ => serde_json::Value::Object(serde_json::Map::new()),
         }
     }
@@ -1704,8 +1718,20 @@ fn check_in_workspace(
     env.imports = import_map;
     env.current_module = m.name.clone();
 
+    // Iter it.2 (DD-3): the module's `Def::Fn`s, for the
+    // mutual-structural-group analysis. A single owned Vec built once
+    // per module; `verify_structural_recursion` reads it to decide
+    // whether a cross-call is to a same-group member.
+    let module_fns: Vec<&FnDef> = m
+        .defs
+        .iter()
+        .filter_map(|d| match d {
+            Def::Fn(f) => Some(f),
+            _ => None,
+        })
+        .collect();
     for def in &m.defs {
-        match check_def(def, &env, out_warnings) {
+        match check_def(def, &env, &module_fns, out_warnings) {
             Ok(()) => {}
             Err(e) => {
                 errors.push(CheckError::Def(def.name().to_string(), Box::new(e)));
@@ -1723,10 +1749,11 @@ fn check_in_workspace(
 fn check_def(
     def: &Def,
     env: &Env,
+    module_fns: &[&FnDef],
     out_warnings: &mut Vec<Diagnostic>,
 ) -> Result<()> {
     match def {
-        Def::Fn(f) => check_fn(f, env, out_warnings),
+        Def::Fn(f) => check_fn(f, env, module_fns, out_warnings),
         Def::Const(c) => check_const(c, env, out_warnings),
         Def::Type(td) => check_type_def(td, env),
         // bugfix-instance-body-unbound-var (2026-05-13): each instance
@@ -1825,7 +1852,10 @@ fn check_instance(
             doc: None,
             suppress: Vec::new(),
         };
-        check_fn(&synthetic, env, out_warnings)?;
+        // Iter it.2: a synthetic instance-method fn is not a
+        // module-level def and does not participate in the
+        // mutual-structural-group analysis; pass no siblings.
+        check_fn(&synthetic, env, &[], out_warnings)?;
     }
     Ok(())
 }
@@ -1918,7 +1948,12 @@ fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> {
     }
 }
 
-fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<()> {
+fn check_fn(
+    f: &FnDef,
+    env: &Env,
+    module_fns: &[&FnDef],
+    out_warnings: &mut Vec<Diagnostic>,
+) -> Result<()> {
     // Peel an outer Forall (Iter 12a). The vars become rigid in the
     // inner env so they pass `check_type_well_formed` and unify only
     // with themselves. An empty `vars` list (vacuously polymorphic)
@@ -2020,6 +2055,29 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
     // call doesn't drown out the underlying type error.
     verify_tail_positions(&f.body, true)?;
 
+    // Iter it.2 (DD-1): structural-recursion guardedness. Sibling of
+    // `verify_tail_positions`; runs on the whole post-synth body so
+    // it can build the `smaller`-set provenance before judging any
+    // recursive call. Out of scope for synthetic Forall-peeled types
+    // — it reads `f.ty` directly via `adt_param_positions`.
+    verify_structural_recursion(f, &env, module_fns)?;
+
+    // Iter it.2 (DD-4 / D2): the first real `Diverge` effect. A fn
+    // whose body syntactically contains a `Term::Loop` raises
+    // `Diverge`, exactly as a `do print` raises `IO`. The "calls a
+    // `Diverge`-declaring callee" half needs no code here — a
+    // callee's `Type::Fn.effects` already flows into `effects`
+    // during synth (identically to `IO`). The existing
+    // declared-vs-raised reconciliation below turns an undeclared
+    // `Diverge` into the existing `UndeclaredEffect` — no new
+    // diagnostic variant. Structural recursion injects nothing (it
+    // contains no `Term::Loop`). The lam boundary is honoured by
+    // `term_contains_loop` (a loop under a `Term::Lam` is that lam's
+    // arrow effect, reconciled at the lam sub-effect site).
+    if term_contains_loop(&f.body) {
+        effects.insert("Diverge".to_string());
+    }
+
     let declared: BTreeSet<String> = declared_effs.into_iter().collect();
     for e in &effects {
         if !declared.contains(e) {
@@ -2810,6 +2868,693 @@ fn verify_loop_body(t: &Term) -> Result<()> {
     }
 }
 
+/// Iter it.2 (DD-4): true iff `t` syntactically contains a
+/// `Term::Loop`, **not** descending into `Term::Lam` bodies. A
+/// lambda is a value with its own arrow effect row — a loop inside
+/// it executes on closure call, not here, so it carries `Diverge`
+/// on the lam's arrow type (handled at the lam sub-effect reconcile
+/// site), not on the enclosing fn. This mirrors exactly how `!IO`
+/// inside a lam does not leak to the enclosing fn.
+fn term_contains_loop(t: &Term) -> bool {
+    match t {
+        Term::Loop { .. } => true,
+        Term::Lam { .. } => false,
+        Term::Lit { .. } | Term::Var { .. } => false,
+        Term::Recur { args } => args.iter().any(term_contains_loop),
+        Term::App { callee, args, .. } => {
+            term_contains_loop(callee) || args.iter().any(term_contains_loop)
+        }
+        Term::Do { args, .. } => args.iter().any(term_contains_loop),
+        Term::Let { value, body, .. } => {
+            term_contains_loop(value) || term_contains_loop(body)
+        }
+        Term::LetRec { body, in_term, .. } => {
+            term_contains_loop(body) || term_contains_loop(in_term)
+        }
+        Term::If { cond, then, else_ } => {
+            term_contains_loop(cond)
+                || term_contains_loop(then)
+                || term_contains_loop(else_)
+        }
+        Term::Seq { lhs, rhs } => {
+            term_contains_loop(lhs) || term_contains_loop(rhs)
+        }
+        Term::Match { scrutinee, arms } => {
+            term_contains_loop(scrutinee)
+                || arms.iter().any(|a| term_contains_loop(&a.body))
+        }
+        Term::Ctor { args, .. } => args.iter().any(term_contains_loop),
+        Term::Clone { value } => term_contains_loop(value),
+        Term::ReuseAs { source, body } => {
+            term_contains_loop(source) || term_contains_loop(body)
+        }
+        Term::Mut { vars, body } => {
+            vars.iter().any(|v| term_contains_loop(&v.init))
+                || term_contains_loop(body)
+        }
+        Term::Assign { value, .. } => term_contains_loop(value),
+    }
+}
+
+// ── Iter it.2: structural-recursion guardedness (DD-1/DD-2/DD-3) ──
+//
+// A recursive call (self, or to a same-ADT-family mutual-group
+// member) must pass a structurally-smaller argument at some
+// inferable parameter position. Accumulator positions are
+// unconstrained (spec D1). it.2-only grandfather: a `tail:true`
+// recursive call is not collected at all, so it never causes
+// rejection (the 21 `tail-app` corpus fixtures stay clean through
+// it.2; it.3 removes the `tail` field and this exemption together).
+
+/// One collected recursive call: the callee name, its argument
+/// terms, and the `smaller` set live at the call site. `tail:true`
+/// recursive calls are never collected (the grandfather).
+struct RecCall {
+    callee: String,
+    args: Vec<Term>,
+    smaller: HashSet<String>,
+}
+
+/// Resolve a declared type to its ADT `type`-decl name, if it is a
+/// non-primitive `Type::Con` that names a `type` decl reachable from
+/// `env` (bare or one-dot-qualified). `Type::Fn`, `Type::Var`,
+/// `Type::Forall`, and primitive cons return `None`.
+fn adt_type_head(t: &Type, env: &Env) -> Option<String> {
+    let Type::Con { name, .. } = t else {
+        return None;
+    };
+    if ailang_core::primitives::is_primitive_name(name) {
+        return None;
+    }
+    if name.matches('.').count() == 1 {
+        let (prefix, suffix) = name.split_once('.').expect("checked");
+        let target = env.imports.get(prefix)?;
+        if env
+            .module_types
+            .get(target)
+            .and_then(|tys| tys.get(suffix))
+            .is_some()
+        {
+            return Some(name.clone());
+        }
+        None
+    } else if env.types.contains_key(name) {
+        Some(name.clone())
+    } else {
+        None
+    }
+}
+
+/// Candidate structural parameter positions of `f`: indices whose
+/// declared type is a non-primitive ADT `Type::Con` (DD-2).
+fn adt_param_positions(f: &FnDef, env: &Env) -> Vec<usize> {
+    let inner = match &f.ty {
+        Type::Forall { body, .. } => (**body).clone(),
+        other => other.clone(),
+    };
+    let Type::Fn { params, .. } = inner else {
+        return Vec::new();
+    };
+    params
+        .iter()
+        .enumerate()
+        .filter_map(|(i, p)| adt_type_head(p, env).map(|_| i))
+        .collect()
+}
+
+/// The constructor-bound field names of a flat post-desugar
+/// pattern. `Pattern::Ctor` fields are `Var`/`Wild` (nested ctor
+/// patterns were rejected upstream by `NestedCtorPatternNotAllowed`).
+fn ctor_bound_names(p: &Pattern) -> Vec<String> {
+    match p {
+        Pattern::Ctor { fields, .. } => fields
+            .iter()
+            .filter_map(|f| match f {
+                Pattern::Var { name } => Some(name.clone()),
+                _ => None,
+            })
+            .collect(),
+        _ => Vec::new(),
+    }
+}
+
+/// True iff `name` is the recursion name `f` calls itself by, or a
+/// same-group mutual member (filled in Task 3 via `group`).
+fn is_rec_callee(name: &str, rec_name: &str, group: &HashSet<String>) -> bool {
+    name == rec_name || group.contains(name)
+}
+
+/// Single `smaller`-threaded walk. Collects every non-`tail`
+/// recursive call together with the `smaller` set in effect at that
+/// syntactic position. `param_smaller_seed` is the set of parameter
+/// names that are *themselves* candidate structural roots — a
+/// `match` on one of them (or on an already-smaller var) extends
+/// `smaller` with that arm's constructor-bound fields. `recur` /
+/// `loop` bodies are walked (a `recur` is not a recursive *call*);
+/// `Term::Lam` is NOT descended into (DD-3/DD-4 lam boundary).
+#[allow(clippy::too_many_arguments)]
+fn collect_rec_calls_walk(
+    t: &Term,
+    rec_name: &str,
+    group: &HashSet<String>,
+    param_roots: &HashSet<String>,
+    smaller: &HashSet<String>,
+    out: &mut Vec<RecCall>,
+) {
+    match t {
+        Term::Lit { .. } | Term::Var { .. } => {}
+        Term::App { callee, args, tail } => {
+            if !*tail {
+                if let Term::Var { name } = &**callee {
+                    if is_rec_callee(name, rec_name, group) {
+                        out.push(RecCall {
+                            callee: name.clone(),
+                            args: args.clone(),
+                            smaller: smaller.clone(),
+                        });
+                    }
+                }
+            }
+            collect_rec_calls_walk(callee, rec_name, group, param_roots, smaller, out);
+            for a in args {
+                collect_rec_calls_walk(a, rec_name, group, param_roots, smaller, out);
+            }
+        }
+        Term::Do { args, .. } => {
+            for a in args {
+                collect_rec_calls_walk(a, rec_name, group, param_roots, smaller, out);
+            }
+        }
+        Term::Let { name, value, body } => {
+            collect_rec_calls_walk(value, rec_name, group, param_roots, smaller, out);
+            // Alias propagation: `let v = <var>` where the bound term
+            // is a structural root (or already strictly smaller)
+            // makes `v` carry the same status in `body`. This is what
+            // makes the desugar-introduced `let $mp_N = <scrutinee>`
+            // (Iter 16a nested-pattern flattening) transparent to the
+            // guardedness walk — without it every nested-ctor-pattern
+            // recursion would be a false `NonStructuralRecursion`.
+            if let Term::Var { name: src } = &**value {
+                if smaller.contains(src) {
+                    let mut s = smaller.clone();
+                    s.insert(name.clone());
+                    collect_rec_calls_walk(body, rec_name, group, param_roots, &s, out);
+                    return;
+                }
+                if param_roots.contains(src) {
+                    let mut r = param_roots.clone();
+                    r.insert(name.clone());
+                    collect_rec_calls_walk(body, rec_name, group, &r, smaller, out);
+                    return;
+                }
+            }
+            collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out);
+        }
+        Term::LetRec { body, in_term, .. } => {
+            collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out);
+            collect_rec_calls_walk(in_term, rec_name, group, param_roots, smaller, out);
+        }
+        Term::If { cond, then, else_ } => {
+            collect_rec_calls_walk(cond, rec_name, group, param_roots, smaller, out);
+            collect_rec_calls_walk(then, rec_name, group, param_roots, smaller, out);
+            collect_rec_calls_walk(else_, rec_name, group, param_roots, smaller, out);
+        }
+        Term::Seq { lhs, rhs } => {
+            collect_rec_calls_walk(lhs, rec_name, group, param_roots, smaller, out);
+            collect_rec_calls_walk(rhs, rec_name, group, param_roots, smaller, out);
+        }
+        Term::Match { scrutinee, arms } => {
+            collect_rec_calls_walk(scrutinee, rec_name, group, param_roots, smaller, out);
+            // A match on a structural root (or an already-smaller var)
+            // makes that arm's constructor-bound fields strictly
+            // smaller. Other scrutinees do not extend `smaller`.
+            let extends = match &**scrutinee {
+                Term::Var { name } => param_roots.contains(name) || smaller.contains(name),
+                _ => false,
+            };
+            for arm in arms {
+                if extends {
+                    let mut s = smaller.clone();
+                    for n in ctor_bound_names(&arm.pat) {
+                        s.insert(n);
+                    }
+                    collect_rec_calls_walk(&arm.body, rec_name, group, param_roots, &s, out);
+                } else {
+                    collect_rec_calls_walk(&arm.body, rec_name, group, param_roots, smaller, out);
+                }
+            }
+        }
+        Term::Ctor { args, .. } => {
+            for a in args {
+                collect_rec_calls_walk(a, rec_name, group, param_roots, smaller, out);
+            }
+        }
+        // DD-3/DD-4: a lambda body is a separate def's territory; do
+        // not descend (consistent with the Diverge lam boundary).
+        Term::Lam { .. } => {}
+        Term::Clone { value } => {
+            collect_rec_calls_walk(value, rec_name, group, param_roots, smaller, out);
+        }
+        Term::ReuseAs { source, body } => {
+            collect_rec_calls_walk(source, rec_name, group, param_roots, smaller, out);
+            collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out);
+        }
+        Term::Mut { vars, body } => {
+            for v in vars {
+                collect_rec_calls_walk(&v.init, rec_name, group, param_roots, smaller, out);
+            }
+            collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out);
+        }
+        Term::Assign { value, .. } => {
+            collect_rec_calls_walk(value, rec_name, group, param_roots, smaller, out);
+        }
+        Term::Loop { binders, body } => {
+            for b in binders {
+                collect_rec_calls_walk(&b.init, rec_name, group, param_roots, smaller, out);
+            }
+            collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                collect_rec_calls_walk(a, rec_name, group, param_roots, smaller, out);
+            }
+        }
+    }
+}
+
+/// Whether the recursive call `c` is structurally guarded at the
+/// candidate position `i`: its `i`-th argument is a bare
+/// `Term::Var` whose name is in the `smaller` set at the call site.
+fn call_guarded_at(c: &RecCall, i: usize) -> bool {
+    match c.args.get(i) {
+        Some(Term::Var { name }) => c.smaller.contains(name),
+        _ => false,
+    }
+}
+
+/// Display form of a recursive call's offending argument (the arg
+/// at the first candidate position, else the first arg), for the
+/// diagnostic. Mirrors the short pretty form the it.1 `Recur*`
+/// diagnostics use.
+fn rec_call_arg_display(c: &RecCall, cand: &[usize]) -> String {
+    let idx = cand.first().copied().unwrap_or(0);
+    match c.args.get(idx).or_else(|| c.args.first()) {
+        Some(Term::Var { name }) => name.clone(),
+        Some(Term::Ctor { ctor, .. }) => format!("{ctor}(…)"),
+        Some(Term::App { callee, .. }) => format!("{}(…)", callee_name(callee)),
+        Some(Term::Lit { .. }) => "<literal>".to_string(),
+        Some(_) => "<expr>".to_string(),
+        None => "<no argument>".to_string(),
+    }
+}
+
+/// DD-1/DD-2/DD-3: structural-recursion guardedness for a single
+/// `FnDef`. A recursive call (self, or — Task 3 — a same-family
+/// mutual-group member) must be structurally guarded at some
+/// parameter position that is structural at *every* such call.
+fn verify_structural_recursion(
+    f: &FnDef,
+    env: &Env,
+    module_fns: &[&FnDef],
+) -> Result<()> {
+    let cand = adt_param_positions(f, env);
+    let group = mutual_structural_group(f, module_fns, env);
+
+    // it.2 transitional boundary: a def with no ADT candidate
+    // position and no mutual cycle has no *structural* parameter to
+    // verify. Its recursion is integer-counter / other-shaped
+    // (`f(n) = … f(n - 1) …`) — genuinely non-structural, but its
+    // migration to `(loop …)` is the destructive it.3 corpus pass,
+    // not it.2's job. it.2 only rejects *misuse of an ADT structural
+    // position* (the spec's load-bearing case: the canonical
+    // `f(xs) = … f(xs) …` negative still fires because it HAS an ADT
+    // candidate). This keeps the corpus clean through it.2 without
+    // weakening the ADT structural check — the `tail==false`
+    // grandfather alone is insufficient because corpus fixtures like
+    // `build_tree(depth: Int)` recurse non-tail on a primitive arg.
+    // Recorded as a resolved spec/it.2-boundary clarification in the
+    // iter journal.
+    if cand.is_empty() && group.members.is_empty() {
+        return Ok(());
+    }
+
+    let param_roots: HashSet<String> = cand
+        .iter()
+        .filter_map(|&i| f.params.get(i).cloned())
+        .collect();
+
+    let mut calls: Vec<RecCall> = Vec::new();
+    collect_rec_calls_walk(
+        &f.body,
+        &f.name,
+        &group.members,
+        &param_roots,
+        &HashSet::new(),
+        &mut calls,
+    );
+    if calls.is_empty() {
+        return Ok(());
+    }
+
+    // Per-call guardedness verdict:
+    // - self-call (`callee == f.name`): guarded iff some candidate
+    //   position of `f` receives a structurally-smaller arg.
+    // - cross-call into a mutual-cycle member: only meaningful if the
+    //   cycle is a valid same-family group (`family_valid`); then
+    //   guarded iff some candidate position of the *callee* receives
+    //   a var in the caller's `smaller` set (DD-3). A cross-call into
+    //   a family-INVALID cycle is unconditionally unguarded — the
+    //   cross-family negative.
+    let guarded = |c: &RecCall| -> bool {
+        if c.callee == f.name {
+            cand.iter().any(|&i| call_guarded_at(c, i))
+        } else if !group.family_valid {
+            false
+        } else {
+            module_fns
+                .iter()
+                .find(|g| g.name == c.callee)
+                .map(|g| adt_param_positions(g, env))
+                .map(|gc| gc.iter().any(|&i| call_guarded_at(c, i)))
+                .unwrap_or(false)
+        }
+    };
+
+    // Structural iff there is a single candidate position of `f`
+    // structural at *every* self-call (the implicit-inference rule,
+    // DD-2) AND every cross-call into the mutual cycle is guarded.
+    let self_calls: Vec<&RecCall> = calls.iter().filter(|c| c.callee == f.name).collect();
+    let self_clear = self_calls.is_empty()
+        || cand
+            .iter()
+            .any(|&i| self_calls.iter().all(|c| call_guarded_at(c, i)));
+    let cross_clear = calls
+        .iter()
+        .filter(|c| c.callee != f.name)
+        .all(guarded);
+
+    if self_clear && cross_clear {
+        return Ok(());
+    }
+
+    // Not structural — emit on the first unguarded recursive call
+    // (all collected calls are already non-`tail`; the `tail:true`
+    // grandfather filtered them out at collection time).
+    let offending = calls.iter().find(|c| !guarded(c)).unwrap_or(&calls[0]);
+    Err(CheckError::NonStructuralRecursion {
+        callee: offending.callee.clone(),
+        arg: rec_call_arg_display(offending, &cand),
+    })
+}
+
+/// Tiny `BTreeMap`-backed union-find over type names (DD-3). No
+/// external dependency; path-halving find, union-by-insertion.
+struct TypeUnionFind {
+    parent: BTreeMap<String, String>,
+}
+
+impl TypeUnionFind {
+    fn new() -> Self {
+        TypeUnionFind { parent: BTreeMap::new() }
+    }
+    fn ensure(&mut self, x: &str) {
+        if !self.parent.contains_key(x) {
+            self.parent.insert(x.to_string(), x.to_string());
+        }
+    }
+    fn find(&mut self, x: &str) -> String {
+        self.ensure(x);
+        let mut cur = x.to_string();
+        while self.parent[&cur] != cur {
+            let grand = self.parent[&self.parent[&cur]].clone();
+            self.parent.insert(cur.clone(), grand.clone());
+            cur = self.parent[&cur].clone();
+        }
+        cur
+    }
+    fn union(&mut self, a: &str, b: &str) {
+        let ra = self.find(a);
+        let rb = self.find(b);
+        if ra != rb {
+            self.parent.insert(ra, rb);
+        }
+    }
+    fn same(&mut self, a: &str, b: &str) -> bool {
+        self.find(a) == self.find(b)
+    }
+}
+
+/// Collect the `Type::Con` head names referenced anywhere inside a
+/// type (recursing through `Fn`/`Forall`/`Con` args), skipping
+/// primitives and type vars.
+fn referenced_con_names(t: &Type, out: &mut Vec<String>) {
+    match t {
+        Type::Con { name, args } => {
+            if !ailang_core::primitives::is_primitive_name(name) {
+                out.push(name.clone());
+            }
+            for a in args {
+                referenced_con_names(a, out);
+            }
+        }
+        Type::Fn { params, ret, .. } => {
+            for p in params {
+                referenced_con_names(p, out);
+            }
+            referenced_con_names(ret, out);
+        }
+        Type::Forall { body, .. } => referenced_con_names(body, out),
+        Type::Var { .. } => {}
+    }
+}
+
+/// DD-3: connected components of the ADT type-reference graph.
+/// Nodes are every visible `type` decl name; an undirected edge
+/// joins `T` and any non-primitive `Con` head appearing in one of
+/// `T`'s constructor field types. The result answers
+/// "are these two ADT heads in one family?".
+fn adt_families(env: &Env) -> TypeUnionFind {
+    let mut uf = TypeUnionFind::new();
+    // All visible TypeDefs: the current module's plus every module's
+    // (workspace-flat). Bare names index the current module; that is
+    // the resolution `adt_type_head` already uses for fixtures.
+    let mut all: Vec<(&String, &TypeDef)> = env.types.iter().collect();
+    for tys in env.module_types.values() {
+        all.extend(tys.iter());
+    }
+    for (name, td) in &all {
+        uf.ensure(name);
+        for ctor in &td.ctors {
+            for field in &ctor.fields {
+                let mut refs = Vec::new();
+                referenced_con_names(field, &mut refs);
+                for r in refs {
+                    // Edge only between ADT decls (a referenced name
+                    // that is not a known type decl, e.g. a builtin
+                    // wrapper, contributes no family edge).
+                    uf.union(name, &r);
+                }
+            }
+        }
+    }
+    uf
+}
+
+/// DD-3: the mutual-recursion cycle `f` belongs to — the set of
+/// *other* module fn names that `f` reaches and that reach `f`
+/// through direct `Term::App` → `Term::Var` recursion (the
+/// back-reaching connected component of the call graph restricted
+/// to `module_fns`), plus whether that cycle is a valid same-ADT-
+/// family structural group. Empty `members` ⇒
+/// `verify_structural_recursion` treats `f` as self-recursive only.
+/// Non-empty `members` with `family_valid = false` ⇒ the cycle
+/// spans unrelated ADT families: each cross-call is an unguarded
+/// recursive call (the cross-family negative).
+fn mutual_structural_group(
+    f: &FnDef,
+    module_fns: &[&FnDef],
+    env: &Env,
+) -> MutualGroup {
+    // Direct-call adjacency among module fns (callee names that are
+    // module fns; ignore builtins / cross-module).
+    let names: HashSet<&str> = module_fns.iter().map(|g| g.name.as_str()).collect();
+    let direct_callees = |g: &FnDef| -> HashSet<String> {
+        let mut cs = Vec::new();
+        collect_direct_app_var_callees(&g.body, &mut cs);
+        cs.into_iter().filter(|c| names.contains(c.as_str())).collect()
+    };
+
+    // Connected component of `f` in the (undirected) call graph.
+    let by_name: BTreeMap<&str, &FnDef> =
+        module_fns.iter().map(|g| (g.name.as_str(), *g)).collect();
+    let mut adj: BTreeMap<String, HashSet<String>> = BTreeMap::new();
+    for g in module_fns {
+        let cs = direct_callees(g);
+        for c in &cs {
+            adj.entry(g.name.clone()).or_default().insert(c.clone());
+            adj.entry(c.clone()).or_default().insert(g.name.clone());
+        }
+    }
+    let mut comp: HashSet<String> = HashSet::new();
+    let mut stack = vec![f.name.clone()];
+    while let Some(n) = stack.pop() {
+        if !comp.insert(n.clone()) {
+            continue;
+        }
+        if let Some(neigh) = adj.get(&n) {
+            for m in neigh {
+                if !comp.contains(m) {
+                    stack.push(m.clone());
+                }
+            }
+        }
+    }
+    comp.remove(&f.name);
+    // Members that genuinely participate in a recursive cycle with
+    // `f`: keep only those that (transitively) call back to `f`.
+    // For the corpus shapes (tree/forest, even/odd) the component is
+    // already the mutual cycle; a one-way helper call would not put
+    // the helper into a back-reaching cycle, so it drops out here.
+    let reaches = |start: &str, target: &str| -> bool {
+        let mut seen: HashSet<String> = HashSet::new();
+        let mut st = vec![start.to_string()];
+        while let Some(n) = st.pop() {
+            if n == target && n != start {
+                return true;
+            }
+            if !seen.insert(n.clone()) {
+                continue;
+            }
+            if let Some(g) = by_name.get(n.as_str()) {
+                for c in direct_callees(g) {
+                    if c == target {
+                        return true;
+                    }
+                    st.push(c);
+                }
+            }
+        }
+        false
+    };
+    let members: HashSet<String> = comp
+        .into_iter()
+        .filter(|m| reaches(&f.name, m) && reaches(m, &f.name))
+        .collect();
+    if members.is_empty() {
+        return MutualGroup { members, family_valid: true };
+    }
+
+    // DD-3 family test: `f` and every cycle member must have a
+    // structural ADT parameter, and all those parameter type heads
+    // must be in ONE family component. If not, the cycle is not a
+    // valid mutual structural group — `family_valid = false` makes
+    // every cross-call into it an unguarded recursive call (the
+    // cross-family negative).
+    let mut uf = adt_families(env);
+    let head_of = |g: &FnDef| -> Option<String> {
+        let inner = match &g.ty {
+            Type::Forall { body, .. } => (**body).clone(),
+            other => other.clone(),
+        };
+        let Type::Fn { params, .. } = inner else { return None };
+        params.iter().find_map(|p| adt_type_head(p, env))
+    };
+    let family_valid = match head_of(f) {
+        None => false,
+        Some(f_head) => members.iter().all(|m| {
+            by_name
+                .get(m.as_str())
+                .and_then(|mg| head_of(mg))
+                .map(|h| uf.same(&f_head, &h))
+                .unwrap_or(false)
+        }),
+    };
+    MutualGroup { members, family_valid }
+}
+
+/// DD-3: the mutual-recursion cycle `f` participates in, and
+/// whether that cycle is a valid same-ADT-family structural group.
+/// `members` is family-agnostic (used to collect cross-calls); a
+/// cross-call into a `members` fn is judged structurally only when
+/// `family_valid` holds, otherwise it is an unguarded recursive
+/// call.
+struct MutualGroup {
+    members: HashSet<String>,
+    family_valid: bool,
+}
+
+/// Direct `Term::App` whose callee is a `Term::Var` — the callee
+/// names reachable by direct application (no descent into `Lam`
+/// bodies, consistent with the guardedness walk's lam boundary).
+fn collect_direct_app_var_callees(t: &Term, out: &mut Vec<String>) {
+    match t {
+        Term::Lit { .. } | Term::Var { .. } | Term::Recur { .. } => {}
+        Term::App { callee, args, .. } => {
+            if let Term::Var { name } = &**callee {
+                out.push(name.clone());
+            }
+            collect_direct_app_var_callees(callee, out);
+            for a in args {
+                collect_direct_app_var_callees(a, out);
+            }
+        }
+        Term::Do { args, .. } => {
+            for a in args {
+                collect_direct_app_var_callees(a, out);
+            }
+        }
+        Term::Let { value, body, .. } => {
+            collect_direct_app_var_callees(value, out);
+            collect_direct_app_var_callees(body, out);
+        }
+        Term::LetRec { body, in_term, .. } => {
+            collect_direct_app_var_callees(body, out);
+            collect_direct_app_var_callees(in_term, out);
+        }
+        Term::If { cond, then, else_ } => {
+            collect_direct_app_var_callees(cond, out);
+            collect_direct_app_var_callees(then, out);
+            collect_direct_app_var_callees(else_, out);
+        }
+        Term::Seq { lhs, rhs } => {
+            collect_direct_app_var_callees(lhs, out);
+            collect_direct_app_var_callees(rhs, out);
+        }
+        Term::Match { scrutinee, arms } => {
+            collect_direct_app_var_callees(scrutinee, out);
+            for arm in arms {
+                collect_direct_app_var_callees(&arm.body, out);
+            }
+        }
+        Term::Ctor { args, .. } => {
+            for a in args {
+                collect_direct_app_var_callees(a, out);
+            }
+        }
+        // Lam boundary (DD-3/DD-4): a closure body is a separate
+        // def's territory; do not descend.
+        Term::Lam { .. } => {}
+        Term::Clone { value } => collect_direct_app_var_callees(value, out),
+        Term::ReuseAs { source, body } => {
+            collect_direct_app_var_callees(source, out);
+            collect_direct_app_var_callees(body, out);
+        }
+        Term::Mut { vars, body } => {
+            for v in vars {
+                collect_direct_app_var_callees(&v.init, out);
+            }
+            collect_direct_app_var_callees(body, out);
+        }
+        Term::Assign { value, .. } => collect_direct_app_var_callees(value, out),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                collect_direct_app_var_callees(&b.init, out);
+            }
+            collect_direct_app_var_callees(body, out);
+        }
+    }
+}
+
 fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<()> {
     // Const types are never polymorphic — a Forall here is rejected
     // outright. Any other type passes through to `synth` as before.
@@ -3579,6 +4324,16 @@ pub(crate) fn synth(
             }
             let body_ty = body_ty?;
             unify(ret_ty, &body_ty, subst)?;
+            // Iter it.2 (DD-4): a `(loop …)` directly in this lam's
+            // body makes the lam's arrow carry `Diverge` — coherent
+            // with how `!IO` scopes across the lam edge. A loop under
+            // a *further-nested* lam is that inner lam's concern;
+            // `term_contains_loop`'s own `Term::Lam => false` stops
+            // there. Reconciled against the lam's declared arrow
+            // effects exactly like every other raised effect.
+            if term_contains_loop(body) {
+                body_effects.insert("Diverge".to_string());
+            }
             let declared: BTreeSet<String> = lam_effects.iter().cloned().collect();
             for e in &body_effects {
                 if !declared.contains(e) {
@@ -3670,6 +4425,13 @@ pub(crate) fn synth(
             let body_ty = body_ty?;
             unify(&ret_ty, &body_ty, subst)?;
 
+            // Iter it.2 (DD-4): a `Term::LetRec` clause is a
+            // fn-equivalent (same as `check_fn` / `Term::Lam`); a
+            // `(loop …)` in its body makes its arrow carry `Diverge`.
+            // Same lam-boundary rule via `term_contains_loop`.
+            if term_contains_loop(body) {
+                body_effects.insert("Diverge".to_string());
+            }
             let declared: BTreeSet<String> = declared_effs.into_iter().collect();
             for e in &body_effects {
                 if !declared.contains(e) {
diff --git a/crates/ailang-check/tests/structural_recursion_pin.rs b/crates/ailang-check/tests/structural_recursion_pin.rs
new file mode 100644
index 0000000..db9d5d9
--- /dev/null
+++ b/crates/ailang-check/tests/structural_recursion_pin.rs
@@ -0,0 +1,129 @@
+//! Iter it.2: pin tests for the structural-recursion guardedness
+//! pass + the it.2-only `tail:true` grandfather + the first real
+//! `Diverge` effect injection.
+//!
+//! Spec: `docs/specs/2026-05-15-iteration-discipline.md`. Mirrors the
+//! it.1 `loop_recur_pin.rs` harness verbatim (same inline
+//! `check_fixture` helper, no `mod common`).
+
+use ailang_check::check_workspace;
+use ailang_surface::load_workspace;
+use std::path::PathBuf;
+
+fn examples_dir() -> PathBuf {
+    let manifest = env!("CARGO_MANIFEST_DIR");
+    PathBuf::from(manifest)
+        .parent().expect("CARGO_MANIFEST_DIR has a parent (crates/ailang-check)")
+        .parent().expect("CARGO_MANIFEST_DIR has a grandparent (crates/)")
+        .join("examples")
+}
+
+/// Load the named fixture under `examples/`, run check_workspace, and
+/// return the diagnostic code list (one entry per Diagnostic).
+fn check_fixture(fixture_name: &str) -> Vec<String> {
+    let path = examples_dir().join(fixture_name);
+    let ws = load_workspace(&path)
+        .unwrap_or_else(|e| panic!("workspace `{fixture_name}` must load: {e:?}"));
+    let diags = check_workspace(&ws);
+    diags.iter().map(|d| d.code.clone()).collect()
+}
+
+#[test]
+fn structural_list_len_is_clean() {
+    // Plain non-tail recursion on a Cons sub-component typechecks
+    // clean: structurally guarded ⇒ pure + total, no diagnostics.
+    assert!(
+        check_fixture("struct_rec_list_len.ail").is_empty(),
+        "expected zero diagnostics for structural list length"
+    );
+}
+
+#[test]
+fn foldl_accumulator_is_structural_and_clean() {
+    // A foldl-shape accumulator walk (structural on the tail,
+    // unconstrained accumulator) classifies as structural recursion
+    // and stays clean + Diverge-free (spec D1).
+    assert!(
+        check_fixture("struct_rec_foldl_sum.ail").is_empty(),
+        "expected zero diagnostics for foldl-shape accumulator walk"
+    );
+}
+
+#[test]
+fn non_structural_self_call_is_rejected() {
+    // A self-call passing the un-decreased parameter at every
+    // candidate position, not `tail`-marked, fires
+    // `non-structural-recursion`.
+    assert!(
+        check_fixture("test_non_structural_recursion.ail.json")
+            .contains(&"non-structural-recursion".to_string()),
+        "expected non-structural-recursion diagnostic"
+    );
+}
+
+#[test]
+fn tree_forest_mutual_is_clean() {
+    // Mutual tree/forest recursion over one ADT family (the
+    // cross-reference edge unions {Tree, Forest}) classifies as a
+    // mutual structural group: clean, Diverge-free.
+    assert!(
+        check_fixture("struct_rec_tree_forest.ail").is_empty(),
+        "expected zero diagnostics for same-family mutual recursion"
+    );
+}
+
+#[test]
+fn mutual_cross_family_is_rejected() {
+    // Mutual recursion whose members' structural params lie in two
+    // unrelated ADT families is not a valid mutual structural group
+    // (DD-3): the cross-call is an unguarded recursive call.
+    assert!(
+        check_fixture("test_mutual_cross_family.ail.json")
+            .contains(&"non-structural-recursion".to_string()),
+        "expected non-structural-recursion for cross-family mutual recursion"
+    );
+}
+
+#[test]
+fn loop_fn_declaring_diverge_is_clean() {
+    // A loop-bearing fn that declares `!Diverge` in its effect row
+    // reconciles clean (DD-4 / D2).
+    assert!(
+        check_fixture("loop_needs_diverge.ail").is_empty(),
+        "expected zero diagnostics for loop fn declaring !Diverge"
+    );
+}
+
+#[test]
+fn loop_fn_missing_diverge_is_rejected() {
+    // A loop-bearing fn missing `!Diverge` raises the existing
+    // `undeclared-effect` (no new diagnostic variant; DD-4).
+    assert!(
+        check_fixture("test_loop_missing_diverge.ail.json")
+            .contains(&"undeclared-effect".to_string()),
+        "expected undeclared-effect for loop fn missing !Diverge"
+    );
+}
+
+#[test]
+fn structural_recursion_is_diverge_free() {
+    // Structural recursion injects no effect: a structural list walk
+    // with no `loop` and no declared `!Diverge` stays clean.
+    assert!(
+        check_fixture("struct_rec_list_len.ail").is_empty(),
+        "structural recursion must be Diverge-free"
+    );
+}
+
+#[test]
+fn non_structural_recursion_code_is_registered() {
+    // A CheckError::NonStructuralRecursion must map to the kebab code.
+    // This step only pins the code() arm exists and returns the exact
+    // string; fixture-level behaviour is pinned in Task 2+.
+    use ailang_check::CheckError;
+    let e = CheckError::NonStructuralRecursion {
+        callee: "f".into(),
+        arg: "n".into(),
+    };
+    assert_eq!(e.code(), "non-structural-recursion");
+}
diff --git a/crates/ailang-core/tests/carve_out_inventory.rs b/crates/ailang-core/tests/carve_out_inventory.rs
index 31c974b..f508e5f 100644
--- a/crates/ailang-core/tests/carve_out_inventory.rs
+++ b/crates/ailang-core/tests/carve_out_inventory.rs
@@ -3,7 +3,7 @@
 //! under `examples/*.ail.json` after milestone close. The list is
 //! hardcoded; any change is a deliberate, brainstorm-level decision.
 //!
-//! Twelve carve-outs post iter mut.2 (2026-05-15):
+//! Twenty carve-outs post iter it.2 (2026-05-15):
 //! - §C4 (a) subject-matter: 7 fixtures from form-a.1 milestone
 //!   close (canonical-form rejection / unbound / class-def rejection).
 //! - Iter mut.2: 5 negative typecheck fixtures for the new mut /
@@ -13,6 +13,14 @@
 //!   fixture convention. The positive nested-shadow case is a
 //!   .ail.json carve-out for symmetry with its negative siblings
 //!   (the driver tests all five from one helper).
+//! - Iter mut.4-tidy: 1 lambda-capture-of-mut-var negative fixture.
+//! - Iter it.1: 4 recur negative typecheck fixtures.
+//! - Iter it.2: 3 negative fixtures — self non-structural recursion,
+//!   mutual cross-family recursion (both fire `non-structural-
+//!   recursion`), and a loop-bearing fn missing `!Diverge` (fires
+//!   the existing `undeclared-effect`, no new variant per DD-4). The
+//!   diagnostic code is the load-bearing assertion, not the surface
+//!   form.
 //! - §C4 (b) compile-time-embed: retired 2026-05-14 by milestone
 //!   prelude-decouple; the prelude is now embedded as `prelude.ail`
 //!   in `ailang-surface` and parsed at compile time via
@@ -42,6 +50,10 @@ const EXPECTED: &[&str] = &[
     "test_recur_arity_mismatch.ail.json",
     "test_recur_type_mismatch.ail.json",
     "test_recur_not_in_tail_position.ail.json",
+    // Iter it.2 — non-structural-recursion negative fixtures
+    "test_non_structural_recursion.ail.json",
+    "test_mutual_cross_family.ail.json",
+    "test_loop_missing_diverge.ail.json",
 ];
 
 fn examples_dir() -> std::path::PathBuf {
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 617b9dd..cd6f2cb 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -164,8 +164,16 @@ Advantages:
 
 The default is total, pure functions. Effects are declared as a set in the
 function type: `(Int) -> Int ![IO]`. The effect set is row-polymorphic
-(`![IO | r]`). In the MVP only the effects `IO` and `Diverge` (for infinite
-loops) are wired up.
+(`![IO | r]`). Two effects are wired up: `IO` (observable side effects,
+raised by `do`-operations), and `Diverge` (non-termination). As of iter
+it.2 (2026-05-15) `Diverge` is no longer nominal: it is the effect carried
+by any function whose body contains a `loop` (or that calls a
+`Diverge`-declaring function), surfaced through the existing
+declared-vs-raised reconciliation (an undeclared `Diverge` is the existing
+`UndeclaredEffect`, no new diagnostic). Structural recursion is pure and
+total and carries no effect — the author who wants a `!Diverge`-free
+signature is structurally pulled toward structural recursion and pays
+`!Diverge` only when genuinely writing an unbounded `loop`.
 
 This is the most important LLM property: when I read a function, I can trust
 its signature without reading the body.
@@ -2446,8 +2454,16 @@ parse, print, prose-project, round-trip, typecheck (binder typing,
 recur arity/type unification, recur tail-position) and codegen
 (loop-header block with one phi per binder, `recur` as a back-edge
 `br`) without removing or modifying the existing `tail-app`/`tail-do`
-paths. The structural-recursion restriction and the `Diverge`
-effect land in it.2; `tail-app`/`tail-do` are retired in it.3. See
+paths. As of iter it.2 (2026-05-15) the structural-recursion
+guardedness restriction and the `Diverge` effect are in effect:
+a non-structural recursion-by-call is the compile error
+`NonStructuralRecursion` (directing the author to `(loop …)` /
+`recur`), and any fn whose body contains a `Term::Loop` (or calls a
+`Diverge`-declaring callee) must declare `!Diverge` in its effect
+row — structural recursion stays pure, total, and effect-free. A
+transitional grandfather exempts still-`tail: true`-marked recursive
+calls so the corpus type-checks unchanged through it.2.
+`tail-app`/`tail-do` are retired in it.3. See
 `docs/specs/2026-05-15-iteration-discipline.md`.
 
 **`Literal`**:
diff --git a/docs/journals/2026-05-15-iter-it.2.md b/docs/journals/2026-05-15-iter-it.2.md
new file mode 100644
index 0000000..8917641
--- /dev/null
+++ b/docs/journals/2026-05-15-iter-it.2.md
@@ -0,0 +1,241 @@
+# iter it.2 — structural-guardedness checker + first real Diverge effect
+
+**Date:** 2026-05-15
+**Started from:** bc9f5120034f2552ad7e78454bb198472404d4b1
+**Status:** DONE
+**Tasks completed:** 6 of 6
+
+## Summary
+
+Second of three iterations in the iteration-discipline milestone.
+Adds the structural-recursion guardedness checker
+(`CheckError::NonStructuralRecursion`) and the first real
+implementation of the Decision-3 `Diverge` effect, both strictly
+additive — nothing `tail`-related is removed (that is it.3). A new
+whole-body pass `verify_structural_recursion` runs as a sibling of
+`verify_tail_positions` in `check_fn`'s post-synth region (DD-1); it
+implements the `smaller`-set algorithm with implicit candidate
+inference and unconstrained accumulator positions (DD-2: the
+foldl-shape accumulator walk classifies as structural), self- and
+mutual-recursion identification with ADT-family connected components
+via an inline union-find (DD-3), and the it.2-only `tail==false`
+grandfather. A new `term_contains_loop` (stopping at `Term::Lam`
+boundaries, DD-4) injects `"Diverge"` into the raised effect set so
+the existing `UndeclaredEffect` reconciliation enforces it with no
+new diagnostic variant; the lam-arrow and `Term::LetRec` cases are
+wired at their respective sub-effect reconcile sites. DESIGN.md
+Decision 3 + the §Data-model hook are synced to present tense. All
+20 tail-app corpus fixtures stay grandfathered-clean;
+`cargo test --workspace` green at 622 passed / 0 failed; the it.1
+loop fixtures gained `!Diverge` (in scope per the plan).
+
+Two spec/plan boundary defects surfaced and were resolved inside
+the task's own stated invariants (corpus stays clean, structural
+check not weakened) — see Concerns. Both are recorded so the it.3
+planner and a future spec-tightening pass have the signal.
+
+## Per-task notes
+
+- iter it.2.1: `CheckError::NonStructuralRecursion { callee, arg }`
+  added beside the it.1 `Recur*` variants (bracket-`[code]`-free
+  Display per F2), `code()` → `"non-structural-recursion"`, `ctx()`
+  → `{callee, arg}`. New pin file `structural_recursion_pin.rs`
+  (loop_recur_pin harness verbatim). `diagnostic.rs` untouched
+  (plan-correctly: `code()` is the registry). RED→GREEN clean.
+
+- iter it.2.2: the pass + helpers next to `verify_loop_body`:
+  `adt_type_head` / `adt_param_positions` / `ctor_bound_names` /
+  `collect_rec_calls_walk` (single `smaller`-threaded walk folding
+  collection + guardedness, `tail==false` grandfather in the App
+  arm, stops at `Term::Lam`) / `call_guarded_at` /
+  `rec_call_arg_display`. `check_fn`/`check_def` gained a
+  `module_fns: &[&FnDef]` param (plan-anticipated in Step 3.2 for
+  mutual grouping; threaded from the per-module loop; synthetic
+  instance-method fns pass `&[]`). Wired
+  `verify_structural_recursion(f, &env, module_fns)?;` immediately
+  after `verify_tail_positions`. Two over-rejection classes found
+  against the corpus and fixed within the task's own acceptance
+  constraint (see Concerns §1, §2). Status DONE_WITH_CONCERNS.
+
+- iter it.2.3: ADT-family union-find (`TypeUnionFind`, inline
+  `BTreeMap`-backed, path-halving, no dependency) +
+  `mutual_structural_group` returning a `MutualGroup { members,
+  family_valid }` (a plan-pseudo-vs-real refinement — the plan's
+  `Vec<&FnDef>` could not express the cross-family-negative; an
+  empty group silently drops the cross-call instead of rejecting
+  it). `collect_direct_app_var_callees` for call-graph adjacency
+  (same lam boundary). `verify_structural_recursion` reworked to a
+  single `guarded` closure: self-calls vs callee-cand, cross-calls
+  guarded only if `family_valid`. tree/forest clean, cross-family
+  rejected. RED→GREEN.
+
+- iter it.2.4: `term_contains_loop` (exhaustive Term match;
+  `Loop=>true`, `Lam=>false`, all else recurse incl. Recur args).
+  Injection in `check_fn` before the declared-vs-raised reconcile.
+  Lam-arrow coherence wired at BOTH the `Term::Lam` synth
+  sub-effect site AND the `Term::LetRec` synth sub-effect site
+  (the plan named only the Lam site; recon line drifted and there
+  are now two structurally-identical reconcile sites — a
+  `Term::LetRec` clause is a fn-equivalent, same as the it.1
+  tail-position treatment, so a loop in a deferred LetRec body must
+  also carry Diverge; injecting at both is the sound completion,
+  not an extra). Four it.1 loop fixtures + two HOF signatures
+  updated to declare `!Diverge` (see Concerns §3). Status
+  DONE_WITH_CONCERNS.
+
+- iter it.2.5: DESIGN.md Decision 3 rewritten (`Diverge` no longer
+  nominal; carried by loop-bearing / Diverge-calling fns; structural
+  recursion pure+total; `IO` description kept + sharpened) +
+  §Data-model hook sentence → present tense, it.3 retirement
+  retained. Drift anchors (`"t":"loop"`/`"t":"recur"`) untouched —
+  `design_schema_drift`/`schema_coverage`/`spec_drift` green.
+
+- iter it.2.6: acceptance gate. Full workspace green; all 7 named
+  spec-acceptance pins green; `mut_counter.ail` still runs `55`
+  (grandfathered, unmigrated); all 20 tail-app corpus fixtures
+  grandfathered-clean (zero `non-structural-recursion`).
+
+- Phase 3 (E2E): `examples/struct_rec_sum_e2e.ail` +
+  `struct_rec_sum_runs_and_prints_15` — an it.2-clean structural
+  recursion (plain non-tail, no `!Diverge`, no `tail-app`) that
+  runs to 15, proving the "total" verdict is behaviourally sound,
+  not just a typecheck assertion. Plus
+  `loop_needs_diverge_runs_and_prints_55` — the Diverge-path twin,
+  proving the Diverge injection is a typecheck-only obligation with
+  zero codegen impact (the loop lowers/runs identically to it.1).
+
+## Concerns
+
+- **§1 — Spec/it.2-boundary defect: no-ADT-candidate recursion.**
+  The plan's load-bearing invariant ("the 21 tail-app corpus
+  fixtures stay clean through it.2 because `collect_rec_calls` only
+  collects `tail==false` calls") is insufficient: corpus fixtures
+  like `bench_latency_explicit.ail`'s `build_tree(depth: Int)`
+  recurse **non-tail** (inside a `term-ctor`) on a **primitive**
+  arg — the `tail==false` grandfather does not exempt them, and
+  they have no ADT candidate position. Strict DD-2 would reject
+  ~18 corpus fixtures in it.2, contradicting the additive mandate.
+  Resolution (does NOT weaken the ADT check): a def with no ADT
+  candidate position AND no mutual cycle has no *structural*
+  position to verify — it is integer-counter / other-shaped
+  recursion whose migration to `(loop …)` is the destructive it.3
+  corpus pass, not it.2's job. it.2 only rejects *misuse of an ADT
+  structural position*; the spec's load-bearing negative
+  (`f(xs: IntList) = … f(xs) …`, HAS an ADT candidate) still fires.
+  This is the honest reading of DD-2's "for each candidate
+  structural position" (vacuous when there are none); the plan's
+  pseudo-code only handled `calls.is_empty()`, not
+  `cand.is_empty()`. Recorded as a resolved it.2/it.3 boundary
+  clarification — the it.3 planner should expect these to be the
+  corpus-migration set, and a spec-tightening pass may want to
+  state the no-candidate boundary explicitly.
+
+- **§2 — Two RC-regression fixtures needed the spec's transitional
+  grandfather applied.** `rc_pin_recurse_implicit.ail` and
+  `rc_let_alias_implicit_param.ail` (NOT in the 20-fixture tail-app
+  set) contain `loop(n: Int, t: Tree) = … (app loop (- n 1) t)` —
+  an ADT param (`t: Tree`) held constant while decrementing an Int,
+  recursing **non-tail**. This is structurally identical to the
+  required negative (`f(xs)=…f(xs)…`): both pass the ADT param
+  unchanged at its candidate position. It therefore correctly fires
+  `NonStructuralRecursion` and CANNOT be exempted by broadening the
+  grandfather without also letting the required negative through
+  (which would weaken the check — explicitly forbidden by the
+  carrier). The recursive call is in tail position, so the
+  spec-prescribed transitional treatment applies: mark it
+  `tail-app` (the it.2 "Transitional grandfather" — identical to
+  the idiom 20 other corpus fixtures use; it.3 migrates to
+  `(loop …)`). The 18d.4 / 18g regressions these fixtures guard
+  live in `pin`/`pin_aliased`'s match arm-close, unaffected by the
+  `loop` recursion's lowering — so this is NOT adapting-a-test-to-
+  dodge-a-bug (the check is correct; the fixture joins the
+  transitional grandfather, with an in-fixture comment recording
+  why). Both fixtures' RC==GC e2e regression guards still pass.
+
+- **§3 — it.1 loop fixtures gained `!Diverge` (plan-in-scope, full
+  enumeration vs plan's two examples).** Plan Step 4.4 named
+  `loop_counter.ail` + `loop_in_lambda_e2e.ail` explicitly; the
+  same in-scope action applies to all it.1 loop fixtures.
+  `loop_counter.ail` (loop in `main` body) → `(effects IO Diverge)`.
+  `loop_smoke.ail` `count_to` (loop in fn body) → `(effects
+  Diverge)`. `loop_nested_in_lambda.ail` / `loop_in_lambda_e2e.ail`
+  (loop in a *lam* body) → `(effects Diverge)` on the **lam**, with
+  the enclosing fn / HOF param-and-return fn-types threaded to
+  carry `!Diverge` (effects are part of the function type — forced,
+  not optional). The lam-boundary rule held: `main` in
+  `loop_in_lambda_e2e` does NOT carry Diverge from its own body
+  (the loop is behind the lam edge) but DOES via callee-effect
+  propagation through `apply` (free per DD-4, identical to `!IO`).
+  The injection was not weakened. Both it.1 loop e2e tests
+  (55 / 49) still pass; round-trip green on every modified `.ail`.
+
+- **§4 — `MutualGroup` is a plan-pseudo-vs-real-API refinement.**
+  The plan's `mutual_structural_group -> Vec<&FnDef>` could not
+  express "cross-family mutual recursion must be rejected" — an
+  empty return drops the cross-call from collection instead of
+  flagging it. Split into `{ members: HashSet<String>,
+  family_valid: bool }`: membership drives collection (cross-calls
+  always collected), validity drives the verdict (a cross-call into
+  a family-invalid cycle is unconditionally unguarded). Minimal
+  shape satisfying both plan requirements; same documented
+  substitution class as it.1's repeated plan-pseudo-vs-real notes.
+
+## Known debt
+
+- The structural check's `rec_call_arg_display` has no real
+  term-pretty-printer (only `type_to_string` exists in
+  `ailang_core::pretty`); non-`Var` offending args render as terse
+  tags (`Ctor(…)`, `fn(…)`, `<expr>`). The canonical non-structural
+  case is always a bare `Var` (the param passed unchanged), so this
+  is cosmetic on the diagnostic only; a future term-pretty-printer
+  would improve the `arg` field. Not drift — recorded for
+  visibility.
+- Three exhaustive Term-walks now exist in the it.2 region
+  (`collect_rec_calls_walk`, `collect_direct_app_var_callees`,
+  `term_contains_loop`). Each collects a genuinely different thing
+  with different threading; a shared generic walker would be
+  speculative abstraction per the AILang quality bar. Recorded so a
+  future reader does not mistake the triplication for an oversight.
+- `mutual_structural_group`'s reaches/component BFS is O(n²)-ish
+  over a module's fns, run once per fn-check. Corpus modules are
+  <40 defs; not a hot path. No action; recorded for visibility.
+
+## Blocked detail
+
+None — all 6 tasks completed; the two spec/plan boundary defects
+(Concerns §1, §2) were resolved inside the task's own stated
+acceptance constraints (corpus stays clean, structural check not
+weakened), not escalated, because the carrier explicitly anticipated
+corpus-breakage handling and the resolutions are the spec's own
+transitional model rather than judgement substitutions.
+
+## Files touched
+
+Check core: `crates/ailang-check/src/lib.rs` (CheckError variant +
+code/ctx; `module_fns` thread through check_def/check_fn;
+`verify_structural_recursion` + helpers + `TypeUnionFind` +
+`MutualGroup` + `term_contains_loop`; Diverge injection at
+check_fn / Term::Lam / Term::LetRec sites).
+Tests (new): `crates/ailang-check/tests/structural_recursion_pin.rs`
+(9 pins). Carve-out: `crates/ailang-core/tests/carve_out_inventory.rs`
+(EXPECTED 17→20 + header comment rewritten accurate).
+E2E: `crates/ail/tests/e2e.rs` (2 new Phase-3 tests).
+Spec: `docs/DESIGN.md` (Decision 3 + §Data-model hook).
+Fixtures (new): `examples/struct_rec_list_len.ail`,
+`examples/struct_rec_foldl_sum.ail`,
+`examples/struct_rec_tree_forest.ail`,
+`examples/struct_rec_sum_e2e.ail`,
+`examples/loop_needs_diverge.ail`,
+`examples/test_non_structural_recursion.ail.json`,
+`examples/test_mutual_cross_family.ail.json`,
+`examples/test_loop_missing_diverge.ail.json`.
+Fixtures (modified): `examples/loop_counter.ail`,
+`examples/loop_smoke.ail`, `examples/loop_nested_in_lambda.ail`,
+`examples/loop_in_lambda_e2e.ail` (all four: it.1 loop fixtures →
+`!Diverge`); `examples/rc_pin_recurse_implicit.ail`,
+`examples/rc_let_alias_implicit_param.ail` (transitional `tail-app`
+grandfather on the `loop` fn — Concerns §2).
+
+## Stats
+
+bench/orchestrator-stats/2026-05-15-iter-it.2.json
diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md
index 49de4b5..9076db7 100644
--- a/docs/journals/INDEX.md
+++ b/docs/journals/INDEX.md
@@ -76,3 +76,4 @@
 - 2026-05-15 — iter mut.4-tidy: close mut-local audit drift. Architect's two `[high]` items addressed — new `CheckError::MutVarCapturedByLambda` rejects any lambda whose body's free vars hit the enclosing `mut_scope_stack` (via the existing `desugar::free_vars_in_term` helper, gated on non-empty stack), and `codegen/lambda.rs`'s blame-typechecker `Internal` path becomes `unreachable!` once typecheck is the gate. Two `[medium]` stale-history comments cleaned in DESIGN.md §"Term (expression)" and `ailang-codegen/src/lib.rs`. New negative fixture `examples/test_mut_var_captured_by_lambda.ail.json` + driver test extension; `carve_out_inventory.rs` EXPECTED 12→13. Spec §"Out of scope" amended with the lambda-capture rejection bullet. Bench: `compile_check.py` `check_ms` showed a uniform ~30-50% regression across the suite traced to a fixed-cost startup tax (mut-* added ~1400 lines of typecheck/codegen surface; the short-circuit on empty `mut_scope_stack` walk in Term::Var did not move the needle, falsifying the hot-path hypothesis); ratified as a feature tax with paired baseline update on `bench/baseline_compile.json`. `check.py` tail-noise envelope continues the audit-pd carve-out (no ratify needed). `cross_lang.py` clean. Tests 594 → 598. mut-local milestone audit closed → 2026-05-15-iter-mut.4-tidy.md
 - 2026-05-15 — bugfix mut-diag-double-code: fieldtest F2 — the four mut-local `CheckError` variants embedded `[<code>]` in their `#[error]` Display body while the non-JSON CLI formatter also prepends `[code]`, doubling it in human stderr; dropped the embedded prefix from the four strings, bringing them in line with all non-mut variants; RED-first via `debug` (`ct1_check_cli.rs::check_human_mode_renders_mut_diagnostic_code_exactly_once`), GREEN applied inline as a trivial mechanical edit; tests 598 → 599 → 2026-05-15-bugfix-mut-diag-double-code.md
 - 2026-05-15 — iter it.1: iteration-discipline milestone (1 of 3) — `Term::Loop` / `Term::Recur` / `LoopBinder` added as strictly-additive first-class AST nodes end-to-end: Form-A `parse_loop`/`parse_recur` + print + prose render/free-var/subst lockstep + canonical-JSON serde/round-trip + schema/spec-drift/schema-coverage/carve-out lockstep (13→17) + typecheck (binder typing + recur arity/type unification via `loop_stack: &mut Vec<Vec<Type>>` threaded exactly as mut.2's `mut_scope_stack`; recur-tail-position via a new private `verify_loop_body`, `verify_tail_positions` public signature unchanged) + codegen (loop-header block, one phi per binder, recur back-edge `br` with a NEW parallel `block_terminated` setter, lambda-boundary `loop_frames` save/restore mirroring mut.3). Four new `CheckError` variants `Recur{OutsideLoop,ArityMismatch,TypeMismatch,NotInTailPosition}` (bracket-`[code]`-free Display per the F2 convention). Strictly additive verified — zero deletions touch `tail-app`/`tail-do`, `verify_tail_positions`' tail-app role, or the seven existing codegen `block_terminated` sites (the 32 within-iter deletions are exclusively DD-3 stub-then-fill replacements). `Term::Recur` synth returns a fresh metavar (resolves the plan's flagged `Type::unit()` open risk: recur appears in `if` branches that must unify with the sibling type). `loop_counter.ail`→`55`, `loop_in_lambda_e2e.ail`→`49`, four negatives fire exact codes, `tail-app` fixtures byte-identical, zero IR/prose snapshot drift; `cargo test --workspace` green. Two mut.1-class plan-pseudo-vs-reality substitutions recorded (prose round-trip asserting AST-equality is impossible — no Form-B parser by design; the diagnostic.rs doc-list premise was false) → 2026-05-15-iter-it.1.md
+- 2026-05-15 — iter it.2: iteration-discipline milestone (2 of 3) — structural-recursion guardedness checker + first real `Diverge` effect, strictly additive (nothing `tail`-related removed; that is it.3). New whole-body pass `verify_structural_recursion` runs as a sibling of `verify_tail_positions` in `check_fn`'s post-synth region (DD-1): the `smaller`-set algorithm with implicit candidate-position inference + unconstrained accumulator positions (DD-2 — foldl-shape accumulator classifies as structural recursion, pure+total), self/mutual identification with an inline ADT-family connected-components union-find (DD-3), and the it.2-only `tail==false` grandfather. `CheckError::NonStructuralRecursion {callee,arg}` (bracket-`[code]`-free Display per F2). `term_contains_loop` (stops at `Term::Lam` boundaries, DD-4) injects `"Diverge"` into the raised effect set so the existing `UndeclaredEffect` machinery enforces it with no new diagnostic variant; lam-arrow + `Term::LetRec` sub-effect sites wired (loop behind a lam edge carries `!Diverge` on the lam's arrow, propagating via the free callee-effect path, not leaking to the enclosing fn — exactly as `!IO` scopes). DESIGN.md Decision 3 + §Data-model hook synced present-tense. Four it.1 loop fixtures gained `!Diverge`. Two spec-premise boundary defects surfaced and resolved inside the task's invariants (corpus clean, check not weakened): (§1) the spec's "21 tail-app fixtures" grandfather premise under-counts the corpus — no-ADT-candidate counter recursions (~18, e.g. `build_tree(depth:Int)`) have no structural position to verify and are deferred to it.3 migration; (§2) two RC-regression fixtures (`rc_pin_recurse_implicit`, `rc_let_alias_implicit_param`) hold an ADT param constant while decrementing an Int — genuinely non-structural, joined the spec's transitional `tail-app` grandfather exactly as the other 20 corpus fixtures do (their RC==GC regression guards verified still green; the regression lives in the unchanged `pin`/`pin_aliased` bodies). Both recorded as corrected it.3 corpus-migration scope. `cargo test --workspace` 622 green / 0 red; all 9 acceptance pins non-vacuous (negatives `.contains(code)`); struct_rec_sum→15, loop_needs_diverge→55, the it.1 55/49 e2e still green → 2026-05-15-iter-it.2.md
diff --git a/examples/loop_counter.ail b/examples/loop_counter.ail
index 155dac0..6dabf37 100644
--- a/examples/loop_counter.ail
+++ b/examples/loop_counter.ail
@@ -1,8 +1,8 @@
 (module loop_counter
 
   (fn main
-    (doc "Iter it.1 — sum 1..10 via an accumulator loop. Expected stdout: 55.")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (doc "Iter it.1 — sum 1..10 via an accumulator loop. Iter it.2: loop-bearing ⇒ !Diverge added (D2). Expected stdout: 55.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO Diverge)))
     (params)
     (body
       (app print
diff --git a/examples/loop_in_lambda_e2e.ail b/examples/loop_in_lambda_e2e.ail
index de103f4..369f6e8 100644
--- a/examples/loop_in_lambda_e2e.ail
+++ b/examples/loop_in_lambda_e2e.ail
@@ -1,21 +1,27 @@
 (module loop_in_lambda_e2e
 
   (fn apply
-    (doc "apply a fn-of-Int to an Int")
-    (type (fn-type (params (fn-type (params (con Int)) (ret (con Int))) (con Int)) (ret (con Int))))
+    (doc "apply a fn-of-Int to an Int. Iter it.2: the supplied closure is loop-bearing, so its arrow carries !Diverge — the higher-order param type and apply's own effect row must reflect that (effects are part of the function type).")
+    (type (fn-type (params (fn-type (params (con Int)) (ret (con Int)) (effects Diverge)) (con Int)) (ret (con Int)) (effects Diverge)))
     (params f x)
     (body (app f x)))
 
   (fn main
-    (doc "Iter it.1 — a loop inside a lambda body, invoked via a closure. The lambda computes x*x by summing x exactly x times through an accumulator loop; apply 7 prints 49. Codegen-soundness gate for the lambda-boundary loop_frames save/restore.")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (doc "Iter it.1 — a loop inside a lambda body, invoked via a closure. The lambda computes x*x by summing x exactly x times through an accumulator loop; apply 7 prints 49. Codegen-soundness gate for the lambda-boundary loop_frames save/restore. Iter it.2: !Diverge propagates out through apply (callee-effect propagation).")
+    (type (fn-type (params) (ret (con Unit)) (effects IO Diverge)))
     (params)
     (body
       (app print
         (app apply
+          ; Iter it.2: the loop lives in THIS lambda's body, so the
+          ; lambda's arrow carries !Diverge (DD-4 lam boundary). The
+          ; loop does not leak Diverge to `main` — `main`'s body does
+          ; not syntactically contain the loop (it stops at the lam
+          ; edge, exactly as !IO does).
           (lam
             (params (typed x (con Int)))
             (ret (con Int))
+            (effects Diverge)
             (body
               (loop ((var acc (con Int) 0) (var k (con Int) 0))
                 (if (app == k x)
diff --git a/examples/loop_needs_diverge.ail b/examples/loop_needs_diverge.ail
new file mode 100644
index 0000000..22317b3
--- /dev/null
+++ b/examples/loop_needs_diverge.ail
@@ -0,0 +1,18 @@
+; Iter it.2 positive (DD-4 / D2): a fn whose body contains a
+; `(loop …)` must declare `!Diverge`. This one does — its effect row
+; carries `Diverge` (and `IO`, since it `print`s the result), so the
+; existing declared-vs-raised reconciliation accepts it. Modelled on
+; `loop_counter.ail` (it.1) with `Diverge` added to the effect row.
+
+(module loop_needs_diverge
+
+  (fn main
+    (doc "Sum 1..10 via an accumulator loop; loop-bearing ⇒ !Diverge. Expected stdout: 55.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO Diverge)))
+    (params)
+    (body
+      (app print
+        (loop ((var acc (con Int) 0) (var i (con Int) 1))
+          (if (app > i 10)
+            acc
+            (recur (app + acc i) (app + i 1))))))))
diff --git a/examples/loop_nested_in_lambda.ail b/examples/loop_nested_in_lambda.ail
index 719977e..6a77411 100644
--- a/examples/loop_nested_in_lambda.ail
+++ b/examples/loop_nested_in_lambda.ail
@@ -1,13 +1,14 @@
 (module loop_nested_in_lambda
 
   (fn make_adder
-    (doc "Iter it.1 — a loop inside a lambda body (lambda-boundary analogue).")
-    (type (fn-type (params (con Int)) (ret (fn-type (params (con Int)) (ret (con Int))))))
+    (doc "Iter it.1 — a loop inside a lambda body (lambda-boundary analogue). Iter it.2: the returned closure is loop-bearing, so its arrow carries !Diverge (DD-4 lam boundary); make_adder's return type reflects that. make_adder's own body does not contain the loop (it stops at the lam edge), so make_adder itself stays effect-free.")
+    (type (fn-type (params (con Int)) (ret (fn-type (params (con Int)) (ret (con Int)) (effects Diverge)))))
     (params base)
     (body
       (lam
         (params (typed x (con Int)))
         (ret (con Int))
+        (effects Diverge)
         (body
           (loop ((var acc (con Int) base) (var k (con Int) 0))
             (if (app == k x)
diff --git a/examples/loop_smoke.ail b/examples/loop_smoke.ail
index 4e7b1f0..832fdc2 100644
--- a/examples/loop_smoke.ail
+++ b/examples/loop_smoke.ail
@@ -1,8 +1,8 @@
 (module loop_smoke
 
   (fn count_to
-    (doc "Iter it.1 — single counted loop; counts i up to n and returns n.")
-    (type (fn-type (params (con Int)) (ret (con Int))))
+    (doc "Iter it.1 — single counted loop; counts i up to n and returns n. Iter it.2: loop-bearing ⇒ !Diverge (D2).")
+    (type (fn-type (params (con Int)) (ret (con Int)) (effects Diverge)))
     (params n)
     (body
       (loop ((var i (con Int) 0))
diff --git a/examples/rc_let_alias_implicit_param.ail b/examples/rc_let_alias_implicit_param.ail
index 56a3e10..20ec358 100644
--- a/examples/rc_let_alias_implicit_param.ail
+++ b/examples/rc_let_alias_implicit_param.ail
@@ -59,6 +59,14 @@
           (case (pat-ctor TLeaf) 0)
           (case (pat-ctor TNode v l r) 1)))))
 
+  ; Iter it.2: integer-counter recursion holding the ADT param `t`
+  ; constant — non-structural by the it.2 guardedness check (D2). The
+  ; recursive call is in tail position, so it joins the transitional
+  ; `tail-app` grandfather (spec it.2 "Transitional grandfather") as
+  ; the rest of the corpus does until it.3 migrates such recursions
+  ; to `(loop …)`. The 18g let-alias-mode regression this fixture
+  ; guards lives in `pin_aliased`'s match arm-close, unaffected by
+  ; this tail marking.
   (fn loop
     (type
       (fn-type
@@ -69,7 +77,7 @@
       (if (app == n 0)
         0
         (let _v (app pin_aliased t)
-          (app loop (app - n 1) t)))))
+          (tail-app loop (app - n 1) t)))))
 
   (fn main
     (type (fn-type (params) (ret (con Unit)) (effects IO)))
diff --git a/examples/rc_pin_recurse_implicit.ail b/examples/rc_pin_recurse_implicit.ail
index 15f84cc..7044c1a 100644
--- a/examples/rc_pin_recurse_implicit.ail
+++ b/examples/rc_pin_recurse_implicit.ail
@@ -38,6 +38,14 @@
         (case (pat-ctor TLeaf) 0)
         (case (pat-ctor TNode v l r) 1))))
 
+  ; Iter it.2: this is integer-counter recursion holding the ADT
+  ; param `t` constant — non-structural by the it.2 guardedness
+  ; check (D2). The recursive call is in tail position, so it joins
+  ; the transitional `tail-app` grandfather (spec it.2 "Transitional
+  ; grandfather") exactly as the rest of the corpus does until it.3
+  ; migrates such recursions to `(loop …)`. The 18d.4 regression this
+  ; fixture guards lives in `pin`'s match arm-close, unaffected by
+  ; this tail marking.
   (fn loop
     (type (fn-type (params (con Int) (con Tree)) (ret (con Int))))
     (params n t)
@@ -45,7 +53,7 @@
       (if (app == n 0)
         0
         (let _v (app pin t)
-          (app loop (app - n 1) t)))))
+          (tail-app loop (app - n 1) t)))))
 
   (fn main
     (type (fn-type (params) (ret (con Unit)) (effects IO)))
diff --git a/examples/struct_rec_foldl_sum.ail b/examples/struct_rec_foldl_sum.ail
new file mode 100644
index 0000000..fd7dfa8
--- /dev/null
+++ b/examples/struct_rec_foldl_sum.ail
@@ -0,0 +1,26 @@
+; Iter it.2 positive (spec D1): foldl-shape accumulator. `go` recurses
+; on the Cons-tail `t` at position 0 (structurally guarded) while
+; threading an unconstrained accumulator `acc` at position 1. The
+; accumulator position is never examined by the guardedness check, so
+; this classifies as structural recursion: pure, total, Diverge-free,
+; with NO `tail-app` marker. This is the single most LLM-natural
+; iteration shape and must stay structural (spec D1).
+
+(module struct_rec_foldl_sum
+
+  (data IntList
+    (ctor INil)
+    (ctor ICons (con Int) (con IntList)))
+
+  (fn go
+    (doc "Sum via a foldl-shape accumulator; structural on the tail.")
+    (type
+      (fn-type
+        (params (con IntList) (con Int))
+        (ret (con Int))))
+    (params xs acc)
+    (body
+      (match xs
+        (case (pat-ctor INil) acc)
+        (case (pat-ctor ICons h t)
+          (app go t (app + acc h)))))))
diff --git a/examples/struct_rec_list_len.ail b/examples/struct_rec_list_len.ail
new file mode 100644
index 0000000..99caff8
--- /dev/null
+++ b/examples/struct_rec_list_len.ail
@@ -0,0 +1,24 @@
+; Iter it.2 positive: structural list length. `len` recurses on the
+; Cons-tail `t` (a constructor sub-component of `xs`) via a plain,
+; non-tail `(app len t)`. Structurally guarded at position 0, pure,
+; total, Diverge-free. No `tail-app` marker — this is the structural
+; recursion form the it.2 guardedness check must accept on its own.
+
+(module struct_rec_list_len
+
+  (data IntList
+    (ctor INil)
+    (ctor ICons (con Int) (con IntList)))
+
+  (fn len
+    (doc "Length of an IntList via structural recursion on the tail.")
+    (type
+      (fn-type
+        (params (con IntList))
+        (ret (con Int))))
+    (params xs)
+    (body
+      (match xs
+        (case (pat-ctor INil) 0)
+        (case (pat-ctor ICons h t)
+          (app + 1 (app len t)))))))
diff --git a/examples/struct_rec_sum_e2e.ail b/examples/struct_rec_sum_e2e.ail
new file mode 100644
index 0000000..94ea5fb
--- /dev/null
+++ b/examples/struct_rec_sum_e2e.ail
@@ -0,0 +1,41 @@
+; Iter it.2 Phase-3 e2e: an it.2-clean structural recursion that
+; actually RUNS. `sum` recurses on the Cons-tail `t` via a plain,
+; non-tail `(app sum t)` — structurally guarded ⇒ the it.2 check
+; classifies it pure + total, so it carries NO `!Diverge` and uses
+; NO `tail-app` marker. This proves the structural-recursion
+; classification is behaviourally sound end-to-end (the "total"
+; verdict is not just a typecheck assertion): build [1,2,3,4,5],
+; sum it structurally, print 15.
+
+(module struct_rec_sum_e2e
+
+  (data IntList
+    (ctor INil)
+    (ctor ICons (con Int) (con IntList)))
+
+  (fn sum
+    (doc "Structural sum: plain non-tail recursion on the Cons tail. No !Diverge, no tail-app.")
+    (type
+      (fn-type
+        (params (con IntList))
+        (ret (con Int))))
+    (params xs)
+    (body
+      (match xs
+        (case (pat-ctor INil) 0)
+        (case (pat-ctor ICons h t)
+          (app + h (app sum t))))))
+
+  (fn main
+    (doc "Build [1,2,3,4,5] and print its structural sum. Expected stdout: 15.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (app print
+        (app sum
+          (term-ctor IntList ICons 1
+            (term-ctor IntList ICons 2
+              (term-ctor IntList ICons 3
+                (term-ctor IntList ICons 4
+                  (term-ctor IntList ICons 5
+                    (term-ctor IntList INil)))))))))))
diff --git a/examples/struct_rec_tree_forest.ail b/examples/struct_rec_tree_forest.ail
new file mode 100644
index 0000000..7d67052
--- /dev/null
+++ b/examples/struct_rec_tree_forest.ail
@@ -0,0 +1,43 @@
+; Iter it.2 positive (spec D1, DD-3): mutual structural recursion
+; over one ADT family. `Tree` references `Forest` (the `Node` field)
+; and `Forest` references `Tree` and `Forest` (the `Cons` fields), so
+; the union-find of the ADT type-reference graph puts {Tree, Forest}
+; in a single connected component. `tree_size` recurses into
+; `forest_size` on the `Node`-bound `f` (structurally smaller); each
+; `forest_size` self/cross call passes a `Cons`-bound sub-component.
+; The whole mutual group is structural: pure, total, Diverge-free,
+; no `tail-app` markers.
+
+(module struct_rec_tree_forest
+
+  (data Tree
+    (ctor Node (con Int) (con Forest)))
+
+  (data Forest
+    (ctor FNil)
+    (ctor FCons (con Tree) (con Forest)))
+
+  (fn tree_size
+    (doc "Node count of a tree; recurses into forest_size on the Node forest.")
+    (type
+      (fn-type
+        (params (con Tree))
+        (ret (con Int))))
+    (params tr)
+    (body
+      (match tr
+        (case (pat-ctor Node v f)
+          (app + 1 (app forest_size f))))))
+
+  (fn forest_size
+    (doc "Node count of a forest; mutual with tree_size, self on the tail.")
+    (type
+      (fn-type
+        (params (con Forest))
+        (ret (con Int))))
+    (params fo)
+    (body
+      (match fo
+        (case (pat-ctor FNil) 0)
+        (case (pat-ctor FCons t rest)
+          (app + (app tree_size t) (app forest_size rest)))))))
diff --git a/examples/test_loop_missing_diverge.ail.json b/examples/test_loop_missing_diverge.ail.json
new file mode 100644
index 0000000..82ecbf4
--- /dev/null
+++ b/examples/test_loop_missing_diverge.ail.json
@@ -0,0 +1 @@
+{"defs":[{"body":{"args":[{"binders":[{"init":{"lit":{"kind":"int","value":0},"t":"lit"},"name":"acc","type":{"k":"con","name":"Int"}},{"init":{"lit":{"kind":"int","value":1},"t":"lit"},"name":"i","type":{"k":"con","name":"Int"}}],"body":{"cond":{"args":[{"name":"i","t":"var"},{"lit":{"kind":"int","value":10},"t":"lit"}],"fn":{"name":">","t":"var"},"t":"app"},"else":{"args":[{"args":[{"name":"acc","t":"var"},{"name":"i","t":"var"}],"fn":{"name":"+","t":"var"},"t":"app"},{"args":[{"name":"i","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"}],"t":"recur"},"t":"if","then":{"name":"acc","t":"var"}},"t":"loop"}],"fn":{"name":"print","t":"var"},"t":"app"},"doc":"Loop-bearing fn that omits !Diverge from its effect row — must fire undeclared-effect.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"test_loop_missing_diverge","schema":"ailang/v0"}
diff --git a/examples/test_mutual_cross_family.ail.json b/examples/test_mutual_cross_family.ail.json
new file mode 100644
index 0000000..70a0b76
--- /dev/null
+++ b/examples/test_mutual_cross_family.ail.json
@@ -0,0 +1 @@
+{"defs":[{"ctors":[{"fields":[],"name":"LNil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"MyList"}],"name":"LCons"}],"kind":"type","name":"MyList"},{"ctors":[{"fields":[],"name":"TLeaf"},{"fields":[{"k":"con","name":"MyTree"},{"k":"con","name":"MyTree"}],"name":"TBranch"}],"kind":"type","name":"MyTree"},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"LNil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"},{"args":[{"args":[{"name":"t","t":"var"}],"fn":{"name":"mk_tree","t":"var"},"t":"app"}],"fn":{"name":"g","t":"var"},"t":"app"}],"fn":{"name":"+","t":"var"},"t":"app"},"pat":{"ctor":"LCons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"f recurses into g passing a List sub-component, but g's structural param is an unrelated Tree family.","kind":"fn","name":"f","params":["xs"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"MyList"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[],"ctor":"TLeaf","t":"ctor","type":"MyTree"},"kind":"fn","name":"mk_tree","params":["xs"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"MyList"}],"ret":{"k":"con","name":"MyTree"}}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"TLeaf","fields":[],"p":"ctor"}},{"body":{"args":[{"args":[{"name":"l","t":"var"}],"fn":{"name":"g","t":"var"},"t":"app"},{"args":[{"args":[],"ctor":"LNil","t":"ctor","type":"MyList"}],"fn":{"name":"f","t":"var"},"t":"app"}],"fn":{"name":"+","t":"var"},"t":"app"},"pat":{"ctor":"TBranch","fields":[{"name":"l","p":"var"},{"name":"r","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"tr","t":"var"},"t":"match"},"doc":"g recurses into f, but its own structural param is a Tree (different ADT family).","kind":"fn","name":"g","params":["tr"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"MyTree"}],"ret":{"k":"con","name":"Int"}}}],"imports":[],"name":"test_mutual_cross_family","schema":"ailang/v0"}
diff --git a/examples/test_non_structural_recursion.ail.json b/examples/test_non_structural_recursion.ail.json
new file mode 100644
index 0000000..bb3d534
--- /dev/null
+++ b/examples/test_non_structural_recursion.ail.json
@@ -0,0 +1 @@
+{"defs":[{"ctors":[{"fields":[],"name":"INil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"name":"ICons"}],"kind":"type","name":"IntList"},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"INil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"},{"args":[{"name":"xs","t":"var"}],"fn":{"name":"f","t":"var"},"t":"app"}],"fn":{"name":"+","t":"var"},"t":"app"},"pat":{"ctor":"ICons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Non-structural: recurses on the SAME xs, not a sub-component. Not tail-marked.","kind":"fn","name":"f","params":["xs"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"Int"}}}],"imports":[],"name":"test_non_structural_recursion","schema":"ailang/v0"}