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

[gunbai-bot]

Deliverable for the BODY-LOWERING MILESTONE (design-first, model-before-implement)

This PR is the design + staged plan — no load-bearing pipeline/substrate edits. Each implementation stage is a separate, separately-signed PR (see §5 of the doc).

The gap (from receipts)

DESIGN.md §4: "recursion is sugar over Loop; cyclic relations via acyclic encodings." A Loop node carries its cycle as an acyclic encoding — one ^loop_bound_edge measure + iteration-fold body (node.dag:210,279-284). The substrate models this faithfully; the inferred tree does not interpret it:

1. Termination is decided tag-only. behavior_multiplicity(Loop) (cardinality.dag:219-228) takes only the Behavior tag — the measure is structurally out of scope — so every raw loop is Violates regardless of its descent evidence.
2. The faithful carrier is a dead scaffold. LoopBound{measure, termination} / loop_bound_witness_for_node (cardinality.dag:278) has zero callers, and even it computes termination without reading the measure it just extracted.
3. No Loop arm in 04_infer. Branch/Match get per-arm body-typing + unification; Loop falls to the generic path and is typed as an opaque conjunction — no per-iteration τ→τ relation.

Thesis

Derive the loop's type from its measure and its body, not its tag: (T1) termination = a lattice-meet over the measure's DescentEvidence, fail-closed to DescentUnknown → Violates; (T2) type the body as a repeated transform with a fixpoint relation. Both are Loop sugar readers, so For/While/Retry/recursion type at once (no N×M).

Adjacent finding (blocks Stage 1)

DescentEvidence is forked (§3): bare cardinality.dag:108-111 vs the richer dag/std/termination.dag lattice (meet/join/promote_to_strict). The fix needs the lattice (multi-measure loops terminate by meet), so consolidation onto one authority must land first.

Staged plan

0. This PR (docs). 1. Consolidate DescentEvidence (FLAG A). 2. Node-aware Loop multiplicity + wire the dead carrier (T1). 3. Loop arm in 04_infer (T2). 4. (optional) body-producer fixture realism.

Every stage carries a discriminating red control (perturb the measure/body → verdict flips) per DESIGN.md §5.

Open flags for operator sign

• A — which layer owns the single DescentEvidence authority (v2 src/v2/std vs dag/std)?
• B — Loop multiplicity decided one layer up (node_multiplicity) while other behaviors stay tag-only — accept the asymmetry?
• C — first cut requires carrier-invariant loops (τ→τ); refinement-typed loops are a named follow-on.

Full design: docs/plans/body-lowering-design.md. Registered as a DESIGN.md open thread.

[gunbai-bot]

Fixed in 23fcdb0 — the caller receipt was wrong and I've corrected it.

Verified against the live tree: `loop_bound_witness_for_node` is indeed called from `src/v2/lens/cost.dag:168` (`base_cost_for_loop`) and `src/v2/test/claim/complexity_gate/subject_complexity_budget_roster.dag:45` — not zero-callers. My exploration only grepped `std`/`compiler` and missed `lens/` and `test/`; thanks for catching it against DESIGN.md's verify-receipts bar.

I've rewritten gap 2 (and the DESIGN.md bullet + Stage 2) to its real, sound point, which you flagged as intact: those existing consumers read only the carrier's `measure` field (for cost sizing, `linear_in_node(measure)`), never its `termination` field — and that `termination` is itself computed measure-blind via the tag-only `termination_proof_witness_for_node` (`cardinality.dag:284`). So the two-fold gap is (a) no inference consumer of the carrier and (b) its `termination` field is a hollow second representation of a proof the measure already determines. Stage 2 now targets the "first measure-aware termination consumer," not "first caller," so wiring instructions don't misroute implementers. Dropped the "dead scaffold" framing entirely.

— sent from fierce-bee-749