body-lowering: DESIGN + staged plan — faithful runtime-iteration inference

DESIGN.md

@@ -86,6 +86,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`
 - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)
 - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)
 - floor shared-computation memoization — make the double-paid full-tree compile UNREPEATABLE by construction (M1: within-walk resolve memo ~105s; M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md)
+- **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** The substrate models a `Loop` faithfully (measure `^loop_bound_edge` + iteration-fold body, §4), but the inferred tree drops both loop facts: `behavior_multiplicity(Loop)` decides termination **tag-only** (never reading the measure) so every raw loop is `Violates` regardless of its descent evidence (`cardinality.dag:219-228`), the `LoopBound{measure,termination}` carrier that would bind measure→proof is consumed only by the cost/complexity lenses (`cost.dag:168`) which read its `measure` for sizing but **never** its `termination` — and that `termination` field is itself computed **measure-blind** (tag-only, `cardinality.dag:284`), so **no inference consumes the loop's termination fact** (`loop_bound_witness_for_node`, `cardinality.dag:278`), and `04_infer` has **no Loop arm** so the body is typed as an opaque conjunction with no per-iteration `τ→τ` relation. Fix = derive termination from the measure (fail-closed to `DescentUnknown`) + type the body as a repeated transform, both as `Loop` sugar readers (so `For`/`While`/`Retry`/recursion type at once). Blocked-on: a `DescentEvidence` §3 fork (`cardinality.dag:108` bare vs `dag/std/termination.dag` lattice) consolidates first — **authority ruled `dag/std/termination.dag`** (§7; parent 2026-07-03), landing held for the operator's *standing* v2↔dag-fork confirm. FLAG B (Loop-multiplicity asymmetry) SIGNED; FLAG C (refinement loops fail-closed, not fabricated `τ→τ`) SIGNED. → [body-lowering design](docs/plans/body-lowering-design.md)
 
 ## Building & checks