Body-producer Stage A: FLAGs D/E/F signed + within-body fact layer (one sugar table, 3-edge seam Loop, definition closure)

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

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)"),
     ]),
   ]