spec: correct it.3 §Remove + §Codegen-rework (it.3-recon-surfaced defects)

Two HEAD-vs-spec defects the it.3 recon found, fixed at the spec:
(1) "remove is_false" was wrong — is_false is shared with
WorkspaceDef.drop_iterative; it survives, doc re-scoped only.
(2) "remove the Decision-3 Diverge line" struck — it.2 already
rewrote Decision 3 to make Diverge the real effect (the milestone's
payload); it.3 touches Decision 8 only.
(3) The codegen-rework bullet under-described the real risk: the
18g.1 pre-tail-call husk-dec (match_lower.rs:658-736) reads
Term::App{tail:true} directly, protects the 18f.2 RC-RSS pin, and
its field-forced deletion is RC-safe ONLY if it.1 loop codegen
drops superseded owned binders across recur — unverified. Spec now
names this as the load-bearing it.3 risk with a RED-gated
verification + a named remediation (owned-loop-binder-drop-on-recur
in scope for it.3). Only 3 (not 7) setters are tail-driven.
No design decision (D1-D4) changes; design validated by shipped
it.1/it.2. Not relitigating shipped work (spec_over_plan_patches).

docs/specs/2026-05-15-iteration-discipline.md

@@ -217,25 +217,74 @@ lower + escape → e2e example.
 
 ### it.3 — retire `tail-app` / `tail-do`
 
-- **Remove.** `Term::App.tail`, `Term::Do.tail`, `is_false`;
+- **Remove.** `Term::App.tail`, `Term::Do.tail` (the two `tail`
+  fields only — **not** the `is_false` serde helper: it.1/it.2-era
+  recon found `is_false` is shared with `WorkspaceDef.drop_iterative`;
+  it survives, only its doc-comment is re-scoped);
   `tail-app` / `tail-do` dispatch + `parse_tail_app` /
   `parse_tail_do` + the keyword-list entries + the `print.rs`
-  `(tail-app …)`/`(tail-do …)` arms + the prose `"tail "` projection;
+  `(tail-app …)`/`(tail-do …)` arms + the prose `"tail "` projection
+  (render + subst arms; the free-var counter arms are already
+  `tail`-agnostic);
   `verify_tail_positions`'s tail-app role (the pass keeps only the
-  `recur`-in-tail-position role from it.1); `CheckError::
-  TailCallNotInTailPosition`; the `musttail` lowering in `emit_call`
+  `recur`-in-tail-position role from it.1 — note `verify_tail_positions`
+  and `verify_loop_body` are entangled mutual recursion: the tail-app
+  arms are deleted in place, the functions are not removed);
+  `CheckError::TailCallNotInTailPosition` (+ its `code()` arm; it has
+  no dedicated `ctx()` arm — it falls into the catch-all, so no
+  `ctx()` edit); the `musttail` lowering in `emit_call`
   / `emit_indirect_call` and the `tail call` hint in
   `lower_effect_op`. DESIGN.md Decision 8 rewritten as *superseded*
   (kept as a tombstone explaining why explicit tail calls were
   retired — the schema-drift anchors and EBNF/jsonc blocks updated in
-  lockstep); the Decision-3 `Diverge` line and the EBNF
-  `tail-app-term` production removed.
-- **Codegen block-termination rework.** The `block_terminated = true`
-  seam, currently set by `tail: true` and consumed by
-  `match_lower.rs:658–913` + `lib.rs:1238–1577`, becomes solely
-  `recur`'s (and the ordinary fall-through `ret`). This is the only
-  non-mechanical part of it.3 and the reason it.1 ships the new seam
-  first.
+  lockstep); the EBNF `tail-app-term`/`tail-do-term` productions
+  removed.
+
+  > **Correction (it.3-recon-surfaced).** The original draft also
+  > said "the Decision-3 `Diverge` line removed". That clause is
+  > **struck**: it.2 already rewrote Decision 3 to make `Diverge`
+  > the *real* effect of `loop`-bearing code — that rewrite is the
+  > milestone's central payload and stays verbatim. it.3 touches
+  > Decision **8** only (tombstone), never Decision 3.
+
+- **Codegen block-termination rework + the 18g.1 husk-dec deletion
+  (the real non-mechanical part).** Two coupled things, only one of
+  which the original draft named:
+  1. *`block_terminated` seam.* Only **three** setters are
+     tail-driven (`emit_call`, `emit_indirect_call`,
+     `lower_effect_op`) — not "seven"; the it.1 journal's "seven"
+     was stale. They are removed with the `musttail` lowering. Every
+     other `block_terminated` consumer (`lib.rs` fn-body
+     fall-through `ret`, Let-scope binder dec, if-branch join
+     bookkeeping; `match_lower.rs` arm-close/phi gates;
+     `lambda.rs` save/restore) is `block_terminated`-mediated and
+     `recur`'s it.1 setter feeds the identical signal — these
+     re-verify clean.
+  2. *18g.1 pre-tail-call shallow husk-dec
+     (`match_lower.rs:658–736`).* This is the **one consumer that
+     reads `Term::App{tail:true}` DIRECTLY**, not via
+     `block_terminated`. It is an RC-correctness optimisation
+     written to fix the **18f.2 tail-latency RC-RSS pin** (a
+     `musttail call … ret` strands the moved-from scrutinee's outer
+     cons-cell husk; 18g.1 shallow-decs it pre-emptively). Removing
+     the `tail` field forces this block's deletion (it no longer
+     compiles). The original spec framed the codegen rework as
+     "solely the `block_terminated` seam" and **missed this**.
+     `recur` is a back-edge `br` (no `musttail`, no frame-exit
+     `ret`) so it strands no husk **iff** it.1's loop codegen drops
+     superseded *owned* binder values across the back-edge. The
+     spec's "it.1 ships the seam first" claim is verified for the
+     `block_terminated` half but is **unverified for the
+     owned-binder-drop half**. it.3 therefore: (i) deletes 18g.1
+     (mechanically forced); (ii) re-runs the 18f.2 / RC-RSS bench
+     pins post-migration as the **gate**; (iii) if RED, the
+     remediation is **owned-loop-binder-drop-on-`recur` added to
+     loop codegen** — this is in scope for it.3 (it is the loop-side
+     of the seam the spec wrongly claimed it.1 fully shipped),
+     **not** a reason to keep 18g.1 (which cannot survive the field
+     removal). This contingency + its named remediation is the
+     load-bearing risk of the milestone; the it.3 plan carries it as
+     a RED-gated step, not a footnote.
 - **Corpus migration (full non-structural set — see the
   Scope-correction note; ~20 tail-app + ~18 no-ADT-candidate +
   the 2 RC fixtures, exact set is the it.3 plan's recon job).**