diff --git a/DESIGN.md b/DESIGN.md
index 25e3b11f227..481241ff0b8 100644
--- a/DESIGN.md
+++ b/DESIGN.md
@@ -89,7 +89,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`
 - 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)
 - **duplicate work = the content-hash qualification of `Materialization`** — the operator's "kill compile→…→recompile" generalized codebase-wide, corrected off a §3 catch: it is NOT a new lens but the qualification step *inside* the spine's `materialize` — the generalization of `std.realization` `reconcile`/`has_collapsible_peer` from the effect-pairwise `create_double_init_collapsible` key to a `ComputationIdentity` lattice (`StructurallyIdentical | NormalizedIdentical | ExtensionallyIdentical{bound} | IdentityUnknown{cause}`, mirroring `DescentEvidence`). Two coupled halves (assembly line): **Half A** = materialization describes the result of *all* computation (spine lane, `materialize`/FLAG D — not just `RealizedStep` effects); **Half B** = the generalized qualifier + multiplicity-source axis (fork/placement/runtime/scope) that picks the fix (this lane). `.dag` boundedness demotes the "undecidable" residue: `IdentityUnknown` is never permanent — it is a *typed, located* `MissingConcept | MissingEnforcement | BoundUnmodeled` debt (the undecidability often *is* a §3 fork), so the lens's product is the located root, not the symptom (§6 moat). Placement-grain flagship (CI release build across 3 `needs:[]` jobs → 1 violation, rewire → clean) proven green-by-execution. No S2 dep; couples to the materialization model. → [duplicate-work design](docs/plans/duplicate-work-graph-lens-design.md)
-- **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** Stages 1–3 LANDED (#6373): `DescentEvidence` consolidated onto its single authority `dag/std/termination.dag` (§7 ruling, parent 2026-07-03), `loop_multiplicity` is node-aware (termination derived from the `^loop_bound_edge` measure, fail-closed to `DescentUnknown`; FLAG B asymmetry rationale in-code), `04_infer` has a Loop arm typing the iteration fold `τ→τ` with refinement-shaped loops refused, never fabricated (FLAG C), and fold-family calls desugar to seam `Loop` nodes (`fold_lowering.dag`). Remaining keystone: the **general body producer** — real ingested fn bodies still never become substrate behaviors (the MVP `03_body_producer` is fixture-bound to bespoke flat-token productions; the accumulator-copy lens's prove-safe-or-refuse `Unclassifiable` buckets and unit-cost call pricing are the displaced cost). Fix = the forward reading of the same `GrammarRelationRow` rows the emitter reads backward (§4 one-grammar-both-directions): one row-selected fold in normalize, exactly-one selection fail-closed, staged within-body → cross-decl → per-op derivation, each stage priced by the refusal buckets it zeroes with RED controls kept live. → [body-lowering design](docs/plans/body-lowering-design.md) · [general body producer design](docs/plans/general-body-producer-design.md)
+- **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** Stages 1–3 LANDED (#6373): `DescentEvidence` consolidated onto its single authority `dag/std/termination.dag` (§7 ruling, parent 2026-07-03), `loop_multiplicity` is node-aware (termination derived from the `^loop_bound_edge` measure, fail-closed to `DescentUnknown`; FLAG B asymmetry rationale in-code), `04_infer` has a Loop arm typing the iteration fold `τ→τ` with refinement-shaped loops refused, never fabricated (FLAG C), and fold-family calls desugar to seam `Loop` nodes (`fold_lowering.dag`). FLAGs D/E/F operator-SIGNED 2026-07-10 and the within-body FACT layer LANDED (#6443): one sugar rule table (`SugarKey` = surface-atom | production identity, type_alias_rhs migrated as proof), the 3-edge seam Loop (`^loop_carrier_edge`, at-most-one, excluded from the iteration fold in one motion; the lens carrier read is a named-edge lookup, the surface navigation deleted), the lexeme-stamped let binder, and the lens definition closure (`let grown = acc` a PROVEN suspect, transitively; pure-literal RHS decides clean; unbound RHS still refuses — the may_alias false-alarm class is dead; `^fold_accumulator_unread` narrowed to the named-step residue, a Stage-B callee-resolution fact). FLAG D condition: the binding-key re-grounding is REQUIRED cleanup before the feature closes. Remaining keystone: the **general body producer** — real ingested fn bodies still never become substrate behaviors (the MVP `03_body_producer` is fixture-bound to bespoke flat-token productions); the fn_decl→Arrow producer rows + scaffold dissolution are gated on the namespace lane's containment `SymbolIndex`, staged behind a typed wrapper-retained frontier (lowered | wrapper-retained{cause}, counted, corpus stays green). Fix = the forward reading of the same `GrammarRelationRow` rows the emitter reads backward (§4 one-grammar-both-directions): one row-selected fold in normalize, exactly-one selection fail-closed, staged within-body → cross-decl → per-op derivation, each stage priced by the refusal buckets it zeroes with RED controls kept live. → [body-lowering design](docs/plans/body-lowering-design.md) · [general body producer design](docs/plans/general-body-producer-design.md)
 - **namespace-only name resolution — the containment tree is the single naming authority (operator-signed 2026-07-06).** Supersedes resolver-graph-major §1c's *import-name-universe* ("own declarations ∪ direct import lists" visibility), carrying forward its mechanics unchanged (binding-edge owner, unbound/double-bound = error, patterns-via-scrutinee, no expected-type picker). One structure — **syntactic containment** — induces everything at once: qualified name = nesting position (`T{a}` → `a` *is* `T.a`; `T{a{a}}` → inner *is* `T.a.a`, so Rule-2 no-ambiguity holds by construction), reference = lexical lookup up the ancestor chain (a sibling module is visible, its members projected `node.Symbol`), `.` = projection one level down (field / module-member / variant — one op), and `.` *is* the `std.induction` sub-value relation (descent evidence). So one content-addressed tree grounds THREE consumers — resolution *walks* it, content-addressing *hashes* it, termination reads its *sub-value* edges (§2 Realization: one structure, N consumers). Frontend BUILDS the tree from nesting (pure structure, zero resolution logic); backend WALKS it (lexical up, project down) — no heuristics to tune (the tuning risk = resolving against a flat index instead of the tree). Two governing rules (operator, 2026-07-06): **no dual representation / minimal at every layer; no ambiguity at any layer.** Rides on `SymbolIndex` = "the containment tree materialized" (`type-env-single-authority`, lively-raven lane), gated on loyal-heron's scaling receipt before any resolver surgery; `import-scoped` (§1c, today) and `namespace-only-Y` (position-info uniqueness: expected type filters a variant to one, never picks) are two walk-rules over one *fill-agnostic* index (fill = whole tree; policy gates lookup, never fill). Census: 98% of names globally unique → always bare; the residue is v1-seed forks (resolve by subtree, free) + github-style variants ((Y) context-resolves); no consolidate-now forks (the census's 2 same-name flags proved to be a homonym + whole-file v1-seed duplication, not genuine cross-tree §3 forks). Terminal step: delete the `import` grammar + supporting code → `import` becomes a *parse error*, deps derived from `container.member` references (Rule-1 end-state). → [namespace-only resolution design](docs/plans/namespace-resolution-design.md)
 
 ## Building & checks
diff --git a/dag/gunbc/design_document.dag b/dag/gunbc/design_document.dag
index 686d2980816..2e501773d70 100644
--- a/dag/gunbc/design_document.dag
+++ b/dag/gunbc/design_document.dag
@@ -148,7 +148,7 @@ fn open_threads_blocks() -> List<MarkdownBlock> {
       li(text: "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.)"),
       li(text: "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)"),
       li(text: "**duplicate work = the content-hash qualification of `Materialization`** — the operator's \"kill compile→…→recompile\" generalized codebase-wide, corrected off a §3 catch: it is NOT a new lens but the qualification step *inside* the spine's `materialize` — the generalization of `std.realization` `reconcile`/`has_collapsible_peer` from the effect-pairwise `create_double_init_collapsible` key to a `ComputationIdentity` lattice (`StructurallyIdentical | NormalizedIdentical | ExtensionallyIdentical\{bound\} | IdentityUnknown\{cause\}`, mirroring `DescentEvidence`). Two coupled halves (assembly line): **Half A** = materialization describes the result of *all* computation (spine lane, `materialize`/FLAG D — not just `RealizedStep` effects); **Half B** = the generalized qualifier + multiplicity-source axis (fork/placement/runtime/scope) that picks the fix (this lane). `.dag` boundedness demotes the \"undecidable\" residue: `IdentityUnknown` is never permanent — it is a *typed, located* `MissingConcept | MissingEnforcement | BoundUnmodeled` debt (the undecidability often *is* a §3 fork), so the lens's product is the located root, not the symptom (§6 moat). Placement-grain flagship (CI release build across 3 `needs:[]` jobs → 1 violation, rewire → clean) proven green-by-execution. No S2 dep; couples to the materialization model. → [duplicate-work design](docs/plans/duplicate-work-graph-lens-design.md)"),
-      li(text: "**body-lowering — make v2's inferred tree faithfully represent runtime iteration.** Stages 1–3 LANDED (#6373): `DescentEvidence` consolidated onto its single authority `dag/std/termination.dag` (§7 ruling, parent 2026-07-03), `loop_multiplicity` is node-aware (termination derived from the `^loop_bound_edge` measure, fail-closed to `DescentUnknown`; FLAG B asymmetry rationale in-code), `04_infer` has a Loop arm typing the iteration fold `τ→τ` with refinement-shaped loops refused, never fabricated (FLAG C), and fold-family calls desugar to seam `Loop` nodes (`fold_lowering.dag`). Remaining keystone: the **general body producer** — real ingested fn bodies still never become substrate behaviors (the MVP `03_body_producer` is fixture-bound to bespoke flat-token productions; the accumulator-copy lens's prove-safe-or-refuse `Unclassifiable` buckets and unit-cost call pricing are the displaced cost). Fix = the forward reading of the same `GrammarRelationRow` rows the emitter reads backward (§4 one-grammar-both-directions): one row-selected fold in normalize, exactly-one selection fail-closed, staged within-body → cross-decl → per-op derivation, each stage priced by the refusal buckets it zeroes with RED controls kept live. → [body-lowering design](docs/plans/body-lowering-design.md) · [general body producer design](docs/plans/general-body-producer-design.md)"),
+      li(text: "**body-lowering — make v2's inferred tree faithfully represent runtime iteration.** Stages 1–3 LANDED (#6373): `DescentEvidence` consolidated onto its single authority `dag/std/termination.dag` (§7 ruling, parent 2026-07-03), `loop_multiplicity` is node-aware (termination derived from the `^loop_bound_edge` measure, fail-closed to `DescentUnknown`; FLAG B asymmetry rationale in-code), `04_infer` has a Loop arm typing the iteration fold `τ→τ` with refinement-shaped loops refused, never fabricated (FLAG C), and fold-family calls desugar to seam `Loop` nodes (`fold_lowering.dag`). FLAGs D/E/F operator-SIGNED 2026-07-10 and the within-body FACT layer LANDED (#6443): one sugar rule table (`SugarKey` = surface-atom | production identity, type_alias_rhs migrated as proof), the 3-edge seam Loop (`^loop_carrier_edge`, at-most-one, excluded from the iteration fold in one motion; the lens carrier read is a named-edge lookup, the surface navigation deleted), the lexeme-stamped let binder, and the lens definition closure (`let grown = acc` a PROVEN suspect, transitively; pure-literal RHS decides clean; unbound RHS still refuses — the may_alias false-alarm class is dead; `^fold_accumulator_unread` narrowed to the named-step residue, a Stage-B callee-resolution fact). FLAG D condition: the binding-key re-grounding is REQUIRED cleanup before the feature closes. Remaining keystone: the **general body producer** — real ingested fn bodies still never become substrate behaviors (the MVP `03_body_producer` is fixture-bound to bespoke flat-token productions); the fn_decl→Arrow producer rows + scaffold dissolution are gated on the namespace lane's containment `SymbolIndex`, staged behind a typed wrapper-retained frontier (lowered | wrapper-retained\{cause\}, counted, corpus stays green). Fix = the forward reading of the same `GrammarRelationRow` rows the emitter reads backward (§4 one-grammar-both-directions): one row-selected fold in normalize, exactly-one selection fail-closed, staged within-body → cross-decl → per-op derivation, each stage priced by the refusal buckets it zeroes with RED controls kept live. → [body-lowering design](docs/plans/body-lowering-design.md) · [general body producer design](docs/plans/general-body-producer-design.md)"),
       li(text: "**namespace-only name resolution — the containment tree is the single naming authority (operator-signed 2026-07-06).** Supersedes resolver-graph-major §1c's *import-name-universe* (\"own declarations ∪ direct import lists\" visibility), carrying forward its mechanics unchanged (binding-edge owner, unbound/double-bound = error, patterns-via-scrutinee, no expected-type picker). One structure — **syntactic containment** — induces everything at once: qualified name = nesting position (`T\{a\}` → `a` *is* `T.a`; `T\{a\{a\}\}` → inner *is* `T.a.a`, so Rule-2 no-ambiguity holds by construction), reference = lexical lookup up the ancestor chain (a sibling module is visible, its members projected `node.Symbol`), `.` = projection one level down (field / module-member / variant — one op), and `.` *is* the `std.induction` sub-value relation (descent evidence). So one content-addressed tree grounds THREE consumers — resolution *walks* it, content-addressing *hashes* it, termination reads its *sub-value* edges (§2 Realization: one structure, N consumers). Frontend BUILDS the tree from nesting (pure structure, zero resolution logic); backend WALKS it (lexical up, project down) — no heuristics to tune (the tuning risk = resolving against a flat index instead of the tree). Two governing rules (operator, 2026-07-06): **no dual representation / minimal at every layer; no ambiguity at any layer.** Rides on `SymbolIndex` = \"the containment tree materialized\" (`type-env-single-authority`, lively-raven lane), gated on loyal-heron's scaling receipt before any resolver surgery; `import-scoped` (§1c, today) and `namespace-only-Y` (position-info uniqueness: expected type filters a variant to one, never picks) are two walk-rules over one *fill-agnostic* index (fill = whole tree; policy gates lookup, never fill). Census: 98% of names globally unique → always bare; the residue is v1-seed forks (resolve by subtree, free) + github-style variants ((Y) context-resolves); no consolidate-now forks (the census's 2 same-name flags proved to be a homonym + whole-file v1-seed duplication, not genuine cross-tree §3 forks). Terminal step: delete the `import` grammar + supporting code → `import` becomes a *parse error*, deps derived from `container.member` references (Rule-1 end-state). → [namespace-only resolution design](docs/plans/namespace-resolution-design.md)"),
     ]),
   ]
diff --git a/docs/plans/general-body-producer-design.md b/docs/plans/general-body-producer-design.md
index 8329244e9bd..87e528a0db2 100644
--- a/docs/plans/general-body-producer-design.md
+++ b/docs/plans/general-body-producer-design.md
@@ -195,6 +195,22 @@ unresolvable callee still refuses).
   *Discipline:* the Loop edge addition must update `loop_behavior_edges_conform`,
   `loop_edge_contributes_to_iteration_fold` (`node.dag:374-387`, consumed by `cost.dag:381`), and
   canonical hashing **in one motion** — a partial update forks the well-formedness authority.
+  *Landed (PR #6443, 2026-07-10) — the within-body FACT layer:* FLAG E one-table consolidation
+  (`SugarKey` = surface-atom | production identity; type_alias_rhs migrated as the proof); FLAG F
+  3-edge seam Loop (exactly-one-legal-name `^loop_carrier_edge`, at-most-one, excluded from the
+  iteration fold in the same motion; both extra-named-edge RED controls still fire) with the seam
+  widened to the whole fold family and the lens's carrier read repointed to
+  `loop_carrier_binder_target` (the surface fn_literal navigation deleted — one authority);
+  the let binder is lexeme-stamped via `dag_grammar_binding_name_terminal` (the Bind prerequisite);
+  and the lens's definition closure decides aliasing (`let grown = acc` is now a PROVEN suspect,
+  transitive; pure-literal RHS decides fresh/clean; an unbound RHS records no binding and the
+  may_alias refusal stands — RED control `let_unknown_alias_still_refuses_may_alias`).
+  `^fold_accumulator_unread` narrows to the named-step residue (`f: step` — a callee-resolution
+  fact, Stage B). *Remaining in Stage A:* the fn_decl/fn_literal → Arrow producer rows and the
+  scaffold dissolution — **gated on the namespace lane's containment `SymbolIndex`** (decl names
+  bind via module-root edges / the namespace authority, not decl subtrees; a near-zero-coverage
+  slice would land a dual authority without dissolving anything), staged behind the typed
+  wrapper-retained frontier (lowered | wrapper-retained{cause}, counted, corpus stays green).
 
 - **Stage B — cross-decl resolution.** Callee signatures resolve named args to declaration
   positions; qualified heads resolve through the containment tree (rides the namespace-only lane's
@@ -206,8 +222,8 @@ unresolvable callee still refuses).
 - **Stage C — per-op derivation.** Run the cost lens over each callee's own lowered body and
   derive, per parameter port, whether output size is linear in that port — materialized as
   `CopiedPortFact` rows (reuse the carrier, `algebra.dag:707-710`; §2's net-concepts test). The
-  hand registry becomes a citation cache; fold-family membership (`is_fold_family_head`, which
-  today omits `fold_list_right` — its own citation's copy mechanism) is likewise derived.
+  hand registry becomes a citation cache; fold-family membership (`fold_family_head`, owned by
+  `v2.compiler.fold_lowering` since PR #6443 — one authority for seam and lens) is likewise derived.
   *Dissolves:* `^combiner_unregistered_carrier_reaches` and the calls-inside-argument half of
   `^copied_port_computed_argument`; the closed-world refusal is **retained** for callees whose
   bodies cannot be resolved or priced.
@@ -255,27 +271,28 @@ rows on the frontier, not surprises:
 - No escape hatches: there is no mode in which the producer "proceeds as if" a refusal had not
   fired; diagnostic replay reads state only.
 
-## 9. Flags for operator sign
-
-- **FLAG D — binding-key protocol.** Eval resolves param refs by structural node equality against
-  `symbol_atom_node(binding)`; the lowering conforms by emitting occurrence-normalized synthetic
-  param refs. The alternative — re-grounding `EnvironmentBindingKey` on binding *identity* rather
-  than whole-node equality — is cleaner but is an eval-protocol change. Recommendation: conform
-  now; name the identity re-grounding as a follow-on with the silent `allocate_literal`
-  fall-through (a §5 fail-open the current protocol carries) as its motivating defect.
-- **FLAG E — one rule table.** Generalize the `SugarRule` key to (surface-atom | production
-  identity) and migrate the existing type_alias_rhs hook onto it, vs adding fn_decl as a sibling
-  hand-inlined arm with a declared consolidation trigger. Recommendation: one table — the sibling
-  arm is the nickname trap in slow motion.
-- **FLAG F — Loop accumulator edge.** Extends the seam Loop from 2 to 3 edges (body, measure,
-  carrier binder). Touches `LoopBoundEdges` conformance, the iteration-fold edge predicate, and
-  canonical hashing in one motion; termination and cost consumers are unaffected (they read the
-  measure edge, which is unchanged). Recommendation: sign the 3-edge shape now so Stage A does not
-  need a mid-flight shape change.
+## 9. Flags — SIGNED (operator, 2026-07-10)
+
+- **FLAG D — binding-key protocol. SIGNED: conform now.** Eval resolves param refs by structural
+  node equality against `symbol_atom_node(binding)`; the lowering conforms by emitting
+  occurrence-normalized synthetic param refs. The identity re-grounding of `EnvironmentBindingKey`
+  (which also deletes the silent `allocate_literal` fall-through, a §5 fail-open the current
+  protocol carries) is **required cleanup before this feature closes** — operator condition on the
+  sign, carried in the dissolution trigger below, not an optional follow-on.
+- **FLAG E — one rule table. SIGNED: one table.** Generalize the `SugarRule` key to (surface-atom
+  | production identity) and migrate the existing type_alias_rhs hook onto it as the proof; no
+  sibling hand-inlined arm.
+- **FLAG F — Loop accumulator edge. SIGNED: 3-edge shape.** The seam Loop grows body + measure +
+  carrier binder; `LoopBoundEdges` conformance, the iteration-fold edge predicate, and canonical
+  hashing update in one motion. Termination and cost consumers unaffected (they read the measure
+  edge, unchanged).
 
 ## Dissolution trigger (DESIGN §6)
 
-This document dissolves when Stage D lands: the general producer subsumes `03_body_producer.dag`'s
-fixture family and the lens's within-body/cross-decl refusal buckets are zeroed with live RED
-controls — at which point the surviving content (the §7 cost carriers) migrates to its own
+This document dissolves when BOTH hold: (1) Stage D lands — the general producer subsumes
+`03_body_producer.dag`'s fixture family and the lens's within-body/cross-decl refusal buckets are
+zeroed with live RED controls; and (2) the FLAG D binding-key re-grounding lands —
+`EnvironmentBindingKey` keyed on binding identity and the silent `allocate_literal` fall-through
+deleted (the feature does not close over the conform-time protocol; operator condition,
+2026-07-10). At that point the surviving content (the §7 cost carriers) migrates to its own
 follow-on design and this file is deleted.
diff --git a/src/v2/compiler/03_normalize.dag b/src/v2/compiler/03_normalize.dag
index 9ec8b0cfa1c..3ca079858bb 100644
--- a/src/v2/compiler/03_normalize.dag
+++ b/src/v2/compiler/03_normalize.dag
@@ -1,7 +1,7 @@
 module v2.compiler.normalize
 
 import v2.std.algebra { list_snoc_item }
-import v2.std.collection { Absent, Present }
+import v2.std.collection { Absent, Present, optional_absent, optional_present }
 import v2.std.grammar { ParseTree }
 
 import v2.std.diagnostic {
@@ -18,7 +18,7 @@ import v2.std.diagnostic {
   rejected_with_pending
 }
 import v2.std.node {
-  Disj,
+  Atom,
   Edge,
   Node,
   Symbol,
@@ -27,12 +27,13 @@ import v2.std.node {
   well_formed
 }
 import v2.std.compilers.sugar {
+  ProductionIdentityKey,
+  SugarKey,
+  SurfaceAtomKey,
   apply_sugar,
-  classify_sugar,
-  sugar_fold_coproduct_pipe_chain
+  sugar_rule_for_key
 }
 import v2.extdeps.languages.dag {
-  parse_production_captured_child_optional,
   parse_production_emitted_identity_optional
 }
 
@@ -74,56 +75,38 @@ fn normalize_fold_step(acc: Outcome<Node>, edge: Edge, child: Outcome<Node>) ->
   }
 }
 
-fn normalize_production_coproduct_fold(
-  n: Node,
-  folded: Node,
-  cd: Diagnostics
-) -> Outcome<Node> {
-  match parse_production_emitted_identity_optional(node: folded) {
-    Present { value: id } =>
-      if id == ^dag_surface_type_alias_rhs {
-        match parse_production_captured_child_optional(node: folded) {
-          Present { value: captured } =>
-            match sugar_fold_coproduct_pipe_chain(captured: captured, shell: n) {
-              Rejected { diagnostics: r } =>
-                Rejected {
-                  diagnostics: rejected_with_pending(pending: cd, rejected: r)
-                }
-              Accepted { value: result, diagnostics: d } =>
-                match result.kind {
-                  TypeNode { connective: Disj } =>
-                    Accepted {
-                      value: result,
-                      diagnostics: diagnostics_merge(outer: cd, inner: d)
-                    }
-                  _ =>
-                    Accepted { value: folded, diagnostics: cd }
-                }
-            }
-          Absent =>
-            Accepted { value: folded, diagnostics: cd }
-        }
-      } else {
-        Accepted { value: folded, diagnostics: cd }
+fn normalize_sugar_key_optional(folded: Node) -> SugarKey? {
+  match folded.kind {
+    TypeNode { connective: Atom { identity: id } } =>
+      optional_present(value: SurfaceAtomKey { atom: id })
+    TypeNode { connective: _ } =>
+      match parse_production_emitted_identity_optional(node: folded) {
+        Present { value: id } =>
+          optional_present(value: ProductionIdentityKey { identity: id })
+        Absent => optional_absent()
       }
-    Absent =>
-      Accepted { value: folded, diagnostics: cd }
+    ComputationNode { behavior: _ } => optional_absent()
   }
 }
 
 fn normalize_sugar_finish(n: Node, folded: Node, cd: Diagnostics) -> Outcome<Node> {
-  match classify_sugar(n: n) {
-    Present { value: rule } =>
-      match apply_sugar(rule: rule, n: n, children: folded.children) {
-        Rejected { diagnostics: r } =>
-          Rejected {
-            diagnostics: rejected_with_pending(pending: cd, rejected: r)
-          }
-        Accepted { value: v, diagnostics: d } =>
-          Accepted {
-            value: v,
-            diagnostics: diagnostics_merge(outer: cd, inner: d)
+  match normalize_sugar_key_optional(folded: folded) {
+    Present { value: key } =>
+      match sugar_rule_for_key(key: key) {
+        Present { value: rule } =>
+          match apply_sugar(rule: rule, n: n, folded: folded) {
+            Rejected { diagnostics: r } =>
+              Rejected {
+                diagnostics: rejected_with_pending(pending: cd, rejected: r)
+              }
+            Accepted { value: v, diagnostics: d } =>
+              Accepted {
+                value: v,
+                diagnostics: diagnostics_merge(outer: cd, inner: d)
+              }
           }
+        Absent =>
+          Accepted { value: folded, diagnostics: cd }
       }
     Absent =>
       Accepted { value: folded, diagnostics: cd }
@@ -136,11 +119,7 @@ fn normalize_node(n: Node) -> Outcome<Node> {
   }) {
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
     Accepted { value: folded, diagnostics: cd } =>
-      match normalize_production_coproduct_fold(n: n, folded: folded, cd: cd) {
-        Rejected { diagnostics: r } => Rejected { diagnostics: r }
-        Accepted { value: after_prod, diagnostics: cd1 } =>
-          normalize_sugar_finish(n: n, folded: after_prod, cd: cd1)
-      }
+      normalize_sugar_finish(n: n, folded: folded, cd: cd)
   }
 }
 
diff --git a/src/v2/compiler/fold_lowering.dag b/src/v2/compiler/fold_lowering.dag
index 2f460be862b..5086437f040 100644
--- a/src/v2/compiler/fold_lowering.dag
+++ b/src/v2/compiler/fold_lowering.dag
@@ -48,6 +48,10 @@ fn fold_call_head_symbol(fold_call: Node) -> Optional<Symbol> {
   }
 }
 
+fn fold_family_head(sym: Symbol) -> Bool {
+  (sym == ^fold) || (sym == ^fold_list) || (sym == ^fold_list_right) || (sym == ^fold_node)
+}
+
 fn fold_call_step_fn(fold_call: Node) -> Optional<Node> {
   match parse_subtree_find_production_captured(root: fold_call, emitted: ^dag_surface_fn_literal) {
     ParseSubtreeFound { captured: fn_literal } => Present { value: fn_literal }
@@ -55,16 +59,40 @@ fn fold_call_step_fn(fold_call: Node) -> Optional<Node> {
   }
 }
 
-fn fold_call_iteration_body(fold_call: Node) -> Optional<Node> {
-  match fold_call_step_fn(fold_call: fold_call) {
+fn step_fn_iteration_body(fn_literal: Node) -> Optional<Node> {
+  match parse_subtree_find_production_captured(
+    root: fn_literal,
+    emitted: ^dag_surface_fn_body
+  ) {
+    ParseSubtreeAbsent => Absent
+    ParseSubtreeFound { captured: body } => Present { value: body }
+  }
+}
+
+fn fold_seq_child(node: Node, name: Symbol) -> Optional<Node> {
+  match find_named_child(root: node, name: name) {
+    Accepted { value: child, diagnostics: _ } => Present { value: child }
+    Rejected { diagnostics: _ } => Absent
+  }
+}
+
+data step_fn_carrier_binder_note: String = "The step fn's FIRST param is the fold's accumulator binder (fn(acc, item) { .. }). fn_literal params are untyped lexeme-stamped idents (dag_grammar_untyped_params_helper = comma_list(terminal_lexeme(ident))), so the binder NAME is the captured atom's identity. Navigation follows the fn_literal grammar expression Seq(kw_fn, Seq(lparen, Seq(Optional(params), ..))): right, right, left lands on the params capture (Optional-absent = empty Conj -> Absent), whose comma_list capture is Conj[left -> first item]. A step fn with no readable first param cannot be a fold step: the caller refuses ^fold_lowering_shape_invalid, never fabricates a carrier."
+
+fn step_fn_carrier_binder_symbol(fn_literal: Node) -> Optional<Symbol> {
+  match fold_seq_child(node: fn_literal, name: ^grammar_sequence_right_node_projection) {
     Absent => Absent
-    Present { value: fn_literal } =>
-      match parse_subtree_find_production_captured(
-        root: fn_literal,
-        emitted: ^dag_surface_fn_body
-      ) {
-        ParseSubtreeAbsent => Absent
-        ParseSubtreeFound { captured: body } => Present { value: body }
+    Present { value: after_kw_fn } =>
+      match fold_seq_child(node: after_kw_fn, name: ^grammar_sequence_right_node_projection) {
+        Absent => Absent
+        Present { value: after_lparen } =>
+          match fold_seq_child(node: after_lparen, name: ^grammar_sequence_left_node_projection) {
+            Absent => Absent
+            Present { value: params } =>
+              match fold_seq_child(node: params, name: ^grammar_sequence_left_node_projection) {
+                Absent => Absent
+                Present { value: first_param } => node_atom_identity_optional(node: first_param)
+              }
+          }
       }
   }
 }
@@ -85,12 +113,20 @@ fn fold_lowering_shape_invalid_diagnostic(n: Node) -> Diagnostic {
   }
 }
 
-fn fold_call_seam_loop(body: Node) -> Node {
+fn fold_carrier_binder_atom(binder: Symbol) -> Node {
+  node_synthetic(
+    kind: TypeNode { connective: Atom { identity: binder } },
+    children: []
+  )
+}
+
+fn fold_call_seam_loop(body: Node, carrier: Symbol) -> Node {
   node_synthetic(
     kind: ComputationNode { behavior: Loop },
     children: [
       Edge { label: Positional, target: body },
-      Edge { label: Named { name: ^loop_bound_edge }, target: fold_iteration_measure_atom() }
+      Edge { label: Named { name: ^loop_bound_edge }, target: fold_iteration_measure_atom() },
+      Edge { label: Named { name: ^loop_carrier_edge }, target: fold_carrier_binder_atom(binder: carrier) }
     ]
   )
 }
@@ -100,12 +136,22 @@ fn fold_call_to_loop(fold_call: Node) -> Outcome<Node> {
     Absent =>
       outcome_rejected(d: fold_lowering_not_a_fold_call_diagnostic(n: fold_call))
     Present { value: head } =>
-      if head == ^fold {
-        match fold_call_iteration_body(fold_call: fold_call) {
+      if fold_family_head(sym: head) {
+        match fold_call_step_fn(fold_call: fold_call) {
           Absent =>
             outcome_rejected(d: fold_lowering_shape_invalid_diagnostic(n: fold_call))
-          Present { value: body } =>
-            outcome_accepted(value: fold_call_seam_loop(body: body))
+          Present { value: fn_literal } =>
+            match step_fn_iteration_body(fn_literal: fn_literal) {
+              Absent =>
+                outcome_rejected(d: fold_lowering_shape_invalid_diagnostic(n: fold_call))
+              Present { value: body } =>
+                match step_fn_carrier_binder_symbol(fn_literal: fn_literal) {
+                  Absent =>
+                    outcome_rejected(d: fold_lowering_shape_invalid_diagnostic(n: fold_call))
+                  Present { value: carrier } =>
+                    outcome_accepted(value: fold_call_seam_loop(body: body, carrier: carrier))
+                }
+            }
         }
       } else {
         outcome_rejected(d: fold_lowering_not_a_fold_call_diagnostic(n: fold_call))
diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag
index ea180e8b612..03afa8c9a60 100644
--- a/src/v2/extdeps/languages/dag.dag
+++ b/src/v2/extdeps/languages/dag.dag
@@ -2108,7 +2108,7 @@ fn dag_grammar_let_expr() -> GrammarExpr {
   dag_grammar_sequence(
     left: dag_grammar_terminal(token_class: ^dag_token_kw_let),
     right: dag_grammar_sequence(
-      left: dag_grammar_terminal(token_class: ^dag_token_ident),
+      left: dag_grammar_binding_name_terminal(),
       right: dag_grammar_sequence(
         left: dag_grammar_terminal(token_class: ^dag_token_eq),
         right: dag_grammar_nonterminal(production: ^dag_production_expr)
diff --git a/src/v2/lens/complexity_accumulator_copy.dag b/src/v2/lens/complexity_accumulator_copy.dag
index ed68cb9e2d6..259506da624 100644
--- a/src/v2/lens/complexity_accumulator_copy.dag
+++ b/src/v2/lens/complexity_accumulator_copy.dag
@@ -82,6 +82,56 @@ fn any_port_carries_carrier(ports: List<PortReading>, carriers: List<Symbol>) ->
   })
 }
 
+type LetBindingFact
+  = BindsFresh
+  | BindsComputed
+
+type LetBinding {
+  name: Symbol
+  fact: LetBindingFact
+}
+
+data let_binding_note: String = "The within-body definition closure (Stage A: def edges decide aliasing). A let binder whose RHS closes to a CARRIER joins the carriers list at bind time - transitive closure by construction, so `let g = acc  let h = g` proves h - and needs no carrier here. BindsFresh (RHS a pure literal) and BindsComputed (RHS a computed expression) substitute the port reading via resolve_port_reading BEFORE classification, so classify_call and the copied-port lattice stay untouched. A binder whose RHS is a bare name that closes to NOTHING (unbound in scope) records NO binding: its uses still refuse ^copied_port_name_may_alias - the closure only ever DECIDES, never defaults clean. Reader today: the analyze traversal's let-spine arm over surface captures (binding-name lexeme stamping, dag_grammar_let_expr); repoints to Bind definition edges when stmt-chain lowering lands, deleting the surface read."
+
+fn no_let_binding_fact() -> Optional<LetBindingFact> {
+  Absent
+}
+
+fn some_let_binding_fact(fact: LetBindingFact) -> Optional<LetBindingFact> {
+  Present { value: fact }
+}
+
+fn let_binding_fact_for(name: Symbol, bindings: List<LetBinding>) -> Optional<LetBindingFact> {
+  fold(bindings, init: no_let_binding_fact(), f: fn(acc, b) {
+    match acc {
+      Present { value: _ } => acc
+      Absent =>
+        if b.name == name {
+          some_let_binding_fact(fact: b.fact)
+        } else {
+          no_let_binding_fact()
+        }
+    }
+  })
+}
+
+fn resolve_port_reading(reading: PortReading, bindings: List<LetBinding>) -> PortReading {
+  match reading {
+    PortBareName { name: n } =>
+      match let_binding_fact_for(name: n, bindings: bindings) {
+        Present { value: fact } =>
+          match fact {
+            BindsFresh => PortPureLiteral
+            BindsComputed => PortComputedExpression
+          }
+        Absent => reading
+      }
+    PortPureLiteral => reading
+    PortComputedExpression => reading
+    PortMissing => reading
+  }
+}
+
 fn classify_copied_port(at: Node, reading: PortReading, carriers: List<Symbol>) -> Optional<Finding> {
   match reading {
     PortBareName { name: n } =>
diff --git a/src/v2/lens/complexity_accumulator_copy/analyze.dag b/src/v2/lens/complexity_accumulator_copy/analyze.dag
index d5449fb5f85..18c0080b017 100644
--- a/src/v2/lens/complexity_accumulator_copy/analyze.dag
+++ b/src/v2/lens/complexity_accumulator_copy/analyze.dag
@@ -1,7 +1,11 @@
 module v2.lens.complexity_accumulator_copy.analyze
 
 import v2.lens.complexity_accumulator_copy {
+  BindsComputed,
+  BindsFresh,
   Finding,
+  LetBinding,
+  LetBindingFact,
   PortBareName,
   PortComputedExpression,
   PortMissing,
@@ -10,7 +14,10 @@ import v2.lens.complexity_accumulator_copy {
   Poly2Suspect,
   Unclassifiable,
   any_port_carries_carrier,
-  classify_call
+  classify_call,
+  let_binding_fact_for,
+  resolve_port_reading,
+  symbol_in
 }
 import v2.extdeps.languages.dag {
   ParseSubtreeAbsent,
@@ -21,13 +28,14 @@ import v2.extdeps.languages.dag {
   parse_subtree_find_production_captured
 }
 import std.algebra { Cons, Empty }
+import v2.compiler.fold_lowering { fold_call_to_loop, fold_family_head }
 import v2.std.algebra { list_append, list_map, list_reverse }
 import v2.std.collection { Absent, List, Optional, Present }
 import v2.std.diagnostic { Accepted, Rejected }
 import v2.std.grammar { node_atom_identity_optional }
 import v2.std.integer { Int }
 import v2.std.logic { Bool }
-import v2.std.node { Edge, Named, Node, Positional, Symbol }
+import v2.std.node { Edge, Named, Node, Positional, Symbol, loop_carrier_binder_target }
 import v2.std.node_query { find_named_child }
 
 fn named_child_optional(cap: Node, name: Symbol) -> Optional<Node> {
@@ -149,62 +157,207 @@ fn call_port_readings(call_capture: Node) -> List<PortReading> {
   )
 }
 
-fn is_fold_family_head(sym: Symbol) -> Bool {
-  (sym == ^fold) || (sym == ^fold_list) || (sym == ^fold_list_right) || (sym == ^fold_node)
+data fold_family_carrier_note: String = "The carrier read is a named-edge lookup on the LOWERED seam Loop (FLAG F): the located fold call desugars via v2.compiler.fold_lowering.fold_call_to_loop and the accumulator binder is the ^loop_carrier_edge target's atom identity - the lens never re-navigates the surface fn_literal capture (that read has exactly one authority, the lowering). A call the seam refuses (named step fn, no fn literal) yields Absent and the ^fold_accumulator_unread refusal stands: the binder is a callee-resolution fact (Stage B), not a within-body fact, and the lens never fabricates a carrier."
+
+fn fold_family_carrier(call_capture: Node) -> Optional<Symbol> {
+  match fold_call_to_loop(fold_call: call_capture) {
+    Rejected { diagnostics: _ } => Absent
+    Accepted { value: seam_loop, diagnostics: _ } =>
+      match loop_carrier_binder_target(children: seam_loop.children) {
+        Found { target: binder } => node_atom_identity_optional(node: binder)
+        Ambiguous => Absent
+        Absent => Absent
+      }
+  }
+}
+
+fn append_findings(fresh: List<Finding>, acc: List<Finding>) -> List<Finding> {
+  list_append(left: fresh, right: acc)
+}
+
+fn let_expr_capture(node: Node) -> Optional<Node> {
+  match parse_production_emitted_identity_optional(node: node) {
+    Present { value: id } =>
+      if id == ^dag_surface_let_expr {
+        parse_production_captured_child_optional(node: node)
+      } else {
+        match parse_production_captured_child_optional(node: node) {
+          Present { value: inner } => let_expr_capture(node: inner)
+          Absent => Absent
+        }
+      }
+    Absent => Absent
+  }
+}
+
+type LetSpine {
+  let_wrapper: Node
+  let_capture: Node
+  rest: Node
 }
 
-fn step_fn_first_param(fn_literal: Node) -> Optional<Symbol> {
-  match sequence_right_node(cap: fn_literal) {
+fn let_spine_of(node: Node) -> Optional<LetSpine> {
+  match sequence_left_node(cap: node) {
     Absent => Absent
-    Present { value: after_kw_fn } =>
-      match sequence_right_node(cap: after_kw_fn) {
+    Present { value: left } =>
+      match let_expr_capture(node: left) {
         Absent => Absent
-        Present { value: after_lparen } =>
-          match sequence_left_node(cap: after_lparen) {
+        Present { value: cap } =>
+          match sequence_right_node(cap: node) {
             Absent => Absent
-            Present { value: params } => sequence_left_symbol(cap: params)
+            Present { value: rest } =>
+              Present { value: LetSpine { let_wrapper: left, let_capture: cap, rest: rest } }
           }
       }
   }
 }
 
-fn fold_family_carrier(call_capture: Node) -> Optional<Symbol> {
-  match find_capture(root: call_capture, emitted: ^dag_surface_fn_literal) {
+fn let_binder_symbol(let_capture: Node) -> Optional<Symbol> {
+  match sequence_right_node(cap: let_capture) {
     Absent => Absent
-    Present { value: fn_literal } => step_fn_first_param(fn_literal: fn_literal)
+    Present { value: after_kw } =>
+      match sequence_left_node(cap: after_kw) {
+        Absent => Absent
+        Present { value: binder } => node_atom_identity_optional(node: binder)
+      }
   }
 }
 
-fn append_findings(fresh: List<Finding>, acc: List<Finding>) -> List<Finding> {
-  list_append(left: fresh, right: acc)
+fn let_rhs_node(let_capture: Node) -> Optional<Node> {
+  match sequence_right_node(cap: let_capture) {
+    Absent => Absent
+    Present { value: after_kw } =>
+      match sequence_right_node(cap: after_kw) {
+        Absent => Absent
+        Present { value: after_binder } => sequence_right_node(cap: after_binder)
+      }
+  }
+}
+
+type LetResolution
+  = LetJoinsCarriers { name: Symbol }
+  | LetBindsFact { binding: LetBinding }
+  | LetUndecided
+
+fn let_resolution(
+  let_capture: Node,
+  carriers: List<Symbol>,
+  bindings: List<LetBinding>
+) -> LetResolution {
+  match let_binder_symbol(let_capture: let_capture) {
+    Absent => LetUndecided
+    Present { value: binder } =>
+      match let_rhs_node(let_capture: let_capture) {
+        Absent => LetUndecided
+        Present { value: rhs } =>
+          let idents = count_value_identifiers(n: rhs)
+          if idents == 0 {
+            LetBindsFact { binding: LetBinding { name: binder, fact: BindsFresh } }
+          } else {
+            if idents == 1 {
+              match arg_value_symbol(arg_capture: rhs) {
+                Absent =>
+                  LetBindsFact { binding: LetBinding { name: binder, fact: BindsComputed } }
+                Present { value: s } =>
+                  if symbol_in(needle: s, xs: carriers) {
+                    LetJoinsCarriers { name: binder }
+                  } else {
+                    match let_binding_fact_for(name: s, bindings: bindings) {
+                      Present { value: fact } =>
+                        LetBindsFact { binding: LetBinding { name: binder, fact: fact } }
+                      Absent => LetUndecided
+                    }
+                  }
+              }
+            } else {
+              LetBindsFact { binding: LetBinding { name: binder, fact: BindsComputed } }
+            }
+          }
+      }
+  }
 }
 
 fn analyze_children(
   n: Node,
   carriers: List<Symbol>,
+  bindings: List<LetBinding>,
   iterating: Bool,
   here: List<Finding>
 ) -> List<Finding> {
   fold(n.children, init: here, f: fn(acc, e) {
     append_findings(
-      fresh: analyze(node: e.target, carriers: carriers, iterating: iterating),
+      fresh: analyze(node: e.target, carriers: carriers, bindings: bindings, iterating: iterating),
       acc: acc
     )
   })
 }
 
-fn analyze(node: Node, carriers: List<Symbol>, iterating: Bool) -> List<Finding> {
+fn analyze_let_spine(
+  spine: LetSpine,
+  carriers: List<Symbol>,
+  bindings: List<LetBinding>,
+  iterating: Bool
+) -> List<Finding> {
+  let left_findings = analyze(
+    node: spine.let_wrapper, carriers: carriers, bindings: bindings, iterating: iterating
+  )
+  match let_resolution(let_capture: spine.let_capture, carriers: carriers, bindings: bindings) {
+    LetJoinsCarriers { name: nm } =>
+      append_findings(
+        fresh: analyze(
+          node: spine.rest,
+          carriers: Cons { head: nm, tail: carriers },
+          bindings: bindings,
+          iterating: iterating
+        ),
+        acc: left_findings
+      )
+    LetBindsFact { binding: b } =>
+      append_findings(
+        fresh: analyze(
+          node: spine.rest,
+          carriers: carriers,
+          bindings: Cons { head: b, tail: bindings },
+          iterating: iterating
+        ),
+        acc: left_findings
+      )
+    LetUndecided =>
+      append_findings(
+        fresh: analyze(
+          node: spine.rest, carriers: carriers, bindings: bindings, iterating: iterating
+        ),
+        acc: left_findings
+      )
+  }
+}
+
+fn resolved_port_readings(call_capture: Node, bindings: List<LetBinding>) -> List<PortReading> {
+  list_map(
+    xs: call_port_readings(call_capture: call_capture),
+    f: fn(reading) { resolve_port_reading(reading: reading, bindings: bindings) }
+  )
+}
+
+fn analyze(node: Node, carriers: List<Symbol>, bindings: List<LetBinding>, iterating: Bool) -> List<Finding> {
   match primary_expr_capture(node: node) {
-    Absent => analyze_children(n: node, carriers: carriers, iterating: iterating, here: Empty)
+    Absent =>
+      match let_spine_of(node: node) {
+        Present { value: spine } =>
+          analyze_let_spine(spine: spine, carriers: carriers, bindings: bindings, iterating: iterating)
+        Absent =>
+          analyze_children(n: node, carriers: carriers, bindings: bindings, iterating: iterating, here: Empty)
+      }
     Present { value: cap } =>
       match sequence_left_symbol(cap: cap) {
         Present { value: head } =>
-          if is_fold_family_head(sym: head) {
+          if fold_family_head(sym: head) {
             match fold_family_carrier(call_capture: cap) {
               Present { value: carrier } =>
                 analyze_children(
                   n: node,
                   carriers: Cons { head: carrier, tail: carriers },
+                  bindings: bindings,
                   iterating: true,
                   here: Empty
                 )
@@ -212,6 +365,7 @@ fn analyze(node: Node, carriers: List<Symbol>, iterating: Bool) -> List<Finding>
                 analyze_children(
                   n: node,
                   carriers: carriers,
+                  bindings: bindings,
                   iterating: true,
                   here: Cons {
                     head: Unclassifiable { at: node, cause: ^fold_accumulator_unread },
@@ -224,7 +378,7 @@ fn analyze(node: Node, carriers: List<Symbol>, iterating: Bool) -> List<Finding>
               match classify_call(
                 at: node,
                 combiner: head,
-                ports: call_port_readings(call_capture: cap),
+                ports: resolved_port_readings(call_capture: cap, bindings: bindings),
                 carriers: carriers
               ) {
                 Present { value: f } => Cons { head: f, tail: Empty }
@@ -233,12 +387,12 @@ fn analyze(node: Node, carriers: List<Symbol>, iterating: Bool) -> List<Finding>
             } else {
               Empty
             }
-            analyze_children(n: node, carriers: carriers, iterating: iterating, here: here)
+            analyze_children(n: node, carriers: carriers, bindings: bindings, iterating: iterating, here: here)
           }
         Absent =>
           let here = if iterating {
             if any_port_carries_carrier(
-              ports: call_port_readings(call_capture: cap),
+              ports: resolved_port_readings(call_capture: cap, bindings: bindings),
               carriers: carriers
             ) {
               Cons {
@@ -251,7 +405,7 @@ fn analyze(node: Node, carriers: List<Symbol>, iterating: Bool) -> List<Finding>
           } else {
             Empty
           }
-          analyze_children(n: node, carriers: carriers, iterating: iterating, here: here)
+          analyze_children(n: node, carriers: carriers, bindings: bindings, iterating: iterating, here: here)
       }
   }
 }
@@ -269,7 +423,7 @@ fn count_fold_sites(n: Node, bound_only: Bool) -> Int {
       match sequence_left_symbol(cap: cap) {
         Absent => 0
         Present { value: head } =>
-          if is_fold_family_head(sym: head) {
+          if fold_family_head(sym: head) {
             if bound_only {
               match fold_family_carrier(call_capture: cap) {
                 Present { value: _ } => 1
@@ -289,7 +443,7 @@ fn count_fold_sites(n: Node, bound_only: Bool) -> Int {
 }
 
 fn accumulator_copy_findings(root: Node) -> List<Finding> {
-  analyze(node: root, carriers: Empty, iterating: false)
+  analyze(node: root, carriers: Empty, bindings: Empty, iterating: false)
 }
 
 fn accumulator_copy_report(root: Node) -> AccumulatorCopyReport {
diff --git a/src/v2/std/compilers/sugar.dag b/src/v2/std/compilers/sugar.dag
index cc9316fe5b5..c738e3f459f 100644
--- a/src/v2/std/compilers/sugar.dag
+++ b/src/v2/std/compilers/sugar.dag
@@ -40,35 +40,45 @@ import v2.std.node {
 type SugarLowering
   = SugarRewriteConnective { connective: Connective, edges: EdgeDiscipline }
   | SugarUnwrapPositionalChild {}
+  | SugarFoldCoproductPipeChain {}
+
+type SugarKey
+  = SurfaceAtomKey { atom: Symbol }
+  | ProductionIdentityKey { identity: Symbol }
 
 type SugarRule {
-  surface_atom: Symbol
+  key: SugarKey
   lowering: SugarLowering
 }
 
 data sugar_rule_service: SugarRule = SugarRule {
-  surface_atom: ^dag_c3_surface_sugar_service,
+  key: SurfaceAtomKey { atom: ^dag_c3_surface_sugar_service },
   lowering: SugarRewriteConnective { connective: Conj, edges: LabeledEdges }
 }
 data sugar_rule_fn: SugarRule = SugarRule {
-  surface_atom: ^dag_c3_surface_sugar_fn,
+  key: SurfaceAtomKey { atom: ^dag_c3_surface_sugar_fn },
   lowering: SugarRewriteConnective { connective: Arrow, edges: PositionalEdges }
 }
 data sugar_rule_type: SugarRule = SugarRule {
-  surface_atom: ^dag_c3_surface_sugar_type,
+  key: SurfaceAtomKey { atom: ^dag_c3_surface_sugar_type },
   lowering: SugarUnwrapPositionalChild {}
 }
 data sugar_rule_operation: SugarRule = SugarRule {
-  surface_atom: ^dag_c3_surface_sugar_operation,
+  key: SurfaceAtomKey { atom: ^dag_c3_surface_sugar_operation },
   lowering: SugarRewriteConnective { connective: Arrow, edges: PositionalEdges }
 }
+data sugar_rule_type_alias_rhs: SugarRule = SugarRule {
+  key: ProductionIdentityKey { identity: ^dag_surface_type_alias_rhs },
+  lowering: SugarFoldCoproductPipeChain {}
+}
 
 fn sugar_rules() -> List<SugarRule> {
   [
     sugar_rule_service,
     sugar_rule_fn,
     sugar_rule_type,
-    sugar_rule_operation
+    sugar_rule_operation,
+    sugar_rule_type_alias_rhs
   ]
 }
 
@@ -76,26 +86,33 @@ fn no_sugar_rule() -> SugarRule? {
   optional_absent()
 }
 
-fn sugar_rule_for_atom(id: Symbol, rule: SugarRule) -> SugarRule? {
-  if id == rule.surface_atom {
-    optional_present(value: rule)
-  } else {
-    optional_absent()
+fn sugar_key_matches(key: SugarKey, rule_key: SugarKey) -> Bool {
+  match key {
+    SurfaceAtomKey { atom: a } =>
+      match rule_key {
+        SurfaceAtomKey { atom: b } => a == b
+        ProductionIdentityKey { identity: _ } => false
+      }
+    ProductionIdentityKey { identity: i } =>
+      match rule_key {
+        SurfaceAtomKey { atom: _ } => false
+        ProductionIdentityKey { identity: j } => i == j
+      }
   }
 }
 
-fn classify_sugar(n: Node) -> SugarRule? {
-  match n.kind {
-    TypeNode { connective: Atom { identity: id } } =>
-      fold(sugar_rules(), init: no_sugar_rule(), f: fn(acc, rule) {
-        match acc {
-          Present { value: _ } => acc
-          Absent => sugar_rule_for_atom(id: id, rule: rule)
+fn sugar_rule_for_key(key: SugarKey) -> SugarRule? {
+  fold(sugar_rules(), init: no_sugar_rule(), f: fn(acc, rule) {
+    match acc {
+      Present { value: _ } => acc
+      Absent =>
+        if sugar_key_matches(key: key, rule_key: rule.key) {
+          optional_present(value: rule)
+        } else {
+          optional_absent()
         }
-      })
-    TypeNode { connective: _ } => no_sugar_rule()
-    ComputationNode { behavior: _ } => no_sugar_rule()
-  }
+    }
+  })
 }
 
 fn sugar_malformed_diagnostic(n: Node) -> Diagnostic {
@@ -263,23 +280,39 @@ fn sugar_fold_coproduct_pipe_chain(captured: Node, shell: Node) -> Outcome<Node>
   }
 }
 
-fn apply_sugar(rule: SugarRule, n: Node, children: List<Edge>) -> Outcome<Node> {
+fn apply_sugar(rule: SugarRule, n: Node, folded: Node) -> Outcome<Node> {
   match rule.lowering {
     SugarRewriteConnective { connective: connective, edges: discipline } =>
-      if edges_conform(children: children, d: discipline) {
+      if edges_conform(children: folded.children, d: discipline) {
         Accepted {
-          value: sugar_type_node(connective: connective, children: children, n: n),
+          value: sugar_type_node(connective: connective, children: folded.children, n: n),
           diagnostics: None
         }
       } else {
         Rejected { diagnostics: diagnostics_singleton(d: sugar_malformed_diagnostic(n: n)) }
       }
     SugarUnwrapPositionalChild {} =>
-      match sugar_positional_unwrap_child(children: children) {
+      match sugar_positional_unwrap_child(children: folded.children) {
         Present { value: child } =>
           Accepted { value: child, diagnostics: None }
         Absent =>
           Rejected { diagnostics: diagnostics_singleton(d: sugar_malformed_diagnostic(n: n)) }
       }
+    SugarFoldCoproductPipeChain {} =>
+      match sugar_named_child_optional(root: folded, name: ^grammar_production_captured_node_projection) {
+        Present { value: captured } =>
+          match sugar_fold_coproduct_pipe_chain(captured: captured, shell: n) {
+            Rejected { diagnostics: r } => Rejected { diagnostics: r }
+            Accepted { value: result, diagnostics: d } =>
+              match result.kind {
+                TypeNode { connective: Disj } =>
+                  Accepted { value: result, diagnostics: d }
+                _ =>
+                  Accepted { value: folded, diagnostics: None }
+              }
+          }
+        Absent =>
+          Accepted { value: folded, diagnostics: None }
+      }
   }
 }
diff --git a/src/v2/std/node.dag b/src/v2/std/node.dag
index e099386b152..d62bf7cc072 100644
--- a/src/v2/std/node.dag
+++ b/src/v2/std/node.dag
@@ -271,14 +271,16 @@ fn loop_body_edges_conform(children: List<Edge>) -> Bool {
   fold(children, init: true, f: fn(acc, e) {
     match e.label {
       Positional => acc
-      Named { name: sym } => acc && (sym == ^loop_bound_edge)
+      Named { name: sym } => acc && ((sym == ^loop_bound_edge) || (sym == ^loop_carrier_edge))
     }
   })
 }
 
 fn loop_behavior_edges_conform(children: List<Edge>) -> Bool {
   let bound_edges = name_occurrences(name: ^loop_bound_edge, children: children)
+  let carrier_edges = name_occurrences(name: ^loop_carrier_edge, children: children)
   (bound_edges == 1)
+  && (carrier_edges <= 1)
   && loop_body_edges_conform(children: children)
   && (loop_positional_child_count(children: children) >= 1)
 }
@@ -371,12 +373,16 @@ fn loop_bound_measure_target(children: List<Edge>) -> NamedEdgeTargetLookup {
   named_edge_target_lookup(children: children, name: ^loop_bound_edge)
 }
 
+fn loop_carrier_binder_target(children: List<Edge>) -> NamedEdgeTargetLookup {
+  named_edge_target_lookup(children: children, name: ^loop_carrier_edge)
+}
+
 fn loop_edge_contributes_to_iteration_fold(parent: Node, e: Edge) -> Bool {
   match parent.kind {
     ComputationNode { behavior: Loop } =>
       match e.label {
         Positional => true
-        Named { name: sym } => sym != ^loop_bound_edge
+        Named { name: sym } => (sym != ^loop_bound_edge) && (sym != ^loop_carrier_edge)
       }
     _ =>
       match e.label {
diff --git a/src/v2/test/claim/complexity/accumulator_copy_fold_analysis_test.dag b/src/v2/test/claim/complexity/accumulator_copy_fold_analysis_test.dag
index 2d428b0b5f9..521eafd21c2 100644
--- a/src/v2/test/claim/complexity/accumulator_copy_fold_analysis_test.dag
+++ b/src/v2/test/claim/complexity/accumulator_copy_fold_analysis_test.dag
@@ -37,6 +37,12 @@ data out_of_iteration_snippet: String = "module once\n\nfn f(xs: List<Int>, ys:
 
 data named_step_snippet: String = "module namedstep\n\nfn f(xs: List<Int>) -> Int {\n  fold(xs, init: 0, f: step)\n}\n"
 
+data let_unknown_alias_snippet: String = "module unknownalias\n\nfn f(xs: List<Int>) -> Int {\n  fold(xs, init: 0, f: fn(acc, x) {\n    let grown = mystery\n    list_append(left: grown, right: x)\n  })\n}\n"
+
+data let_fresh_snippet: String = "module freshlet\n\nfn f(xs: List<Int>) -> Int {\n  fold(xs, init: 0, f: fn(acc, x) {\n    let seed = 0\n    list_append(left: seed, right: x)\n  })\n}\n"
+
+data let_transitive_alias_snippet: String = "module transalias\n\nfn f(xs: List<Int>) -> Int {\n  fold(xs, init: 0, f: fn(acc, x) {\n    let g = acc\n    let h = g\n    list_append(left: h, right: x)\n  })\n}\n"
+
 fn ingest(source_text: String, file: Symbol) -> Optional<Node> {
   let lm = dag_language_model()
   match tokenize(text: source_text, file: file, rules: lm.lex) {
@@ -93,11 +99,40 @@ test fn noncarrier_name_in_copied_port_refuses_not_clean() -> Bool {
   }
 }
 
-test fn let_alias_refuses_not_clean() -> Bool {
+test fn let_alias_is_proven_suspect() -> Bool {
   match findings_of(source_text: let_alias_snippet, file: ^alias_file) {
     Absent => false
     Present { value: fs } =>
-      findings_have_refusal_cause(fs: fs, cause: ^copied_port_name_may_alias)
+      findings_have_suspect(fs: fs)
+      && !findings_have_refusal_cause(fs: fs, cause: ^copied_port_name_may_alias)
+  }
+}
+
+test fn let_transitive_alias_is_proven_suspect() -> Bool {
+  match findings_of(source_text: let_transitive_alias_snippet, file: ^transalias_file) {
+    Absent => false
+    Present { value: fs } =>
+      findings_have_suspect(fs: fs)
+      && !findings_have_refusal_cause(fs: fs, cause: ^copied_port_name_may_alias)
+  }
+}
+
+test fn let_fresh_binding_is_provably_clean() -> Bool {
+  match findings_of(source_text: let_fresh_snippet, file: ^freshlet_file) {
+    Absent => false
+    Present { value: fs } => is_empty_findings(fs: fs)
+  }
+}
+
+test fn let_unknown_alias_still_refuses_may_alias() -> Bool {
+  match findings_of(source_text: let_unknown_alias_snippet, file: ^unknownalias_file) {
+    Absent => false
+    Present { value: fs } =>
+      if findings_have_suspect(fs: fs) {
+        false
+      } else {
+        findings_have_refusal_cause(fs: fs, cause: ^copied_port_name_may_alias)
+      }
   }
 }
 
diff --git a/src/v2/test/claim/complexity/fold_lowering_test.dag b/src/v2/test/claim/complexity/fold_lowering_test.dag
index c83dfb83294..5d7de5d6f44 100644
--- a/src/v2/test/claim/complexity/fold_lowering_test.dag
+++ b/src/v2/test/claim/complexity/fold_lowering_test.dag
@@ -11,6 +11,7 @@ import v2.extdeps.languages.dag {
   dag_language_model,
   parse_subtree_find_production_captured
 }
+import v2.std.algebra { list_snoc_item }
 import v2.std.cardinality {
   Bounded,
   Multiplicity,
@@ -22,7 +23,15 @@ import v2.std.collection { Absent, List, Optional, Present }
 import v2.std.diagnostic { Accepted, Outcome, Rejected }
 import v2.std.grammar { node_atom_identity_optional }
 import v2.std.logic { Bool }
-import v2.std.node { Node, Symbol }
+import v2.std.node {
+  Edge,
+  Named,
+  Node,
+  Symbol,
+  loop_carrier_binder_target,
+  node_rebuild,
+  well_formed
+}
 import v2.std.text { String }
 
 data fold_lowering_witness_note: String = "Grounds the un-forked fold->Loop desugaring (v2.compiler.fold_lowering) by execution on REAL source, end-to-end through the census ingest (tokenize -> parse_module -> normalize). A surface fold parses as an ordinary call; after the StampLexeme grammar fix its callee carries its NAME (^fold) as an atom identity and the collection likewise (^xs) — the survival sub-facts are the RED control that a grammar regression (head stamped as the token class) breaks. The located fold-call subtree (the first primary_expr capture — the outermost fn-body expression) desugars to the canonical seam Loop, and the kept loop_multiplicity derives PROVEN termination from the fold-iteration measure — the same real derivation the foundation's loop witnesses use, now reached from a real parsed fold call rather than a hand-built loop. Two fail-closed red controls: a non-fold call (head ^g) refuses (never desugars a foreign call), and a fold call carrying no fn-literal iteration body refuses (never fabricates a loop). This is the desugaring the whole-tree body producer will run on every located fold call once corpus walking is affordable; the shape it emits is exactly what the accumulator-copy rule (M3) will key on."
@@ -128,6 +137,52 @@ test fn fold_call_lowers_to_terminating_loop() -> Bool {
   }
 }
 
+fn lowered_fixture_loop() -> Optional<Node> {
+  match ingest_and_locate(source_text: fold_snippet, file: ^fold_probe_file) {
+    Absent => Absent
+    Present { value: call } =>
+      match fold_call_to_loop(fold_call: call) {
+        Accepted { value: loop, diagnostics: _ } => Present { value: loop }
+        Rejected { diagnostics: _ } => Absent
+      }
+  }
+}
+
+test fn lowered_loop_binds_carrier_binder() -> Bool {
+  match lowered_fixture_loop() {
+    Absent => false
+    Present { value: loop } =>
+      match loop_carrier_binder_target(children: loop.children) {
+        Found { target: binder } =>
+          match node_atom_identity_optional(node: binder) {
+            Present { value: sym } => sym == ^acc
+            Absent => false
+          }
+        Ambiguous => false
+        Absent => false
+      }
+  }
+}
+
+test fn duplicate_carrier_edge_is_malformed() -> Bool {
+  match lowered_fixture_loop() {
+    Absent => false
+    Present { value: loop } =>
+      match loop_carrier_binder_target(children: loop.children) {
+        Found { target: binder } =>
+          !well_formed(n: node_rebuild(
+            n: loop,
+            children: list_snoc_item(
+              xs: loop.children,
+              item: Edge { label: Named { name: ^loop_carrier_edge }, target: binder }
+            )
+          ))
+        Ambiguous => false
+        Absent => false
+      }
+  }
+}
+
 test fn non_fold_call_refuses() -> Bool {
   match ingest_and_locate(source_text: non_fold_snippet, file: ^g_probe_file) {
     Absent => false