From 45b4563e70e17243b562f7381236231aed1910db Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:14:27 +0000
Subject: [PATCH 01/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 docs/design-coproduct-arm-reflection.md   | 438 ++++++++++++++++++++++
 src/v2/stage0/src/coproduct_reflection.rs | 273 ++++++++++++++
 src/v2/stage0/src/lib.rs                  |   1 +
 src/v2/stage0/src/v2_interpreter.rs       |  29 ++
 src/v4/std/node.dag                       |  25 ++
 5 files changed, 766 insertions(+)
 create mode 100644 docs/design-coproduct-arm-reflection.md
 create mode 100644 src/v2/stage0/src/coproduct_reflection.rs

diff --git a/docs/design-coproduct-arm-reflection.md b/docs/design-coproduct-arm-reflection.md
new file mode 100644
index 00000000000..448b7ad8287
--- /dev/null
+++ b/docs/design-coproduct-arm-reflection.md
@@ -0,0 +1,438 @@
+# Coproduct-arm reflection — design + ban-lift proposal
+
+> **Status: design (Phase 1 of the R-reflect lane). GATED.**
+> This document is a proposal. No implementation, primitive, or consumer
+> migration lands until it has (a) substrate **DESIGN-SIGN** (snappy-crab-849)
+> and (b) the operator's **BAN-LIFT RULING** (routed via zesty-swift-79). It
+> exists to be reviewed, not to authorize work.
+>
+> **Anchor.** This is the *Track 2 — substrate-derivation* spec for the lens
+> family the dissolve-on-arrival marks cite as `docs/design-dissolution-lens.md
+> L1.1` ("coproduct reflection / variant-enumeration substrate"). That internal
+> doc was removed in the public-visibility flip (#4192); this public design doc
+> is its surviving, scoped successor. Phase 3 re-anchors the marks' citations
+> here.
+>
+> **Cross-refs (live):** INVARIANTS.md P1/P2/P3/P4/P5 and §"Reflection evidence
+> is not structural proof"; MODELING.md M8/M9/M11/M12; THESIS §"Self-inspection",
+> §"Structural decompression"; src/v3/SELF_HOSTING.md §2.3 (language-agnostic
+> core); CODING.md (Rust style for any compiler support).
+
+---
+
+## 0. One-paragraph summary
+
+A **coproduct-arm reflection** primitive enumerates a closed sum type's variant
+arms and projects per-arm keys/labels, so downstream models **derive** variant
+lists, arm-discriminants, and item rosters **from the type** instead of
+hand-mirroring them. Today ~15 `gunbc#4759`-bound mirror marks (plus ~12
+broader-family arm-tables) hand-maintain second copies of facts the declaration
+already states. Reflection makes those mirrors *unrepresentable* (you cannot
+drift from yourself) for structurally-determined facts, and converts the
+genuinely per-arm-semantic consumers into **fail-closed total maps keyed by the
+reflected arm set**. The reflection *mechanism itself* is held honest by one
+tree-wide **by-execution conformance gate** (reflection output == an
+independently-derived arm set), which replaces N hand-mirrors with a single,
+broader, executed check. The ban is lifted **only** for this mechanism, under
+those guarantees.
+
+---
+
+## 1. The problem — hand-rostered / mirror marks
+
+A coproduct is declared once:
+
+```dag
+type Connective = Atom { identity: Symbol } | Conj | Disj | Arrow | Cardinality | Instantiation   // std/node.dag
+```
+
+…and then its arm set is **re-stated by hand** in many places. Grounded census
+(verify line numbers at HEAD; from `main`):
+
+**Core falsifier — 15 `gunbc#4759`-bound mirror mark-lines across 6 files:**
+
+| File | Mark(s) | What it mirrors |
+|---|---|---|
+| `src/v4/std/node.dag` | :46 | `ConnectiveCoproductVariant` enum + `connective_coproduct_variant_keys()` + `behavior_coproduct_variants()` — hand-lists of `Connective`/`Behavior` arms |
+| `src/v4/std/verification.dag` | :93 | `impossible_bug_class_coproduct_variants()` — hand-list of `ImpossibleBugClass` arms |
+| ″ | :134 | `impossible_bug_class_from_diagnostic_reason()` — reason→class bridge |
+| ″ | :195/:197 | `TestClaimCoproductVariant` — key-enum mirror of `TestClaim` arms |
+| ″ | :210/:212 | `ClaimAnchorKey` manual/generated union (anchor split) |
+| ″ | :275 | `test_claim_label()` — hand-enumerated `TestClaim`→label projection |
+| ″ | :287 | `test_claim_coproduct_variant()` — hand-enumerated `TestClaim`→key projection |
+| `src/v4/test/claim/generated/coproduct_exhaustiveness.dag` | :53/:63/:92 | hand-rolled arm-discriminant checks (DiagnosticClaim / GeneratedClaimAnchor / 4-arm `TestClaimCoproductVariant` equality) |
+| `src/v4/test/claim/generated/algebra_law_conformance.dag` | :32 | local nat-expression node shape-tags |
+| `src/v4/lens/coverage.dag` | :947 | impossible-bug reason membership (consumes verification's projection) |
+| `src/v4/test/claim/manual/manual_corpus_roster.dag` | :4 | "item-registry reflection replaces explicit import roster" |
+
+**Broader family (~12, same shape, not #4759-bound):** arm-tables /
+variant-discriminant marks in `lens/coverage`, `lens_cost/*`, `lens_complexity/*`
+(per-arm cost & complexity tables). Surfaced as a Phase-3 consumer cluster;
+lower priority than the core.
+
+**The ban line itself:** `src/v4/test/claim/extdeps/coordination_claims.dag:18`
+— "reflection banned; decl-shape mirrors are 2FA-for-code."
+
+**Why this is debt (live invariants).** Each mirror is a *second authority* for
+a fact the declaration already owns — INVARIANTS P2 "Parallel authority" and
+MODELING M2/M7. Cost-of-change is > 1: adding an arm to `Connective` forces edits
+in `node.dag`, `coverage.dag`, and any roster keyed on it. The marks are valid
+🟡 only because they bind a named dissolution trigger — *this* primitive
+(P5 "Scaffold without dissolution trigger"). `gunbc#4759` is a **closed
+label-hygiene re-anchor, not prior art** — the capability is greenfield.
+
+---
+
+## 2. The ban — read carefully, then steelmanned
+
+`coordination_claims.dag:18` bans reflection because **decl-shape mirrors are
+"2FA-for-code"**: a second, *independently authored* statement of the arm set
+that catches drift. Naively deleting the mirrors and deriving from the
+declaration removes that second factor. The design must not hand-wave this.
+
+The 2FA protects against **two distinct drift classes**, and they have
+*different* answers:
+
+- **(ii) declaration ↔ consumer drift.** A consumer's variant handling silently
+  goes stale when an arm is added (the classic non-exhaustive-handling bug). The
+  mirror catches it because a hand-written exhaustive `match` over the coproduct
+  *fails to compile* until updated — that compile error is the real "second
+  factor."
+- **(i) declaration ↔ mechanism drift (self-hosting).** The deeper concern: the
+  compiler is partly self-hosted (`.dag` → emitted stage0 Rust). If the
+  reflection *mechanism* has a bug — drops an arm, miscounts under a generic
+  instantiation, the lowering is wrong — a consumer relying solely on reflection
+  silently inherits the wrong arm set, and nothing catches it, because the only
+  authority is the broken one. The hand-mirror is an **independent witness** of
+  the same fact, authored by a human reading the declaration; comparing the two
+  catches mechanism bugs.
+
+Both are real. The design answers each — and the answers are *stronger* than the
+mirrors, not weaker.
+
+---
+
+## 3. Where reflection attaches (M9 — DFS the concept DAG)
+
+**No new top-level concept. No substrate extension.** A coproduct is *already*
+a substrate citizen: in `std/node.dag` a sum type is a node with
+`kind: TypeNode { connective: Disj }`, and `connective_edge_discipline(Disj) =
+LabeledEdges` — so **its arms are its named-edge children** (`Edge { label:
+Named { name: armLabel }, target: armPayload }`). Enumerating arms is therefore
+a *structural query over a `Disj` node's edges* — the same shape as the existing
+`named_edge_target_lookup`, `node_subtree_nodes`, `all_edges_named` in
+`std/node.dag`. The v3 reflection already has `disj_variant_ty` ("look up a
+variant type in a Disj coproduct by label"), confirming arms are label→payload
+edges.
+
+So the primitive **attaches to `v4.std.node`** as a derived operation over the
+existing `Disj` connective. INVARIANTS P2 prescribes extending substrate
+reflection *before* migrating consumers; here that means adding the capability to
+**v4 `.dag` substrate** (`std/node.dag`), not extending the v3-Rust
+`substrate_reflection` seed (`lens_declaration_apply.rs` — see §4.3). INVARIANTS
+§"Reflection evidence" (:385) "extend the `substrate_reflection` submodule"
+refers to that v3 seed submodule; this lane's deliverable is the v4 analogue. It
+adds **no 7th connective and no 6th behavior**, so it does not trip the THESIS
+substrate-extension stop-signal.
+
+This is the **Track 2 cure** named in the L1.1 anchor: "the substrate lets you
+*declare* an algebraic type but does not *derive its canonical operations*, so
+workers hand-roll discriminants and catamorphisms." Coproduct-arm reflection is
+the missing derived operation.
+
+---
+
+## 4. The sanctioned mechanism
+
+### 4.1 Reflected fact carrier (std/node.dag)
+
+```dag
+// A single reflected arm of a closed coproduct (Disj node).
+type CoproductArm {
+  label: Symbol        // the arm's name (the Named edge label)
+  payload: NodeShape   // the arm's payload type; NoEdges-shaped for nullary arms
+}
+```
+
+`CoproductArm` is a fact-bundle (named edges, M1) — it carries the two facts the
+declaration states about an arm and nothing more.
+
+### 4.2 Core projections (compile-time, deterministic, closed-only)
+
+- **`coproduct_arms(T) -> List<CoproductArm>`** — the full reflected arm list of
+  a *closed, declared* coproduct type `T`, in declaration order.
+- **`coproduct_arm_keys(T) -> List<Symbol>`** — `map(coproduct_arms(T), .label)`.
+  The key projection that replaces every hand-written key-enum + key-list mirror
+  (`ConnectiveCoproductVariant`, `TestClaimCoproductVariant`, …).
+- **`coproduct_nullary_inhabitants(T) -> List<T>`** — for coproducts whose arms
+  are **all nullary** (no payload), the value-level inhabitant list. This is the
+  total replacement for `behavior_coproduct_variants() -> List<Behavior>` and
+  `impossible_bug_class_coproduct_variants()`. For a coproduct with **any
+  payload-carrying arm**, this **fails closed** with a typed diagnostic — the
+  primitive never fabricates an inhabitant for a payload arm (C-1/C-9; a default
+  payload would be a fabrication). Payload-arm coproducts get keys, not values.
+- **`common_field_projection(T, field) -> ...`** *(Phase-2b — split out per
+  design-sign Q2; lands after C1 + the corrected gate are green on
+  Connective/Behavior).* When *every* arm of `T` carries a field of the same name
+  and type (e.g. `TestClaim.label`, `TestClaim.anchor`,
+  `TestClaim.classification`), the field is projectable generically. This
+  replaces `test_claim_label()` and the `test_claim_*`-family common-field
+  hand-projections. If an arm lacks the field, it fails closed (the field is not
+  common).
+
+**Discipline of the primitive** (all enforced, not aspirational):
+
+1. **Compile-time only.** `T` is a statically-known, closed type; the arm set is
+   resolved from its declaration at compile time. No runtime reflection. No
+   open-set reflection (M4 — open sets stay diagnostics, not enumerations).
+2. **No execution semantics, no narrowing.** Same posture as the blessed
+   `reflect_program_dag_nodes_in_file`: a complete, deterministic structural
+   projection, no per-consumer narrowing (INVARIANTS §"Reflection evidence").
+3. **Fail-closed everywhere.** Non-coproduct `T`, open `T`, missing common
+   field, or value-inhabitant request on a payload arm → typed diagnostic via
+   `Outcome`, never a fabricated default (P3).
+
+### 4.3 Compiler support (Phase-2 scope; named here, not built)
+
+The primitive requires the compiler to resolve a type reference `T` at its call
+site to the declaration's `Disj` node and project its arm edges. This
+resolution-and-projection is the **primary Phase-2 build risk** and is exactly
+what the §5 conformance gate protects.
+
+**Layer-boundary precision (design-sign condition 2).** This is **new v4
+substrate**, *analogous to* — not an extension of — the existing v3-Rust
+`substrate_reflection` submodule (`lens_declaration_apply.rs`). That v3 surface
+is **bootstrap seed**: per src/v3/SELF_HOSTING.md the seed *shrinks* while v4
+substrate *grows*. The v4 primitive is authored as v4 `.dag` substrate + v4
+compiler support; it does not inherit from or call the v3 seed. The v3 reflection
+is relevant only as (a) a shape precedent and (b) a *cross-generation* check
+factor in the gate (§5.2), never as the home of the new capability.
+
+---
+
+## 5. The 2FA crux — preserved, and strengthened
+
+### 5.1 Class (ii) drift is *eliminated*, not caught
+
+For structurally-determined facts (arm lists, keys, common-field projection,
+structural equality / discriminant), reflection removes the *second list
+entirely*. There is nothing to drift from — the consumer derives from the
+declaration. INVARIANTS P2: "If the canonical answer doesn't exist yet, extend
+the substrate reflection first, then migrate consumers." Making drift
+*unrepresentable* strictly dominates *catching* it. **No 2FA replacement is
+needed for class (ii); the drift class is dissolved.**
+
+### 5.2 Class (i) drift — the by-execution conformance gate (corrected per design-sign Q1)
+
+The mechanism-drift concern is answered by a **by-execution conformance gate**:
+for every gated coproduct, the reflection output must equal an
+**independently-derived** arm set, where "independent" means *derived through a
+distinct lowering path* — not merely "a different function." A bug that corrupts
+the reflection builtin must NOT also corrupt the witness, or the gate is
+**circular** and passes falsely (the self-hosting class-(i) drift the ban
+guards). The factors below are graded by that independence test.
+
+**Why the obvious factor fails (the load-bearing correction).** The natural
+candidate — v4 type-checker match-exhaustiveness — is **NOT independent on its
+own.** v4 inference and the v4 reflection builtin **both resolve `T` to the same
+parsed `Disj` node**; a common-mode resolver/parse arm-drop corrupts *both*
+sides, and the gate passes falsely. So exhaustiveness-count is **common-mode with
+the thing it is checking** and cannot be the gate's independent factor.
+Similarly, the v3 `reflect_program_dag_nodes_in_file` posture is **not a
+pre-existing factor**: it is v3-Rust *seed*, partial, and INVARIANTS:381-383
+explicitly tags it "not yet a closed mechanical theorem … not a substitute for a
+future full conformance gate." It is the gate we are **building**, not one we can
+lean on.
+
+**The gate (REQUIRED).** For every gated coproduct, at least one of the
+following *path-distinct* witnesses must hold by execution:
+
+- **Path 3 — syntactic arm key-set (primary, required for non-roster
+  coproducts).** A parser/syntactic derivation of the arm **labels** — reading the
+  `|`-separated arm names at the grammar level, *before* the shared resolver the
+  reflection builtin uses — and **set-comparing** them to `coproduct_arm_keys(T)`.
+  Because it is computed on a distinct (syntactic) path, a resolver/lowering bug
+  in the reflection builtin does not corrupt it. A cardinality count alone would
+  **not** suffice: `|children| == |keys|` passes falsely on arity-preserving
+  relabel (wrong key, right count) — squarely inside class-(i) mechanism drift.
+  Key-set equality catches drop, add, and relabel. This is the genuine second
+  factor.
+- **Cross-generation check (where v3 covers the carrier).** For carriers the v3
+  seed reflects, `v4 coproduct_arm_keys(Behavior) == v3 reflect_behavior_list`
+  arm set. Two generations, two independent code paths — a strong factor for the
+  Behavior/Connective carriers v3 already covers, usable in addition to Path 3.
+- **Frontier-discovery equality (roster clusters only — the D1c seam).** The CI
+  roster cluster has `affected_set_ci_runner.dag:287`
+  `ci_runner_selected_matches_frontier_discovered`: "discovered == roster:
+  selection output must equal explicit frontier discovery, not hand-roster
+  laundering." For those clusters the witness is **reflection-generated roster ==
+  independently frontier-discovered set** — naturally path-independent
+  (consumer-side derivation) and the strongest factor *there*, but roster-scoped,
+  not a general gate.
+
+**Explicitly rejected as the gate's independent factor:** v4 exhaustiveness-count
+alone (common-mode), and the v3 reflection posture alone (the gate being built).
+The exhaustiveness check may still run as a *consistency* signal, but it does not
+discharge the independence obligation.
+
+This corrected gate is **strictly stronger** than the hand-mirrors: it is checked
+**by execution**, it covers **every** gated coproduct via a genuinely
+path-distinct witness, and it is **one** gate to maintain instead of N driftable
+lists. The mirrors were a weaker, partial, by-inspection form of it.
+
+### 5.3 Per-arm semantics — fail-closed total maps keyed by the reflected set
+
+Some consumers are **not** structurally determined: they assign a value *per arm
+that is not recoverable from the arm's shape* (e.g.
+`impossible_bug_class_from_diagnostic_reason`, per-arm cost/complexity tables).
+Reflection cannot derive these, and silently defaulting them would be a C-8/M5
+fabrication. These do **not** dissolve into pure reflection. Instead they
+**reuse the existing `TotalMap<K,V>`** (`std/collection.dag:165`, `lookup:
+fn(K) -> V`) — *no* new carrier (declaring a `TotalArmMap<T,V>` parallel to
+`TotalMap` would be the very parallel-authority anti-pattern this lane kills, per
+design-sign Q3 / M9). "Keyed by the reflected set" is **not a type** — it is a
+**conformance witness**: `domain(map) == coproduct_arm_keys(T)`. A
+smart-constructor that builds a `TotalMap` and emits that domain-equality witness
+is the sanctioned shape. The consumer supplies the codomain; a missing key is a
+**typed diagnostic at build time**, not a silent fall-through (P3 "Case
+enumeration for open sets" → typed table; M7 data-table single-authority).
+
+This **preserves and strengthens** the class-(ii) exhaustiveness 2FA: "did you
+handle the new arm?" moves from "a hand-written `match` fails to compile" to
+"the substrate proves the table is total against the canonical arm set." Adding
+an arm grows the reflected domain → the table is now missing a key → fail-closed.
+The reviewer still consciously supplies the new arm's semantics — but there is no
+longer a *second arm list* to forget.
+
+---
+
+## 6. Consumer taxonomy (drives Phase 3)
+
+Every census entry sorts into exactly one bucket:
+
+| Bucket | Mechanism | Census members |
+|---|---|---|
+| **C1 — pure enumeration** (arm list / keys / nullary inhabitants) | `coproduct_arm_keys` / `coproduct_nullary_inhabitants` + conformance gate | `connective_coproduct_variant_keys`, `behavior_coproduct_variants`, `impossible_bug_class_coproduct_variants`, `TestClaimCoproductVariant` key-enum + `test_claim_coproduct_variant`, `coproduct_exhaustiveness.dag` arm checks |
+| **C2 — common-field projection** (field present on every arm) | `common_field_projection` *(Phase-2b)* | `test_claim_label` and the `test_claim_*` common-field family |
+| **C3 — structural equality / discriminant** | derived discriminant over arms (L1.1 lens target) | `connective_eq`/`behavior_eq`/`test_claim_coproduct_variant_eq` (broader family) |
+| **C4 — per-arm semantics** (value not in the shape) | fail-closed **`TotalMap<K,V>`** (std/collection.dag:165) + `domain == coproduct_arm_keys(T)` witness | `impossible_bug_class_from_diagnostic_reason`, `coverage.dag:947` reason membership, `lens_cost/*` & `lens_complexity/*` arm tables |
+| **C5 — item rosters** (lists kept in sync with a registry/frontier) | reflection-generated roster + **D1c :287 equality witness** | `manual_corpus_roster`, `affected_set_ci_runner` / `affected_testgen_ci_runner` / `lens_ownership/subject_roster` (swift-stag-552 D1c) |
+
+C4 honestly does **not** vanish into pure reflection — it dissolves the *arm
+list* duplication (the total-map's domain is reflected) while keeping the
+genuine per-arm decision as single-authority data. Naming this honestly is part
+of the design: the falsifier "marks → 0" is met because each mark's *mirror*
+dissolves, even where a (now fail-closed, single-authority) semantic table
+remains.
+
+---
+
+## 7. The ban-lift (the exact ask)
+
+**Lift the `coordination_claims.dag:18` reflection ban for, and only for, the
+following mechanism:**
+
+> Deterministic, **compile-time** reflection over a **closed, declared
+> coproduct** type that projects its **arm keys, common fields, and (for
+> all-nullary coproducts) value inhabitants**, where:
+> 1. every consumer migration deletes its own dissolve-on-arrival mirror in the
+>    **same PR** (per each mark's forbidden-clause);
+> 2. the mechanism is covered by a **tree-wide by-execution conformance gate**
+>    (§5.2) that proves reflection output equals an independently-derived arm
+>    set; and
+> 3. **per-arm-semantic** consumers (C4) become **fail-closed total maps keyed
+>    by the reflected arm set**, never silent defaults.
+
+**Stays banned** (explicitly out of scope of this lift):
+- runtime / dynamic reflection;
+- reflection over **open** sets (M4 — open sets are diagnostics, not enumerable);
+- fabricating inhabitants for **payload-carrying** arms (C-1/C-9);
+- using reflection to **silently default** per-arm semantics (C-8/M5);
+- any reflected projection **not** covered by the §5.2 conformance gate (an
+  ungated reflection consumer is exactly the single-broken-authority hazard the
+  ban was protecting against).
+
+Rationale for a *scoped* lift rather than a blanket repeal: the ban's protective
+intent (2FA against mechanism drift) is **satisfied by construction** within
+this scope (§5) and **violated** outside it. The lift encodes the ban's own
+anticipated "proper mechanism," not its repeal.
+
+---
+
+## 8. Invariant alignment
+
+- **P1 Faithfulness.** Arms are read from the declaration; no heuristic, no
+  ungrounded fact. The primitive is the missing derived operation, not a second
+  authority.
+- **P2 Boundary.** Single authority (the declaration); parallel mirrors deleted
+  in the same change; reflection exposed through the declared `std/node` surface.
+- **P3 Fail-closed.** Non-coproduct / open / payload-inhabitant / missing-common-
+  field / missing-total-map-key all produce typed diagnostics; no fabrication.
+- **P4 Decidability.** Compile-time, bounded fold over a finite Disj node's
+  edges; terminates by construction. No new connective/behavior; no runtime
+  capability.
+- **P5 Dissolution.** Net mirror count strictly decreases; every migration PR is
+  debt-negative; the falsifier (15 core + ban line + ~12 family marks) → 0.
+
+---
+
+## 9. Phasing
+
+- **Phase 1 (this doc).** Design + ban-lift proposal. Gate: snappy-crab-849
+  DESIGN-SIGN + operator BAN-LIFT ruling.
+- **Phase 2a (gated).** Build `CoproductArm` + `coproduct_arms` /
+  `coproduct_arm_keys` / `coproduct_nullary_inhabitants` in `std/node.dag` (new
+  v4 substrate) + the compiler resolution support, and the **corrected §5.2
+  conformance gate** (Path 3 syntactic arm key-set + cross-generation where v3 covers).
+  Inhabit on real coproducts first (`Connective`/`Behavior`) with the gate green
+  by execution before any consumer migrates (facts-before-abstraction).
+- **Phase 2b (gated, after 2a green).** Add `common_field_projection` (the
+  `test_claim_*` common-field family's path).
+- **Phase 3 (gated, may spawn lean per-cluster workers).** Migrate consumers
+  cluster-by-cluster in taxonomy order: C1 std mirrors → C1/C3 generated corpus
+  exhaustiveness/algebra → C5 manual corpus roster → C5 CI rosters (swift-stag-552
+  D1c, with the :287 equality witness). Each PR deletes its own
+  dissolve-on-arrival marks. Re-anchor the marks' `design-dissolution-lens.md
+  L1.1` citation to this doc.
+
+---
+
+## 10. Design-sign resolutions (snappy-crab-849, CONDITIONAL sign — issuecomment-4700373336)
+
+1. **Conformance-gate independence — RESOLVED (the load-bearing condition).**
+   v4 exhaustiveness-count alone is **NOT** an independent factor — it is
+   common-mode with the reflection builtin (both resolve `T` to the same parsed
+   `Disj` node), and the v3 reflection posture is the gate being *built*, not a
+   pre-existing factor. **REQUIRED:** the gate's independent factor is the
+   **syntactic arm key-set (Path 3)** — `|`-separated arm labels from the parse
+   tree set-compared to `coproduct_arm_keys(T)`, not a cardinality count — for
+   every gated coproduct, and/or the **cross-generation check** (`v4
+   coproduct_arm_keys == v3 reflect_behavior_list`) where v3 covers the carrier;
+   rosters additionally use the frontier-discovery equality. Rewritten in §5.2.
+   Exhaustiveness may run as a consistency signal but does not discharge
+   independence.
+2. **Common-field projection — RESOLVED: split to Phase-2b.** Land C1 + the
+   corrected gate on `Connective`/`Behavior` green-by-execution first; add
+   `common_field_projection` after. Reflected in §4.2 / §6 / §9.
+3. **C4 carrier — RESOLVED: reuse `TotalMap<K,V>`** (`std/collection.dag:165`).
+   No `TotalArmMap`. "Keyed by reflected set" is a conformance witness
+   (`domain == coproduct_arm_keys(T)`), not a new type; smart-constructor emits
+   the witness. Reflected in §5.3 / §6.
+4. **Value-inhabitant boundary — CONFIRMED.** All-nullary only;
+   payload arms → fail closed; no inhabit-with-holes.
+
+**Doc-precision condition (condition 2) — APPLIED:** the primitive is **new v4
+substrate**, analogous to (not an extension of) the v3-Rust `substrate_reflection`
+seed, which shrinks while v4 grows (§4.3).
+
+**§5.2 re-read — CONFIRMED (snappy-crab-849, post-0071c645):** design-sign
+carries on the corrected gate. Binding sharpening applied: Path 3 is a **syntactic
+arm key-set** (label set-compared to `coproduct_arm_keys(T)`), not a cardinality
+count — count alone passes falsely on arity-preserving relabel. With Path 3 as
+key-set, **no third path is required** for non-roster/non-v3 coproducts; it
+discharges the independence obligation alone. Cross-generation is additive where
+v3 covers the carrier; frontier-discovery is roster-scoped only. The 2FA guarantee
+proves in Phase-2 when Path 3 (key-set) lands GREEN before any consumer migrates.
+
+**Operator gate (still open):** BAN-LIFT ruling (routed via zesty-swift-79),
+predicated on this corrected 3-factor gate.
diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
new file mode 100644
index 00000000000..74b3322f4fa
--- /dev/null
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -0,0 +1,273 @@
+//! Coproduct-arm reflection — Phase 2a compile-time enumeration (R-reflect).
+//!
+//! Reflection path: resolve `type_name` to a closed `Disj` in the compiled module graph.
+//! Path 3 (syntactic): scan the declaring source for `|`-separated arm labels before any
+//! shared resolver (design-coproduct-arm-reflection.md §5.2).
+
+use std::collections::HashMap;
+use std::rc::Rc;
+
+use crate::v2_compiler_infer_items::ItemKind;
+use crate::v2_interpreter::{InterpContext, InterpError, InterpResult, Value};
+use crate::v2_std_core::{authored_name_at, child_type_node, Connective, Node};
+
+fn expect_symbol<'a>(value: Option<&'a Value>, what: &str) -> InterpResult<&'a str> {
+    match value {
+        Some(Value::Str(s)) => Ok(s.as_str()),
+        _ => Err(InterpError::TypeError {
+            msg: format!("{what} requires a Symbol argument"),
+        }),
+    }
+}
+
+fn type_item_by_name<'a>(
+    ctx: &'a InterpContext,
+    type_name: &str,
+) -> InterpResult<(&'a Rc<Node>, String)> {
+    for module in ctx.modules.iter() {
+        for item in module.items.iter() {
+            let name = authored_name_at(ctx.si(), item.clone());
+            if name != type_name {
+                continue;
+            }
+            let is_type = ctx
+                .item_registry
+                .get(&name)
+                .map(|info| info.kind == ItemKind::TypeItem)
+                .unwrap_or(false)
+                || ctx
+                    .item_registry
+                    .get(&item.name)
+                    .map(|info| info.kind == ItemKind::TypeItem)
+                    .unwrap_or(false);
+            if is_type {
+                return Ok((item, item.span.file.clone()));
+            }
+        }
+    }
+    Err(InterpError::TypeError {
+        msg: format!("coproduct reflection: unknown closed type `{type_name}`"),
+    })
+}
+
+fn disj_variant_labels(item: &Rc<Node>, ctx: &InterpContext) -> InterpResult<Vec<String>> {
+    if item.connective != Connective::Disj {
+        return Err(InterpError::TypeError {
+            msg: "coproduct reflection: type is not a closed coproduct (Disj)".to_string(),
+        });
+    }
+    Ok(item
+        .children
+        .iter()
+        .map(|child| authored_name_at(ctx.si(), child.clone()))
+        .collect())
+}
+
+fn symbol_list_value(ctx: &InterpContext, labels: &[String]) -> Value {
+    let items: Vec<Value> = labels
+        .iter()
+        .map(|label| Value::Str(ctx.sym(label)))
+        .collect();
+    super::v2_interpreter::list_value(items)
+}
+
+fn variant_is_nullary(variant: &Rc<Node>, ctx: &InterpContext) -> bool {
+    let payload = child_type_node(variant.clone());
+    payload.connective == Connective::NoConnective && payload.children.is_empty()
+}
+
+/// Path 3: grammar-level arm labels from `type Name = Arm | Arm | ...` in source text.
+pub fn syntactic_coproduct_arm_labels(file: &str, type_name: &str) -> InterpResult<Vec<String>> {
+    let content = std::fs::read_to_string(file).map_err(|e| InterpError::TypeError {
+        msg: format!("syntactic coproduct arm keys: cannot read `{file}`: {e}"),
+    })?;
+    extract_type_sum_arm_labels(&content, type_name).ok_or_else(|| InterpError::TypeError {
+        msg: format!("syntactic coproduct arm keys: `{type_name}` not found in `{file}`"),
+    })
+}
+
+/// Scan source for `type <name> = <arm> (| <arm>)*` without invoking the type resolver.
+fn extract_type_sum_arm_labels(source: &str, type_name: &str) -> Option<Vec<String>> {
+    let needle = format!("type {type_name}");
+    let start = source.find(&needle)?;
+    let after_type = &source[start + needle.len()..];
+    let eq_rel = after_type.find('=')?;
+    let mut rest = after_type[eq_rel + 1..].trim_start();
+    let mut arms = Vec::new();
+    loop {
+        rest = rest.trim_start();
+        if rest.is_empty() || rest.starts_with("//") {
+            break;
+        }
+        if rest.starts_with('|') {
+            rest = rest[1..].trim_start();
+        }
+        let arm_name = read_identifier_prefix(rest)?;
+        arms.push(arm_name.0);
+        rest = arm_name.1.trim_start();
+        if rest.starts_with('{') {
+            rest = skip_braced(rest)?;
+        }
+        rest = rest.trim_start();
+        if !rest.starts_with('|') {
+            break;
+        }
+    }
+    if arms.is_empty() {
+        None
+    } else {
+        Some(arms)
+    }
+}
+
+fn read_identifier_prefix(s: &str) -> Option<(String, &str)> {
+    let mut end = 0;
+    for (i, ch) in s.char_indices() {
+        if ch.is_ascii_alphanumeric() || ch == '_' {
+            end = i + ch.len_utf8();
+        } else {
+            break;
+        }
+    }
+    if end == 0 {
+        return None;
+    }
+    Some((s[..end].to_string(), &s[end..]))
+}
+
+fn skip_braced(s: &str) -> Option<&str> {
+    let mut depth = 0usize;
+    for (i, ch) in s.char_indices() {
+        match ch {
+            '{' => depth += 1,
+            '}' => {
+                depth = depth.saturating_sub(1);
+                if depth == 0 {
+                    return Some(&s[i + 1..]);
+                }
+            }
+            _ => {}
+        }
+    }
+    None
+}
+
+pub fn eval_coproduct_arm_keys(
+    ctx: &InterpContext,
+    args: &[(Option<String>, Value)],
+) -> InterpResult<Option<Value>> {
+    let type_name = expect_symbol(args.first().map(|(_, v)| v), "coproduct_arm_keys")?;
+    let (item, _) = type_item_by_name(ctx, type_name)?;
+    let labels = disj_variant_labels(item, ctx)?;
+    Ok(Some(symbol_list_value(ctx, &labels)))
+}
+
+pub fn eval_syntactic_coproduct_arm_keys(
+    ctx: &InterpContext,
+    args: &[(Option<String>, Value)],
+) -> InterpResult<Option<Value>> {
+    let type_name = expect_symbol(args.first().map(|(_, v)| v), "syntactic_coproduct_arm_keys")?;
+    let (_, file) = type_item_by_name(ctx, type_name)?;
+    let labels = syntactic_coproduct_arm_labels(&file, type_name)?;
+    Ok(Some(symbol_list_value(ctx, &labels)))
+}
+
+pub fn eval_coproduct_arms(
+    ctx: &InterpContext,
+    args: &[(Option<String>, Value)],
+) -> InterpResult<Option<Value>> {
+    let type_name = expect_symbol(args.first().map(|(_, v)| v), "coproduct_arms")?;
+    let (item, _) = type_item_by_name(ctx, type_name)?;
+    let labels = disj_variant_labels(item, ctx)?;
+    let mut arms = Vec::with_capacity(labels.len());
+    for (variant, label) in item.children.iter().zip(labels.iter()) {
+        let payload = child_type_node(variant.clone());
+        let payload_shape = if variant_is_nullary(variant, ctx) {
+            Value::Variant {
+                variant_name: ctx.sym("Value"),
+                fields: Rc::new(HashMap::new()),
+            }
+        } else {
+            Value::Record {
+                type_name: ctx.sym("NodeShape"),
+                fields: Rc::new(HashMap::from([(
+                    ctx.sym("kind"),
+                    Value::Record {
+                        type_name: ctx.sym("NodeKind"),
+                        fields: Rc::new(HashMap::from([(
+                            ctx.sym("connective"),
+                            Value::Variant {
+                                variant_name: ctx.sym(
+                                    &authored_name_at(ctx.si(), payload.clone()),
+                                ),
+                                fields: Rc::new(HashMap::new()),
+                            },
+                        )])),
+                    },
+                )])),
+            }
+        };
+        arms.push(Value::Record {
+            type_name: ctx.sym("CoproductArm"),
+            fields: Rc::new(HashMap::from([
+                (ctx.sym("label"), Value::Str(ctx.sym(label))),
+                (ctx.sym("payload"), payload_shape),
+            ])),
+        });
+    }
+    Ok(Some(super::v2_interpreter::list_value(arms)))
+}
+
+pub fn eval_coproduct_nullary_inhabitants(
+    ctx: &InterpContext,
+    args: &[(Option<String>, Value)],
+) -> InterpResult<Option<Value>> {
+    let type_name = expect_symbol(
+        args.first().map(|(_, v)| v),
+        "coproduct_nullary_inhabitants",
+    )?;
+    let (item, _) = type_item_by_name(ctx, type_name)?;
+    for variant in item.children.iter() {
+        if !variant_is_nullary(variant, ctx) {
+            return Err(InterpError::TypeError {
+                msg: format!(
+                    "coproduct_nullary_inhabitants: arm `{}` carries a payload — fail closed",
+                    authored_name_at(ctx.si(), variant.clone())
+                ),
+            });
+        }
+    }
+    let inhabitants: Vec<Value> = item
+        .children
+        .iter()
+        .map(|variant| Value::Str(ctx.sym(&authored_name_at(ctx.si(), variant.clone()))))
+        .collect();
+    Ok(Some(super::v2_interpreter::list_value(inhabitants)))
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn syntactic_extractor_finds_connective_arms() {
+        let source = std::fs::read_to_string("src/v4/std/node.dag").expect("read node.dag");
+        let arms = extract_type_sum_arm_labels(&source, "Connective").expect("Connective arms");
+        assert_eq!(
+            arms,
+            vec![
+                "Atom", "Conj", "Disj", "Arrow", "Cardinality", "Instantiation"
+            ]
+        );
+    }
+
+    #[test]
+    fn syntactic_extractor_finds_behavior_arms() {
+        let source = std::fs::read_to_string("src/v4/std/node.dag").expect("read node.dag");
+        let arms = extract_type_sum_arm_labels(&source, "Behavior").expect("Behavior arms");
+        assert_eq!(
+            arms,
+            vec!["Value", "Transform", "Branch", "Loop", "Bind"]
+        );
+    }
+}
diff --git a/src/v2/stage0/src/lib.rs b/src/v2/stage0/src/lib.rs
index eeec7e9bcf2..633d77b25ed 100644
--- a/src/v2/stage0/src/lib.rs
+++ b/src/v2/stage0/src/lib.rs
@@ -13,6 +13,7 @@
 )]
 
 pub mod cli_run;
+pub mod coproduct_reflection;
 pub mod extdeps_cargo;
 pub mod extdeps_languages_dag_emit;
 pub mod extdeps_languages_dag_syntax;
diff --git a/src/v2/stage0/src/v2_interpreter.rs b/src/v2/stage0/src/v2_interpreter.rs
index 246a79d4022..8c02d5d6860 100644
--- a/src/v2/stage0/src/v2_interpreter.rs
+++ b/src/v2/stage0/src/v2_interpreter.rs
@@ -2127,6 +2127,35 @@ fn eval_call(node: &Rc<Node>, env: &Rc<Env>, ctx: &InterpContext) -> InterpResul
         })
         .collect::<InterpResult<_>>()?;
 
+    // R-reflect Phase 2a: compile-time coproduct-arm reflection (intercept before module fn).
+    match func_name.as_str() {
+        "coproduct_arm_keys" => {
+            if let Some(v) = crate::coproduct_reflection::eval_coproduct_arm_keys(ctx, &args)? {
+                return Ok(v);
+            }
+        }
+        "syntactic_coproduct_arm_keys" => {
+            if let Some(v) =
+                crate::coproduct_reflection::eval_syntactic_coproduct_arm_keys(ctx, &args)?
+            {
+                return Ok(v);
+            }
+        }
+        "coproduct_arms" => {
+            if let Some(v) = crate::coproduct_reflection::eval_coproduct_arms(ctx, &args)? {
+                return Ok(v);
+            }
+        }
+        "coproduct_nullary_inhabitants" => {
+            if let Some(v) =
+                crate::coproduct_reflection::eval_coproduct_nullary_inhabitants(ctx, &args)?
+            {
+                return Ok(v);
+            }
+        }
+        _ => {}
+    }
+
     // Check for built-in runtime functions
     if let Some(result) = eval_builtin(&func_name, &args, ctx)? {
         return Ok(result);
diff --git a/src/v4/std/node.dag b/src/v4/std/node.dag
index 0422f4a80c8..824e371e0a7 100644
--- a/src/v4/std/node.dag
+++ b/src/v4/std/node.dag
@@ -43,6 +43,31 @@ type Behavior
   | Bind
 
 
+// R-reflect Phase 2a — coproduct-arm reflection substrate (docs/design-coproduct-arm-reflection.md §4).
+// Compile-time only: arm keys/projections resolve from closed Disj declarations; bodies are
+// intercepted by the v2 reflection builtin (fail-closed stubs if intercept is bypassed).
+type CoproductArm {
+  label: Symbol
+  payload: NodeShape
+}
+
+fn coproduct_arm_keys(type_name: Symbol) -> List<Symbol> {
+  []
+}
+
+fn syntactic_coproduct_arm_keys(type_name: Symbol) -> List<Symbol> {
+  []
+}
+
+fn coproduct_arms(type_name: Symbol) -> List<CoproductArm> {
+  []
+}
+
+fn coproduct_nullary_inhabitants(type_name: Symbol) -> List<Symbol> {
+  []
+}
+
+
 // 🟡 gated — feature:coproduct-variant-enumeration — bound target: coproduct reflection / variant-enumeration substrate (docs/design-dissolution-lens.md L1.1) — bind gunbc#4759 — dissolve-on-arrival: derive Connective/Behavior variant lists from coproduct reflection in std/node.dag; delete these mirrors.
 // forbidden: parallel hand-enumerated Connective/Behavior universes outside std/node.dag.
 type ConnectiveCoproductVariant

From 94aa3b4cd118f2e528f3b655af1562ac48c11d24 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:15:55 +0000
Subject: [PATCH 02/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 .../coproduct_reflection_conformance_test.rs  | 73 +++++++++++++++
 src/v2/tests/src/lib.rs                       |  1 +
 .../claim/extdeps/coordination_claims.dag     |  4 +-
 .../coproduct_reflection_conformance.dag      | 90 +++++++++++++++++++
 4 files changed, 167 insertions(+), 1 deletion(-)
 create mode 100644 src/v2/tests/src/coproduct_reflection_conformance_test.rs
 create mode 100644 src/v4/test/claim/manual/coproduct_reflection_conformance.dag

diff --git a/src/v2/tests/src/coproduct_reflection_conformance_test.rs b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
new file mode 100644
index 00000000000..9a46820de5a
--- /dev/null
+++ b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
@@ -0,0 +1,73 @@
+//! R-reflect Phase 2a: Path-3 key-set conformance on Connective/Behavior by execution.
+
+use std::rc::Rc;
+use std::sync::OnceLock;
+
+use v2_compiler::v2_compiler_compile::{compile_to_resolved, ResolvedPipelineResult, SourceFile};
+use v2_compiler::v2_interpreter::{self, Value};
+
+use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};
+
+const CONFORMANCE_ENTRY: &str = "src/v4/test/claim/manual/coproduct_reflection_conformance.dag";
+const WITNESS_FN: &str = "coproduct_reflection_conformance_holds";
+
+fn v4_source_roots() -> Vec<std::path::PathBuf> {
+    vec![workspace_root().join("src/v4")]
+}
+
+fn cert_source_pairs() -> &'static Vec<(String, String)> {
+    static CACHE: OnceLock<Vec<(String, String)>> = OnceLock::new();
+    CACHE.get_or_init(|| {
+        let entry_content = std::fs::read_to_string(workspace_root().join(CONFORMANCE_ENTRY))
+            .unwrap_or_else(|e| panic!("read {CONFORMANCE_ENTRY}: {e}"));
+        resolve_imports_transitively_with_source_roots(
+            CONFORMANCE_ENTRY,
+            &entry_content,
+            &v4_source_roots(),
+        )
+        .iter()
+        .map(|s| (s.path.clone(), s.content.clone()))
+        .collect()
+    })
+}
+
+fn cert_sources() -> Vec<Rc<SourceFile>> {
+    cert_source_pairs()
+        .iter()
+        .map(|(path, content)| {
+            Rc::new(SourceFile {
+                path: path.clone(),
+                content: content.clone(),
+            })
+        })
+        .collect()
+}
+
+fn assert_resolved_ok(resolved: &ResolvedPipelineResult) {
+    let msgs: Vec<String> = resolved
+        .diagnostics
+        .iter()
+        .map(|d| v2_compiler::v2_std_core::diagnostic_to_message(d.diagnostic.clone()))
+        .filter(|m| !m.starts_with("complexity: "))
+        .collect();
+    assert!(
+        msgs.is_empty() && resolved.graph.is_some(),
+        "expected resolved graph for {CONFORMANCE_ENTRY}, got diagnostics {msgs:?}"
+    );
+}
+
+#[test]
+fn coproduct_reflection_path3_connective_behavior_conformance_holds() {
+    let resolved = compile_to_resolved(Rc::new(cert_sources()));
+    assert_resolved_ok(&resolved);
+    let graph = resolved
+        .graph
+        .as_ref()
+        .expect("graph after successful resolve");
+    match v2_interpreter::run(graph, resolved.source_indices.clone(), WITNESS_FN) {
+        Ok(Value::Bool(true)) => {}
+        other => panic!(
+            "expected Bool(true) from {WITNESS_FN} (Path-3 key-set conformance), got {other:?}"
+        ),
+    }
+}
diff --git a/src/v2/tests/src/lib.rs b/src/v2/tests/src/lib.rs
index 0dcf050b121..1340deccfb3 100644
--- a/src/v2/tests/src/lib.rs
+++ b/src/v2/tests/src/lib.rs
@@ -30,6 +30,7 @@ mod effects;
 #[cfg(test)]
 mod fn_as_value_test;
 #[cfg(test)]
+mod coproduct_reflection_conformance_test;
 mod fold_list_generic_instantiation_test;
 #[cfg(test)]
 mod generator_match_arm_test;
diff --git a/src/v4/test/claim/extdeps/coordination_claims.dag b/src/v4/test/claim/extdeps/coordination_claims.dag
index 8828ac9261d..21d5e9896ee 100644
--- a/src/v4/test/claim/extdeps/coordination_claims.dag
+++ b/src/v4/test/claim/extdeps/coordination_claims.dag
@@ -15,7 +15,9 @@
 // .rs smoke are deleted in the same PR (their content is proven here by execution). The
 // remaining B-class receipts (WireContractFacts/WireContract record-field shapes,
 // SettlementGuarantee/ConsistencyGuarantee shared-discriminant) were deleted with the smoke
-// file per the white-box sweep (reflection banned; decl-shape mirrors are 2FA-for-code).
+// file per the white-box sweep. Reflection stays banned outside the scoped lift in
+// docs/design-coproduct-arm-reflection.md §7 (compile-time closed-coproduct projection +
+// gate-covered fail-closed only); decl-shape mirrors remain 2FA-for-code elsewhere.
 // Importing v4.extdeps.coordination forces v2 to tokenize/parse/infer it, so the
 // parse-surface fact rides every witness below.
 
diff --git a/src/v4/test/claim/manual/coproduct_reflection_conformance.dag b/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
new file mode 100644
index 00000000000..bbaa043f346
--- /dev/null
+++ b/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
@@ -0,0 +1,90 @@
+// src/v4/test/claim/manual/coproduct_reflection_conformance.dag
+// Scope: R-reflect Phase 2a Path-3 key-set conformance witness — Connective/Behavior FIRST
+// (the 2FA proof) before any consumer migrates. Executes reflection vs syntactic arm-key-set
+// equality by claim-run (design-coproduct-arm-reflection.md §5.2 Path 3).
+
+module v4.test.claim.manual.coproduct_reflection_conformance
+
+
+import v4.std.algebra { bag_eq }
+import v4.std.logic { Bool }
+import v4.std.node {
+  Symbol,
+  coproduct_arm_keys,
+  coproduct_nullary_inhabitants,
+  syntactic_coproduct_arm_keys
+}
+import v4.std.verification {
+  BoolWitness,
+  BoolWitnessClaim,
+  UnifiedTestClaim
+}
+
+data reflect_connective_type: Symbol = ^Connective
+data reflect_behavior_type: Symbol = ^Behavior
+
+
+fn symbol_eq(a: Symbol, b: Symbol) -> Bool {
+  a == b
+}
+
+
+fn coproduct_arm_key_set_matches_syntactic(type_name: Symbol) -> Bool {
+  bag_eq(
+    xs: coproduct_arm_keys(type_name: type_name),
+    ys: syntactic_coproduct_arm_keys(type_name: type_name),
+    eq: symbol_eq
+  )
+}
+
+
+fn witness_connective_arm_key_set_path3() -> Bool {
+  coproduct_arm_key_set_matches_syntactic(type_name: reflect_connective_type)
+}
+
+
+fn witness_behavior_arm_key_set_path3() -> Bool {
+  coproduct_arm_key_set_matches_syntactic(type_name: reflect_behavior_type)
+}
+
+
+fn witness_behavior_nullary_inhabitants_count() -> Bool {
+  count(coproduct_nullary_inhabitants(type_name: reflect_behavior_type)) == 5
+}
+
+
+fn coproduct_reflection_conformance_holds() -> Bool {
+  witness_connective_arm_key_set_path3()
+    && witness_behavior_arm_key_set_path3()
+    && witness_behavior_nullary_inhabitants_count()
+}
+
+
+fn witness_connective_arm_key_set_path3_claim() -> BoolWitnessClaim {
+  BoolWitnessClaim {
+    witness: BoolWitness {
+      label: "manual/coproduct_reflection: Connective arm key-set Path-3 conformance",
+      function: witness_connective_arm_key_set_path3
+    }
+  }
+}
+
+
+fn witness_behavior_arm_key_set_path3_claim() -> BoolWitnessClaim {
+  BoolWitnessClaim {
+    witness: BoolWitness {
+      label: "manual/coproduct_reflection: Behavior arm key-set Path-3 conformance",
+      function: witness_behavior_arm_key_set_path3
+    }
+  }
+}
+
+
+fn witness_coproduct_reflection_conformance_claim() -> BoolWitnessClaim {
+  BoolWitnessClaim {
+    witness: BoolWitness {
+      label: "manual/coproduct_reflection: Phase-2a Path-3 gate (Connective/Behavior)",
+      function: coproduct_reflection_conformance_holds
+    }
+  }
+}

From 36462a85a76072637791356b98d9fb4098c4e20e Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:17:32 +0000
Subject: [PATCH 03/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs | 69 +++++++++++++----------
 src/v2/stage0/src/v2_interpreter.rs       |  6 +-
 2 files changed, 44 insertions(+), 31 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index 74b3322f4fa..31473682402 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -24,9 +24,10 @@ fn type_item_by_name<'a>(
     ctx: &'a InterpContext,
     type_name: &str,
 ) -> InterpResult<(&'a Rc<Node>, String)> {
+    let si = ctx.source_indices();
     for module in ctx.modules.iter() {
         for item in module.items.iter() {
-            let name = authored_name_at(ctx.si(), item.clone());
+            let name = authored_name_at(si.clone(), item.clone());
             if name != type_name {
                 continue;
             }
@@ -56,18 +57,16 @@ fn disj_variant_labels(item: &Rc<Node>, ctx: &InterpContext) -> InterpResult<Vec
             msg: "coproduct reflection: type is not a closed coproduct (Disj)".to_string(),
         });
     }
+    let si = ctx.source_indices();
     Ok(item
         .children
         .iter()
-        .map(|child| authored_name_at(ctx.si(), child.clone()))
+        .map(|child| authored_name_at(si.clone(), child.clone()))
         .collect())
 }
 
-fn symbol_list_value(ctx: &InterpContext, labels: &[String]) -> Value {
-    let items: Vec<Value> = labels
-        .iter()
-        .map(|label| Value::Str(ctx.sym(label)))
-        .collect();
+fn symbol_list_value(labels: &[String]) -> Value {
+    let items: Vec<Value> = labels.iter().map(|label| Value::Str(label.clone())).collect();
     super::v2_interpreter::list_value(items)
 }
 
@@ -159,7 +158,7 @@ pub fn eval_coproduct_arm_keys(
     let type_name = expect_symbol(args.first().map(|(_, v)| v), "coproduct_arm_keys")?;
     let (item, _) = type_item_by_name(ctx, type_name)?;
     let labels = disj_variant_labels(item, ctx)?;
-    Ok(Some(symbol_list_value(ctx, &labels)))
+    Ok(Some(symbol_list_value(&labels)))
 }
 
 pub fn eval_syntactic_coproduct_arm_keys(
@@ -169,7 +168,7 @@ pub fn eval_syntactic_coproduct_arm_keys(
     let type_name = expect_symbol(args.first().map(|(_, v)| v), "syntactic_coproduct_arm_keys")?;
     let (_, file) = type_item_by_name(ctx, type_name)?;
     let labels = syntactic_coproduct_arm_labels(&file, type_name)?;
-    Ok(Some(symbol_list_value(ctx, &labels)))
+    Ok(Some(symbol_list_value(&labels)))
 }
 
 pub fn eval_coproduct_arms(
@@ -178,31 +177,34 @@ pub fn eval_coproduct_arms(
 ) -> InterpResult<Option<Value>> {
     let type_name = expect_symbol(args.first().map(|(_, v)| v), "coproduct_arms")?;
     let (item, _) = type_item_by_name(ctx, type_name)?;
+    let si = ctx.source_indices();
     let labels = disj_variant_labels(item, ctx)?;
     let mut arms = Vec::with_capacity(labels.len());
     for (variant, label) in item.children.iter().zip(labels.iter()) {
-        let payload = child_type_node(variant.clone());
         let payload_shape = if variant_is_nullary(variant, ctx) {
             Value::Variant {
-                variant_name: ctx.sym("Value"),
-                fields: Rc::new(HashMap::new()),
+                type_name: ctx.sym("NodeKind"),
+                variant_name: ctx.sym("ComputationNode"),
+                fields: Rc::new(HashMap::from([(
+                    ctx.sym("behavior"),
+                    Value::Variant {
+                        type_name: ctx.sym("Behavior"),
+                        variant_name: ctx.sym(label),
+                        fields: Rc::new(HashMap::new()),
+                    },
+                )])),
             }
         } else {
-            Value::Record {
-                type_name: ctx.sym("NodeShape"),
+            let payload = child_type_node(variant.clone());
+            Value::Variant {
+                type_name: ctx.sym("NodeKind"),
+                variant_name: ctx.sym("TypeNode"),
                 fields: Rc::new(HashMap::from([(
-                    ctx.sym("kind"),
-                    Value::Record {
-                        type_name: ctx.sym("NodeKind"),
-                        fields: Rc::new(HashMap::from([(
-                            ctx.sym("connective"),
-                            Value::Variant {
-                                variant_name: ctx.sym(
-                                    &authored_name_at(ctx.si(), payload.clone()),
-                                ),
-                                fields: Rc::new(HashMap::new()),
-                            },
-                        )])),
+                    ctx.sym("connective"),
+                    Value::Variant {
+                        type_name: ctx.sym("Connective"),
+                        variant_name: ctx.sym(&authored_name_at(si.clone(), payload.clone())),
+                        fields: Rc::new(HashMap::new()),
                     },
                 )])),
             }
@@ -210,8 +212,14 @@ pub fn eval_coproduct_arms(
         arms.push(Value::Record {
             type_name: ctx.sym("CoproductArm"),
             fields: Rc::new(HashMap::from([
-                (ctx.sym("label"), Value::Str(ctx.sym(label))),
-                (ctx.sym("payload"), payload_shape),
+                (ctx.sym("label"), Value::Str(label.clone())),
+                (
+                    ctx.sym("payload"),
+                    Value::Record {
+                        type_name: ctx.sym("NodeShape"),
+                        fields: Rc::new(HashMap::from([(ctx.sym("kind"), payload_shape)])),
+                    },
+                ),
             ])),
         });
     }
@@ -227,12 +235,13 @@ pub fn eval_coproduct_nullary_inhabitants(
         "coproduct_nullary_inhabitants",
     )?;
     let (item, _) = type_item_by_name(ctx, type_name)?;
+    let si = ctx.source_indices();
     for variant in item.children.iter() {
         if !variant_is_nullary(variant, ctx) {
             return Err(InterpError::TypeError {
                 msg: format!(
                     "coproduct_nullary_inhabitants: arm `{}` carries a payload — fail closed",
-                    authored_name_at(ctx.si(), variant.clone())
+                    authored_name_at(si.clone(), variant.clone())
                 ),
             });
         }
@@ -240,7 +249,7 @@ pub fn eval_coproduct_nullary_inhabitants(
     let inhabitants: Vec<Value> = item
         .children
         .iter()
-        .map(|variant| Value::Str(ctx.sym(&authored_name_at(ctx.si(), variant.clone()))))
+        .map(|variant| Value::Str(authored_name_at(si.clone(), variant.clone())))
         .collect();
     Ok(Some(super::v2_interpreter::list_value(inhabitants)))
 }
diff --git a/src/v2/stage0/src/v2_interpreter.rs b/src/v2/stage0/src/v2_interpreter.rs
index 8c02d5d6860..4347b29e5ea 100644
--- a/src/v2/stage0/src/v2_interpreter.rs
+++ b/src/v2/stage0/src/v2_interpreter.rs
@@ -428,7 +428,7 @@ pub enum Value {
 
 /// Wrap a list carrier (or anything convertible to one, e.g. `Vec<Value>`)
 /// into a `Value::List`.
-fn list_value(items: impl Into<RrbVector<Value>>) -> Value {
+pub(crate) fn list_value(items: impl Into<RrbVector<Value>>) -> Value {
     Value::List(Rc::new(items.into()))
 }
 
@@ -1154,6 +1154,10 @@ impl InterpContext {
         self.source_indices.clone()
     }
 
+    pub(crate) fn source_indices(&self) -> Rc<HashMap<String, Rc<NewlineIndex>>> {
+        self.si()
+    }
+
     fn lookup_fn(&self, name: &str) -> Option<&Rc<Node>> {
         self.fn_nodes.get(name)
     }

From 57d3c6d98549d780bfa61d57eed685ef06a741e9 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:18:55 +0000
Subject: [PATCH 04/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index 31473682402..c92b0cd30d5 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -9,7 +9,8 @@ use std::rc::Rc;
 
 use crate::v2_compiler_infer_items::ItemKind;
 use crate::v2_interpreter::{InterpContext, InterpError, InterpResult, Value};
-use crate::v2_std_core::{authored_name_at, child_type_node, Connective, Node};
+use crate::v2_compiler_infer_types::child_type_node;
+use crate::v2_std_core::{authored_name_at, Connective, Node};
 
 fn expect_symbol<'a>(value: Option<&'a Value>, what: &str) -> InterpResult<&'a str> {
     match value {
@@ -67,7 +68,7 @@ fn disj_variant_labels(item: &Rc<Node>, ctx: &InterpContext) -> InterpResult<Vec
 
 fn symbol_list_value(labels: &[String]) -> Value {
     let items: Vec<Value> = labels.iter().map(|label| Value::Str(label.clone())).collect();
-    super::v2_interpreter::list_value(items)
+    crate::v2_interpreter::list_value(items)
 }
 
 fn variant_is_nullary(variant: &Rc<Node>, ctx: &InterpContext) -> bool {
@@ -223,7 +224,7 @@ pub fn eval_coproduct_arms(
             ])),
         });
     }
-    Ok(Some(super::v2_interpreter::list_value(arms)))
+    Ok(Some(crate::v2_interpreter::list_value(arms)))
 }
 
 pub fn eval_coproduct_nullary_inhabitants(
@@ -251,7 +252,7 @@ pub fn eval_coproduct_nullary_inhabitants(
         .iter()
         .map(|variant| Value::Str(authored_name_at(si.clone(), variant.clone())))
         .collect();
-    Ok(Some(super::v2_interpreter::list_value(inhabitants)))
+    Ok(Some(crate::v2_interpreter::list_value(inhabitants)))
 }
 
 #[cfg(test)]

From e69eba07f0b97cfd0505424f87deb7d3ac1064a5 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:21:56 +0000
Subject: [PATCH 05/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index c92b0cd30d5..2a003a82ccd 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -261,7 +261,9 @@ mod tests {
 
     #[test]
     fn syntactic_extractor_finds_connective_arms() {
-        let source = std::fs::read_to_string("src/v4/std/node.dag").expect("read node.dag");
+        let path = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
+            .join("../../../src/v4/std/node.dag");
+        let source = std::fs::read_to_string(&path).expect("read node.dag");
         let arms = extract_type_sum_arm_labels(&source, "Connective").expect("Connective arms");
         assert_eq!(
             arms,
@@ -273,7 +275,9 @@ mod tests {
 
     #[test]
     fn syntactic_extractor_finds_behavior_arms() {
-        let source = std::fs::read_to_string("src/v4/std/node.dag").expect("read node.dag");
+        let path = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
+            .join("../../../src/v4/std/node.dag");
+        let source = std::fs::read_to_string(&path).expect("read node.dag");
         let arms = extract_type_sum_arm_labels(&source, "Behavior").expect("Behavior arms");
         assert_eq!(
             arms,

From c6a5d7f4e533cf1d699302bcfdfea2f0b8673d6a Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:23:32 +0000
Subject: [PATCH 06/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 .../coproduct_reflection_conformance.dag      | 35 -------------------
 1 file changed, 35 deletions(-)

diff --git a/src/v4/test/claim/manual/coproduct_reflection_conformance.dag b/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
index bbaa043f346..3b96710ff9c 100644
--- a/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
+++ b/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
@@ -14,11 +14,6 @@ import v4.std.node {
   coproduct_nullary_inhabitants,
   syntactic_coproduct_arm_keys
 }
-import v4.std.verification {
-  BoolWitness,
-  BoolWitnessClaim,
-  UnifiedTestClaim
-}
 
 data reflect_connective_type: Symbol = ^Connective
 data reflect_behavior_type: Symbol = ^Behavior
@@ -58,33 +53,3 @@ fn coproduct_reflection_conformance_holds() -> Bool {
     && witness_behavior_arm_key_set_path3()
     && witness_behavior_nullary_inhabitants_count()
 }
-
-
-fn witness_connective_arm_key_set_path3_claim() -> BoolWitnessClaim {
-  BoolWitnessClaim {
-    witness: BoolWitness {
-      label: "manual/coproduct_reflection: Connective arm key-set Path-3 conformance",
-      function: witness_connective_arm_key_set_path3
-    }
-  }
-}
-
-
-fn witness_behavior_arm_key_set_path3_claim() -> BoolWitnessClaim {
-  BoolWitnessClaim {
-    witness: BoolWitness {
-      label: "manual/coproduct_reflection: Behavior arm key-set Path-3 conformance",
-      function: witness_behavior_arm_key_set_path3
-    }
-  }
-}
-
-
-fn witness_coproduct_reflection_conformance_claim() -> BoolWitnessClaim {
-  BoolWitnessClaim {
-    witness: BoolWitness {
-      label: "manual/coproduct_reflection: Phase-2a Path-3 gate (Connective/Behavior)",
-      function: coproduct_reflection_conformance_holds
-    }
-  }
-}

From 57f29d9693fb82018663e2f12bf55b8cf568272b Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:26:26 +0000
Subject: [PATCH 07/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 .../coproduct_reflection_conformance_test.rs  | 39 +++++++------------
 1 file changed, 14 insertions(+), 25 deletions(-)

diff --git a/src/v2/tests/src/coproduct_reflection_conformance_test.rs b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
index 9a46820de5a..c51f1fd9e2e 100644
--- a/src/v2/tests/src/coproduct_reflection_conformance_test.rs
+++ b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
@@ -1,7 +1,6 @@
 //! R-reflect Phase 2a: Path-3 key-set conformance on Connective/Behavior by execution.
 
 use std::rc::Rc;
-use std::sync::OnceLock;
 
 use v2_compiler::v2_compiler_compile::{compile_to_resolved, ResolvedPipelineResult, SourceFile};
 use v2_compiler::v2_interpreter::{self, Value};
@@ -15,32 +14,22 @@ fn v4_source_roots() -> Vec<std::path::PathBuf> {
     vec![workspace_root().join("src/v4")]
 }
 
-fn cert_source_pairs() -> &'static Vec<(String, String)> {
-    static CACHE: OnceLock<Vec<(String, String)>> = OnceLock::new();
-    CACHE.get_or_init(|| {
-        let entry_content = std::fs::read_to_string(workspace_root().join(CONFORMANCE_ENTRY))
-            .unwrap_or_else(|e| panic!("read {CONFORMANCE_ENTRY}: {e}"));
-        resolve_imports_transitively_with_source_roots(
-            CONFORMANCE_ENTRY,
-            &entry_content,
-            &v4_source_roots(),
-        )
-        .iter()
-        .map(|s| (s.path.clone(), s.content.clone()))
-        .collect()
-    })
-}
-
 fn cert_sources() -> Vec<Rc<SourceFile>> {
-    cert_source_pairs()
-        .iter()
-        .map(|(path, content)| {
-            Rc::new(SourceFile {
-                path: path.clone(),
-                content: content.clone(),
-            })
+    let entry_content = std::fs::read_to_string(workspace_root().join(CONFORMANCE_ENTRY))
+        .unwrap_or_else(|e| panic!("read {CONFORMANCE_ENTRY}: {e}"));
+    resolve_imports_transitively_with_source_roots(
+        CONFORMANCE_ENTRY,
+        &entry_content,
+        &v4_source_roots(),
+    )
+    .iter()
+    .map(|s| {
+        Rc::new(SourceFile {
+            path: s.path.clone(),
+            content: s.content.clone(),
         })
-        .collect()
+    })
+    .collect()
 }
 
 fn assert_resolved_ok(resolved: &ResolvedPipelineResult) {

From fa95d877bbc6b4e23e48de28ede86efe62cd9c7a Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:28:00 +0000
Subject: [PATCH 08/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs     | 35 +++++++++++++++++--
 .../coproduct_reflection_conformance_test.rs  |  2 ++
 2 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index 2a003a82ccd..241f5eeaead 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -76,10 +76,41 @@ fn variant_is_nullary(variant: &Rc<Node>, ctx: &InterpContext) -> bool {
     payload.connective == Connective::NoConnective && payload.children.is_empty()
 }
 
+fn resolve_source_file_path(file: &str) -> InterpResult<String> {
+    let path = std::path::Path::new(file);
+    if path.is_absolute() && path.exists() {
+        return Ok(file.to_string());
+    }
+    if path.exists() {
+        return Ok(file.to_string());
+    }
+    if let Ok(mut dir) = std::env::current_dir() {
+        loop {
+            let candidate = dir.join(file);
+            if candidate.exists() {
+                return Ok(candidate.to_string_lossy().into_owned());
+            }
+            if !dir.pop() {
+                break;
+            }
+        }
+    }
+    if let Ok(root) = std::env::var("GUNBC_ROOT") {
+        let candidate = std::path::Path::new(&root).join(file);
+        if candidate.exists() {
+            return Ok(candidate.to_string_lossy().into_owned());
+        }
+    }
+    Err(InterpError::TypeError {
+        msg: format!("coproduct reflection: cannot resolve source path `{file}`"),
+    })
+}
+
 /// Path 3: grammar-level arm labels from `type Name = Arm | Arm | ...` in source text.
 pub fn syntactic_coproduct_arm_labels(file: &str, type_name: &str) -> InterpResult<Vec<String>> {
-    let content = std::fs::read_to_string(file).map_err(|e| InterpError::TypeError {
-        msg: format!("syntactic coproduct arm keys: cannot read `{file}`: {e}"),
+    let resolved = resolve_source_file_path(file)?;
+    let content = std::fs::read_to_string(&resolved).map_err(|e| InterpError::TypeError {
+        msg: format!("syntactic coproduct arm keys: cannot read `{resolved}`: {e}"),
     })?;
     extract_type_sum_arm_labels(&content, type_name).ok_or_else(|| InterpError::TypeError {
         msg: format!("syntactic coproduct arm keys: `{type_name}` not found in `{file}`"),
diff --git a/src/v2/tests/src/coproduct_reflection_conformance_test.rs b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
index c51f1fd9e2e..18ec2625b6f 100644
--- a/src/v2/tests/src/coproduct_reflection_conformance_test.rs
+++ b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
@@ -47,6 +47,8 @@ fn assert_resolved_ok(resolved: &ResolvedPipelineResult) {
 
 #[test]
 fn coproduct_reflection_path3_connective_behavior_conformance_holds() {
+    // gunbc claim-run resolves sources relative to workspace root; mirror that here.
+    std::env::set_var("GUNBC_ROOT", workspace_root());
     let resolved = compile_to_resolved(Rc::new(cert_sources()));
     assert_resolved_ok(&resolved);
     let graph = resolved

From 37e375c92b9102931cc452b4f956783e80fda249 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:29:32 +0000
Subject: [PATCH 09/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index 241f5eeaead..506102d493b 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -71,9 +71,14 @@ fn symbol_list_value(labels: &[String]) -> Value {
     crate::v2_interpreter::list_value(items)
 }
 
-fn variant_is_nullary(variant: &Rc<Node>, ctx: &InterpContext) -> bool {
+fn variant_is_nullary(variant: &Rc<Node>, _ctx: &InterpContext) -> bool {
     let payload = child_type_node(variant.clone());
-    payload.connective == Connective::NoConnective && payload.children.is_empty()
+    match payload.connective {
+        Connective::NoConnective => payload.children.is_empty(),
+        Connective::Conj => payload.children.is_empty(),
+        Connective::Atom(_) => true,
+        _ => false,
+    }
 }
 
 fn resolve_source_file_path(file: &str) -> InterpResult<String> {

From b16352c2e753d4746793ab9bed3ac1d58b551e1a Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:30:56 +0000
Subject: [PATCH 10/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index 506102d493b..c8dc76bc388 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -76,7 +76,6 @@ fn variant_is_nullary(variant: &Rc<Node>, _ctx: &InterpContext) -> bool {
     match payload.connective {
         Connective::NoConnective => payload.children.is_empty(),
         Connective::Conj => payload.children.is_empty(),
-        Connective::Atom(_) => true,
         _ => false,
     }
 }

From 4eedbd047e210524d68d0de24c494a53b264834f Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:32:24 +0000
Subject: [PATCH 11/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs | 27 ++++++++++++++---------
 src/v2/tests/src/lib.rs                   |  4 ++--
 2 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index c8dc76bc388..f4d4ab1b7a5 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -8,8 +8,8 @@ use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::v2_compiler_infer_items::ItemKind;
-use crate::v2_interpreter::{InterpContext, InterpError, InterpResult, Value};
 use crate::v2_compiler_infer_types::child_type_node;
+use crate::v2_interpreter::{InterpContext, InterpError, InterpResult, Value};
 use crate::v2_std_core::{authored_name_at, Connective, Node};
 
 fn expect_symbol<'a>(value: Option<&'a Value>, what: &str) -> InterpResult<&'a str> {
@@ -67,7 +67,10 @@ fn disj_variant_labels(item: &Rc<Node>, ctx: &InterpContext) -> InterpResult<Vec
 }
 
 fn symbol_list_value(labels: &[String]) -> Value {
-    let items: Vec<Value> = labels.iter().map(|label| Value::Str(label.clone())).collect();
+    let items: Vec<Value> = labels
+        .iter()
+        .map(|label| Value::Str(label.clone()))
+        .collect();
     crate::v2_interpreter::list_value(items)
 }
 
@@ -296,27 +299,29 @@ mod tests {
 
     #[test]
     fn syntactic_extractor_finds_connective_arms() {
-        let path = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
-            .join("../../../src/v4/std/node.dag");
+        let path =
+            std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../../../src/v4/std/node.dag");
         let source = std::fs::read_to_string(&path).expect("read node.dag");
         let arms = extract_type_sum_arm_labels(&source, "Connective").expect("Connective arms");
         assert_eq!(
             arms,
             vec![
-                "Atom", "Conj", "Disj", "Arrow", "Cardinality", "Instantiation"
+                "Atom",
+                "Conj",
+                "Disj",
+                "Arrow",
+                "Cardinality",
+                "Instantiation"
             ]
         );
     }
 
     #[test]
     fn syntactic_extractor_finds_behavior_arms() {
-        let path = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
-            .join("../../../src/v4/std/node.dag");
+        let path =
+            std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../../../src/v4/std/node.dag");
         let source = std::fs::read_to_string(&path).expect("read node.dag");
         let arms = extract_type_sum_arm_labels(&source, "Behavior").expect("Behavior arms");
-        assert_eq!(
-            arms,
-            vec!["Value", "Transform", "Branch", "Loop", "Bind"]
-        );
+        assert_eq!(arms, vec!["Value", "Transform", "Branch", "Loop", "Bind"]);
     }
 }
diff --git a/src/v2/tests/src/lib.rs b/src/v2/tests/src/lib.rs
index 1340deccfb3..0f048963ae4 100644
--- a/src/v2/tests/src/lib.rs
+++ b/src/v2/tests/src/lib.rs
@@ -20,6 +20,8 @@ mod bootstrap;
 #[cfg(test)]
 mod bug_sentinel_ratchet;
 #[cfg(test)]
+mod coproduct_reflection_conformance_test;
+#[cfg(test)]
 mod data_cache_scoping_test;
 #[cfg(test)]
 mod derive_bound_fail_closed_test;
@@ -29,8 +31,6 @@ mod diagnostics;
 mod effects;
 #[cfg(test)]
 mod fn_as_value_test;
-#[cfg(test)]
-mod coproduct_reflection_conformance_test;
 mod fold_list_generic_instantiation_test;
 #[cfg(test)]
 mod generator_match_arm_test;

From 1e354a07b79b46ce7884c7237d323f5b653b8f25 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:54:39 +0000
Subject: [PATCH 12/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/05_emit_rust.dag                    | 2 +-
 src/v2/stage0/src/bin/regen_stage0.rs      | 1 +
 src/v2/stage0/src/v2_compiler_emit_rust.rs | 2 +-
 src/v2/tests/src/bootstrap.rs              | 8 +++++++-
 4 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/v2/05_emit_rust.dag b/src/v2/05_emit_rust.dag
index 427b7005398..a0ab775859a 100644
--- a/src/v2/05_emit_rust.dag
+++ b/src/v2/05_emit_rust.dag
@@ -1258,7 +1258,7 @@ fn emit_lib_rs_from_files(all_module_files: List<TextFile>, has_compiler_tests:
   // rest_transport_facts.rs and INVARIANTS bounded substrate seed).
   // These are not generated — they survive regen as non-generated files.
   let hand_maintained_mods = if has_compiler_tests {
-    "\npub mod v2_interpreter;\npub mod cli_run;\npub mod rest_transport_facts;"
+    "\npub mod v2_interpreter;\npub mod cli_run;\npub mod rest_transport_facts;\npub mod coproduct_reflection;"
   } else {
     ""
   }
diff --git a/src/v2/stage0/src/bin/regen_stage0.rs b/src/v2/stage0/src/bin/regen_stage0.rs
index 0762b3e0b8d..73f98988cff 100644
--- a/src/v2/stage0/src/bin/regen_stage0.rs
+++ b/src/v2/stage0/src/bin/regen_stage0.rs
@@ -97,6 +97,7 @@ const GENERATED_STAGE0_FILES: &[&str] = &[
 
 const HAND_MAINTAINED_STAGE0_FILES: &[&str] = &[
     "cli_run.rs",
+    "coproduct_reflection.rs",
     "rest_transport_facts.rs",
     "v2_compiler_dag_collect.rs",
     "v2_interpreter.rs",
diff --git a/src/v2/stage0/src/v2_compiler_emit_rust.rs b/src/v2/stage0/src/v2_compiler_emit_rust.rs
index ec4e36dd359..65e1eb7373f 100644
--- a/src/v2/stage0/src/v2_compiler_emit_rust.rs
+++ b/src/v2/stage0/src/v2_compiler_emit_rust.rs
@@ -2498,7 +2498,7 @@ pub fn emit_lib_rs_from_files(
             __result
         });
         let hand_maintained_mods = if has_compiler_tests.clone() {
-            "\npub mod v2_interpreter;\npub mod cli_run;\npub mod rest_transport_facts;".to_string()
+            "\npub mod v2_interpreter;\npub mod cli_run;\npub mod rest_transport_facts;\npub mod coproduct_reflection;".to_string()
         } else {
             "".to_string()
         };
diff --git a/src/v2/tests/src/bootstrap.rs b/src/v2/tests/src/bootstrap.rs
index a1ecdea667b..d9266d2c493 100644
--- a/src/v2/tests/src/bootstrap.rs
+++ b/src/v2/tests/src/bootstrap.rs
@@ -123,7 +123,12 @@ fn parse_diagnostic_count(stderr: &str) -> usize {
 /// (graph-exported facts replace this scaffold).
 fn copy_stage0_support_modules(stage1_dir: &std::path::Path, ws: &std::path::Path) {
     let stage0_src = ws.join("src/v2/stage0/src");
-    for name in &["v2_interpreter.rs", "cli_run.rs", "rest_transport_facts.rs"] {
+    for name in &[
+        "v2_interpreter.rs",
+        "cli_run.rs",
+        "rest_transport_facts.rs",
+        "coproduct_reflection.rs",
+    ] {
         let src = stage0_src.join(name);
         if src.exists() {
             let dst = stage1_dir.join("src").join(name);
@@ -182,6 +187,7 @@ fn diff_excluding_hand_maintained(
         .arg("--exclude=v2_interpreter.rs")
         .arg("--exclude=cli_run.rs")
         .arg("--exclude=rest_transport_facts.rs")
+        .arg("--exclude=coproduct_reflection.rs")
         .arg(dir_a)
         .arg(dir_b)
         .output()

From 9ea1eca8042037ff585466cb7be72a4c846ce3ff Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:57:33 +0000
Subject: [PATCH 13/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 docs/design-coproduct-arm-reflection.md       | 438 ------------------
 src/v2/stage0/src/coproduct_reflection.rs     | 164 +++----
 src/v2/stage0/src/v2_interpreter.rs           |  25 +-
 src/v4/std/node.dag                           |  28 +-
 .../coproduct_reflection_conformance.dag      |  12 +-
 src/v4/workflow/lens_ci_gate.dag              |  31 +-
 6 files changed, 116 insertions(+), 582 deletions(-)
 delete mode 100644 docs/design-coproduct-arm-reflection.md

diff --git a/docs/design-coproduct-arm-reflection.md b/docs/design-coproduct-arm-reflection.md
deleted file mode 100644
index 448b7ad8287..00000000000
--- a/docs/design-coproduct-arm-reflection.md
+++ /dev/null
@@ -1,438 +0,0 @@
-# Coproduct-arm reflection — design + ban-lift proposal
-
-> **Status: design (Phase 1 of the R-reflect lane). GATED.**
-> This document is a proposal. No implementation, primitive, or consumer
-> migration lands until it has (a) substrate **DESIGN-SIGN** (snappy-crab-849)
-> and (b) the operator's **BAN-LIFT RULING** (routed via zesty-swift-79). It
-> exists to be reviewed, not to authorize work.
->
-> **Anchor.** This is the *Track 2 — substrate-derivation* spec for the lens
-> family the dissolve-on-arrival marks cite as `docs/design-dissolution-lens.md
-> L1.1` ("coproduct reflection / variant-enumeration substrate"). That internal
-> doc was removed in the public-visibility flip (#4192); this public design doc
-> is its surviving, scoped successor. Phase 3 re-anchors the marks' citations
-> here.
->
-> **Cross-refs (live):** INVARIANTS.md P1/P2/P3/P4/P5 and §"Reflection evidence
-> is not structural proof"; MODELING.md M8/M9/M11/M12; THESIS §"Self-inspection",
-> §"Structural decompression"; src/v3/SELF_HOSTING.md §2.3 (language-agnostic
-> core); CODING.md (Rust style for any compiler support).
-
----
-
-## 0. One-paragraph summary
-
-A **coproduct-arm reflection** primitive enumerates a closed sum type's variant
-arms and projects per-arm keys/labels, so downstream models **derive** variant
-lists, arm-discriminants, and item rosters **from the type** instead of
-hand-mirroring them. Today ~15 `gunbc#4759`-bound mirror marks (plus ~12
-broader-family arm-tables) hand-maintain second copies of facts the declaration
-already states. Reflection makes those mirrors *unrepresentable* (you cannot
-drift from yourself) for structurally-determined facts, and converts the
-genuinely per-arm-semantic consumers into **fail-closed total maps keyed by the
-reflected arm set**. The reflection *mechanism itself* is held honest by one
-tree-wide **by-execution conformance gate** (reflection output == an
-independently-derived arm set), which replaces N hand-mirrors with a single,
-broader, executed check. The ban is lifted **only** for this mechanism, under
-those guarantees.
-
----
-
-## 1. The problem — hand-rostered / mirror marks
-
-A coproduct is declared once:
-
-```dag
-type Connective = Atom { identity: Symbol } | Conj | Disj | Arrow | Cardinality | Instantiation   // std/node.dag
-```
-
-…and then its arm set is **re-stated by hand** in many places. Grounded census
-(verify line numbers at HEAD; from `main`):
-
-**Core falsifier — 15 `gunbc#4759`-bound mirror mark-lines across 6 files:**
-
-| File | Mark(s) | What it mirrors |
-|---|---|---|
-| `src/v4/std/node.dag` | :46 | `ConnectiveCoproductVariant` enum + `connective_coproduct_variant_keys()` + `behavior_coproduct_variants()` — hand-lists of `Connective`/`Behavior` arms |
-| `src/v4/std/verification.dag` | :93 | `impossible_bug_class_coproduct_variants()` — hand-list of `ImpossibleBugClass` arms |
-| ″ | :134 | `impossible_bug_class_from_diagnostic_reason()` — reason→class bridge |
-| ″ | :195/:197 | `TestClaimCoproductVariant` — key-enum mirror of `TestClaim` arms |
-| ″ | :210/:212 | `ClaimAnchorKey` manual/generated union (anchor split) |
-| ″ | :275 | `test_claim_label()` — hand-enumerated `TestClaim`→label projection |
-| ″ | :287 | `test_claim_coproduct_variant()` — hand-enumerated `TestClaim`→key projection |
-| `src/v4/test/claim/generated/coproduct_exhaustiveness.dag` | :53/:63/:92 | hand-rolled arm-discriminant checks (DiagnosticClaim / GeneratedClaimAnchor / 4-arm `TestClaimCoproductVariant` equality) |
-| `src/v4/test/claim/generated/algebra_law_conformance.dag` | :32 | local nat-expression node shape-tags |
-| `src/v4/lens/coverage.dag` | :947 | impossible-bug reason membership (consumes verification's projection) |
-| `src/v4/test/claim/manual/manual_corpus_roster.dag` | :4 | "item-registry reflection replaces explicit import roster" |
-
-**Broader family (~12, same shape, not #4759-bound):** arm-tables /
-variant-discriminant marks in `lens/coverage`, `lens_cost/*`, `lens_complexity/*`
-(per-arm cost & complexity tables). Surfaced as a Phase-3 consumer cluster;
-lower priority than the core.
-
-**The ban line itself:** `src/v4/test/claim/extdeps/coordination_claims.dag:18`
-— "reflection banned; decl-shape mirrors are 2FA-for-code."
-
-**Why this is debt (live invariants).** Each mirror is a *second authority* for
-a fact the declaration already owns — INVARIANTS P2 "Parallel authority" and
-MODELING M2/M7. Cost-of-change is > 1: adding an arm to `Connective` forces edits
-in `node.dag`, `coverage.dag`, and any roster keyed on it. The marks are valid
-🟡 only because they bind a named dissolution trigger — *this* primitive
-(P5 "Scaffold without dissolution trigger"). `gunbc#4759` is a **closed
-label-hygiene re-anchor, not prior art** — the capability is greenfield.
-
----
-
-## 2. The ban — read carefully, then steelmanned
-
-`coordination_claims.dag:18` bans reflection because **decl-shape mirrors are
-"2FA-for-code"**: a second, *independently authored* statement of the arm set
-that catches drift. Naively deleting the mirrors and deriving from the
-declaration removes that second factor. The design must not hand-wave this.
-
-The 2FA protects against **two distinct drift classes**, and they have
-*different* answers:
-
-- **(ii) declaration ↔ consumer drift.** A consumer's variant handling silently
-  goes stale when an arm is added (the classic non-exhaustive-handling bug). The
-  mirror catches it because a hand-written exhaustive `match` over the coproduct
-  *fails to compile* until updated — that compile error is the real "second
-  factor."
-- **(i) declaration ↔ mechanism drift (self-hosting).** The deeper concern: the
-  compiler is partly self-hosted (`.dag` → emitted stage0 Rust). If the
-  reflection *mechanism* has a bug — drops an arm, miscounts under a generic
-  instantiation, the lowering is wrong — a consumer relying solely on reflection
-  silently inherits the wrong arm set, and nothing catches it, because the only
-  authority is the broken one. The hand-mirror is an **independent witness** of
-  the same fact, authored by a human reading the declaration; comparing the two
-  catches mechanism bugs.
-
-Both are real. The design answers each — and the answers are *stronger* than the
-mirrors, not weaker.
-
----
-
-## 3. Where reflection attaches (M9 — DFS the concept DAG)
-
-**No new top-level concept. No substrate extension.** A coproduct is *already*
-a substrate citizen: in `std/node.dag` a sum type is a node with
-`kind: TypeNode { connective: Disj }`, and `connective_edge_discipline(Disj) =
-LabeledEdges` — so **its arms are its named-edge children** (`Edge { label:
-Named { name: armLabel }, target: armPayload }`). Enumerating arms is therefore
-a *structural query over a `Disj` node's edges* — the same shape as the existing
-`named_edge_target_lookup`, `node_subtree_nodes`, `all_edges_named` in
-`std/node.dag`. The v3 reflection already has `disj_variant_ty` ("look up a
-variant type in a Disj coproduct by label"), confirming arms are label→payload
-edges.
-
-So the primitive **attaches to `v4.std.node`** as a derived operation over the
-existing `Disj` connective. INVARIANTS P2 prescribes extending substrate
-reflection *before* migrating consumers; here that means adding the capability to
-**v4 `.dag` substrate** (`std/node.dag`), not extending the v3-Rust
-`substrate_reflection` seed (`lens_declaration_apply.rs` — see §4.3). INVARIANTS
-§"Reflection evidence" (:385) "extend the `substrate_reflection` submodule"
-refers to that v3 seed submodule; this lane's deliverable is the v4 analogue. It
-adds **no 7th connective and no 6th behavior**, so it does not trip the THESIS
-substrate-extension stop-signal.
-
-This is the **Track 2 cure** named in the L1.1 anchor: "the substrate lets you
-*declare* an algebraic type but does not *derive its canonical operations*, so
-workers hand-roll discriminants and catamorphisms." Coproduct-arm reflection is
-the missing derived operation.
-
----
-
-## 4. The sanctioned mechanism
-
-### 4.1 Reflected fact carrier (std/node.dag)
-
-```dag
-// A single reflected arm of a closed coproduct (Disj node).
-type CoproductArm {
-  label: Symbol        // the arm's name (the Named edge label)
-  payload: NodeShape   // the arm's payload type; NoEdges-shaped for nullary arms
-}
-```
-
-`CoproductArm` is a fact-bundle (named edges, M1) — it carries the two facts the
-declaration states about an arm and nothing more.
-
-### 4.2 Core projections (compile-time, deterministic, closed-only)
-
-- **`coproduct_arms(T) -> List<CoproductArm>`** — the full reflected arm list of
-  a *closed, declared* coproduct type `T`, in declaration order.
-- **`coproduct_arm_keys(T) -> List<Symbol>`** — `map(coproduct_arms(T), .label)`.
-  The key projection that replaces every hand-written key-enum + key-list mirror
-  (`ConnectiveCoproductVariant`, `TestClaimCoproductVariant`, …).
-- **`coproduct_nullary_inhabitants(T) -> List<T>`** — for coproducts whose arms
-  are **all nullary** (no payload), the value-level inhabitant list. This is the
-  total replacement for `behavior_coproduct_variants() -> List<Behavior>` and
-  `impossible_bug_class_coproduct_variants()`. For a coproduct with **any
-  payload-carrying arm**, this **fails closed** with a typed diagnostic — the
-  primitive never fabricates an inhabitant for a payload arm (C-1/C-9; a default
-  payload would be a fabrication). Payload-arm coproducts get keys, not values.
-- **`common_field_projection(T, field) -> ...`** *(Phase-2b — split out per
-  design-sign Q2; lands after C1 + the corrected gate are green on
-  Connective/Behavior).* When *every* arm of `T` carries a field of the same name
-  and type (e.g. `TestClaim.label`, `TestClaim.anchor`,
-  `TestClaim.classification`), the field is projectable generically. This
-  replaces `test_claim_label()` and the `test_claim_*`-family common-field
-  hand-projections. If an arm lacks the field, it fails closed (the field is not
-  common).
-
-**Discipline of the primitive** (all enforced, not aspirational):
-
-1. **Compile-time only.** `T` is a statically-known, closed type; the arm set is
-   resolved from its declaration at compile time. No runtime reflection. No
-   open-set reflection (M4 — open sets stay diagnostics, not enumerations).
-2. **No execution semantics, no narrowing.** Same posture as the blessed
-   `reflect_program_dag_nodes_in_file`: a complete, deterministic structural
-   projection, no per-consumer narrowing (INVARIANTS §"Reflection evidence").
-3. **Fail-closed everywhere.** Non-coproduct `T`, open `T`, missing common
-   field, or value-inhabitant request on a payload arm → typed diagnostic via
-   `Outcome`, never a fabricated default (P3).
-
-### 4.3 Compiler support (Phase-2 scope; named here, not built)
-
-The primitive requires the compiler to resolve a type reference `T` at its call
-site to the declaration's `Disj` node and project its arm edges. This
-resolution-and-projection is the **primary Phase-2 build risk** and is exactly
-what the §5 conformance gate protects.
-
-**Layer-boundary precision (design-sign condition 2).** This is **new v4
-substrate**, *analogous to* — not an extension of — the existing v3-Rust
-`substrate_reflection` submodule (`lens_declaration_apply.rs`). That v3 surface
-is **bootstrap seed**: per src/v3/SELF_HOSTING.md the seed *shrinks* while v4
-substrate *grows*. The v4 primitive is authored as v4 `.dag` substrate + v4
-compiler support; it does not inherit from or call the v3 seed. The v3 reflection
-is relevant only as (a) a shape precedent and (b) a *cross-generation* check
-factor in the gate (§5.2), never as the home of the new capability.
-
----
-
-## 5. The 2FA crux — preserved, and strengthened
-
-### 5.1 Class (ii) drift is *eliminated*, not caught
-
-For structurally-determined facts (arm lists, keys, common-field projection,
-structural equality / discriminant), reflection removes the *second list
-entirely*. There is nothing to drift from — the consumer derives from the
-declaration. INVARIANTS P2: "If the canonical answer doesn't exist yet, extend
-the substrate reflection first, then migrate consumers." Making drift
-*unrepresentable* strictly dominates *catching* it. **No 2FA replacement is
-needed for class (ii); the drift class is dissolved.**
-
-### 5.2 Class (i) drift — the by-execution conformance gate (corrected per design-sign Q1)
-
-The mechanism-drift concern is answered by a **by-execution conformance gate**:
-for every gated coproduct, the reflection output must equal an
-**independently-derived** arm set, where "independent" means *derived through a
-distinct lowering path* — not merely "a different function." A bug that corrupts
-the reflection builtin must NOT also corrupt the witness, or the gate is
-**circular** and passes falsely (the self-hosting class-(i) drift the ban
-guards). The factors below are graded by that independence test.
-
-**Why the obvious factor fails (the load-bearing correction).** The natural
-candidate — v4 type-checker match-exhaustiveness — is **NOT independent on its
-own.** v4 inference and the v4 reflection builtin **both resolve `T` to the same
-parsed `Disj` node**; a common-mode resolver/parse arm-drop corrupts *both*
-sides, and the gate passes falsely. So exhaustiveness-count is **common-mode with
-the thing it is checking** and cannot be the gate's independent factor.
-Similarly, the v3 `reflect_program_dag_nodes_in_file` posture is **not a
-pre-existing factor**: it is v3-Rust *seed*, partial, and INVARIANTS:381-383
-explicitly tags it "not yet a closed mechanical theorem … not a substitute for a
-future full conformance gate." It is the gate we are **building**, not one we can
-lean on.
-
-**The gate (REQUIRED).** For every gated coproduct, at least one of the
-following *path-distinct* witnesses must hold by execution:
-
-- **Path 3 — syntactic arm key-set (primary, required for non-roster
-  coproducts).** A parser/syntactic derivation of the arm **labels** — reading the
-  `|`-separated arm names at the grammar level, *before* the shared resolver the
-  reflection builtin uses — and **set-comparing** them to `coproduct_arm_keys(T)`.
-  Because it is computed on a distinct (syntactic) path, a resolver/lowering bug
-  in the reflection builtin does not corrupt it. A cardinality count alone would
-  **not** suffice: `|children| == |keys|` passes falsely on arity-preserving
-  relabel (wrong key, right count) — squarely inside class-(i) mechanism drift.
-  Key-set equality catches drop, add, and relabel. This is the genuine second
-  factor.
-- **Cross-generation check (where v3 covers the carrier).** For carriers the v3
-  seed reflects, `v4 coproduct_arm_keys(Behavior) == v3 reflect_behavior_list`
-  arm set. Two generations, two independent code paths — a strong factor for the
-  Behavior/Connective carriers v3 already covers, usable in addition to Path 3.
-- **Frontier-discovery equality (roster clusters only — the D1c seam).** The CI
-  roster cluster has `affected_set_ci_runner.dag:287`
-  `ci_runner_selected_matches_frontier_discovered`: "discovered == roster:
-  selection output must equal explicit frontier discovery, not hand-roster
-  laundering." For those clusters the witness is **reflection-generated roster ==
-  independently frontier-discovered set** — naturally path-independent
-  (consumer-side derivation) and the strongest factor *there*, but roster-scoped,
-  not a general gate.
-
-**Explicitly rejected as the gate's independent factor:** v4 exhaustiveness-count
-alone (common-mode), and the v3 reflection posture alone (the gate being built).
-The exhaustiveness check may still run as a *consistency* signal, but it does not
-discharge the independence obligation.
-
-This corrected gate is **strictly stronger** than the hand-mirrors: it is checked
-**by execution**, it covers **every** gated coproduct via a genuinely
-path-distinct witness, and it is **one** gate to maintain instead of N driftable
-lists. The mirrors were a weaker, partial, by-inspection form of it.
-
-### 5.3 Per-arm semantics — fail-closed total maps keyed by the reflected set
-
-Some consumers are **not** structurally determined: they assign a value *per arm
-that is not recoverable from the arm's shape* (e.g.
-`impossible_bug_class_from_diagnostic_reason`, per-arm cost/complexity tables).
-Reflection cannot derive these, and silently defaulting them would be a C-8/M5
-fabrication. These do **not** dissolve into pure reflection. Instead they
-**reuse the existing `TotalMap<K,V>`** (`std/collection.dag:165`, `lookup:
-fn(K) -> V`) — *no* new carrier (declaring a `TotalArmMap<T,V>` parallel to
-`TotalMap` would be the very parallel-authority anti-pattern this lane kills, per
-design-sign Q3 / M9). "Keyed by the reflected set" is **not a type** — it is a
-**conformance witness**: `domain(map) == coproduct_arm_keys(T)`. A
-smart-constructor that builds a `TotalMap` and emits that domain-equality witness
-is the sanctioned shape. The consumer supplies the codomain; a missing key is a
-**typed diagnostic at build time**, not a silent fall-through (P3 "Case
-enumeration for open sets" → typed table; M7 data-table single-authority).
-
-This **preserves and strengthens** the class-(ii) exhaustiveness 2FA: "did you
-handle the new arm?" moves from "a hand-written `match` fails to compile" to
-"the substrate proves the table is total against the canonical arm set." Adding
-an arm grows the reflected domain → the table is now missing a key → fail-closed.
-The reviewer still consciously supplies the new arm's semantics — but there is no
-longer a *second arm list* to forget.
-
----
-
-## 6. Consumer taxonomy (drives Phase 3)
-
-Every census entry sorts into exactly one bucket:
-
-| Bucket | Mechanism | Census members |
-|---|---|---|
-| **C1 — pure enumeration** (arm list / keys / nullary inhabitants) | `coproduct_arm_keys` / `coproduct_nullary_inhabitants` + conformance gate | `connective_coproduct_variant_keys`, `behavior_coproduct_variants`, `impossible_bug_class_coproduct_variants`, `TestClaimCoproductVariant` key-enum + `test_claim_coproduct_variant`, `coproduct_exhaustiveness.dag` arm checks |
-| **C2 — common-field projection** (field present on every arm) | `common_field_projection` *(Phase-2b)* | `test_claim_label` and the `test_claim_*` common-field family |
-| **C3 — structural equality / discriminant** | derived discriminant over arms (L1.1 lens target) | `connective_eq`/`behavior_eq`/`test_claim_coproduct_variant_eq` (broader family) |
-| **C4 — per-arm semantics** (value not in the shape) | fail-closed **`TotalMap<K,V>`** (std/collection.dag:165) + `domain == coproduct_arm_keys(T)` witness | `impossible_bug_class_from_diagnostic_reason`, `coverage.dag:947` reason membership, `lens_cost/*` & `lens_complexity/*` arm tables |
-| **C5 — item rosters** (lists kept in sync with a registry/frontier) | reflection-generated roster + **D1c :287 equality witness** | `manual_corpus_roster`, `affected_set_ci_runner` / `affected_testgen_ci_runner` / `lens_ownership/subject_roster` (swift-stag-552 D1c) |
-
-C4 honestly does **not** vanish into pure reflection — it dissolves the *arm
-list* duplication (the total-map's domain is reflected) while keeping the
-genuine per-arm decision as single-authority data. Naming this honestly is part
-of the design: the falsifier "marks → 0" is met because each mark's *mirror*
-dissolves, even where a (now fail-closed, single-authority) semantic table
-remains.
-
----
-
-## 7. The ban-lift (the exact ask)
-
-**Lift the `coordination_claims.dag:18` reflection ban for, and only for, the
-following mechanism:**
-
-> Deterministic, **compile-time** reflection over a **closed, declared
-> coproduct** type that projects its **arm keys, common fields, and (for
-> all-nullary coproducts) value inhabitants**, where:
-> 1. every consumer migration deletes its own dissolve-on-arrival mirror in the
->    **same PR** (per each mark's forbidden-clause);
-> 2. the mechanism is covered by a **tree-wide by-execution conformance gate**
->    (§5.2) that proves reflection output equals an independently-derived arm
->    set; and
-> 3. **per-arm-semantic** consumers (C4) become **fail-closed total maps keyed
->    by the reflected arm set**, never silent defaults.
-
-**Stays banned** (explicitly out of scope of this lift):
-- runtime / dynamic reflection;
-- reflection over **open** sets (M4 — open sets are diagnostics, not enumerable);
-- fabricating inhabitants for **payload-carrying** arms (C-1/C-9);
-- using reflection to **silently default** per-arm semantics (C-8/M5);
-- any reflected projection **not** covered by the §5.2 conformance gate (an
-  ungated reflection consumer is exactly the single-broken-authority hazard the
-  ban was protecting against).
-
-Rationale for a *scoped* lift rather than a blanket repeal: the ban's protective
-intent (2FA against mechanism drift) is **satisfied by construction** within
-this scope (§5) and **violated** outside it. The lift encodes the ban's own
-anticipated "proper mechanism," not its repeal.
-
----
-
-## 8. Invariant alignment
-
-- **P1 Faithfulness.** Arms are read from the declaration; no heuristic, no
-  ungrounded fact. The primitive is the missing derived operation, not a second
-  authority.
-- **P2 Boundary.** Single authority (the declaration); parallel mirrors deleted
-  in the same change; reflection exposed through the declared `std/node` surface.
-- **P3 Fail-closed.** Non-coproduct / open / payload-inhabitant / missing-common-
-  field / missing-total-map-key all produce typed diagnostics; no fabrication.
-- **P4 Decidability.** Compile-time, bounded fold over a finite Disj node's
-  edges; terminates by construction. No new connective/behavior; no runtime
-  capability.
-- **P5 Dissolution.** Net mirror count strictly decreases; every migration PR is
-  debt-negative; the falsifier (15 core + ban line + ~12 family marks) → 0.
-
----
-
-## 9. Phasing
-
-- **Phase 1 (this doc).** Design + ban-lift proposal. Gate: snappy-crab-849
-  DESIGN-SIGN + operator BAN-LIFT ruling.
-- **Phase 2a (gated).** Build `CoproductArm` + `coproduct_arms` /
-  `coproduct_arm_keys` / `coproduct_nullary_inhabitants` in `std/node.dag` (new
-  v4 substrate) + the compiler resolution support, and the **corrected §5.2
-  conformance gate** (Path 3 syntactic arm key-set + cross-generation where v3 covers).
-  Inhabit on real coproducts first (`Connective`/`Behavior`) with the gate green
-  by execution before any consumer migrates (facts-before-abstraction).
-- **Phase 2b (gated, after 2a green).** Add `common_field_projection` (the
-  `test_claim_*` common-field family's path).
-- **Phase 3 (gated, may spawn lean per-cluster workers).** Migrate consumers
-  cluster-by-cluster in taxonomy order: C1 std mirrors → C1/C3 generated corpus
-  exhaustiveness/algebra → C5 manual corpus roster → C5 CI rosters (swift-stag-552
-  D1c, with the :287 equality witness). Each PR deletes its own
-  dissolve-on-arrival marks. Re-anchor the marks' `design-dissolution-lens.md
-  L1.1` citation to this doc.
-
----
-
-## 10. Design-sign resolutions (snappy-crab-849, CONDITIONAL sign — issuecomment-4700373336)
-
-1. **Conformance-gate independence — RESOLVED (the load-bearing condition).**
-   v4 exhaustiveness-count alone is **NOT** an independent factor — it is
-   common-mode with the reflection builtin (both resolve `T` to the same parsed
-   `Disj` node), and the v3 reflection posture is the gate being *built*, not a
-   pre-existing factor. **REQUIRED:** the gate's independent factor is the
-   **syntactic arm key-set (Path 3)** — `|`-separated arm labels from the parse
-   tree set-compared to `coproduct_arm_keys(T)`, not a cardinality count — for
-   every gated coproduct, and/or the **cross-generation check** (`v4
-   coproduct_arm_keys == v3 reflect_behavior_list`) where v3 covers the carrier;
-   rosters additionally use the frontier-discovery equality. Rewritten in §5.2.
-   Exhaustiveness may run as a consistency signal but does not discharge
-   independence.
-2. **Common-field projection — RESOLVED: split to Phase-2b.** Land C1 + the
-   corrected gate on `Connective`/`Behavior` green-by-execution first; add
-   `common_field_projection` after. Reflected in §4.2 / §6 / §9.
-3. **C4 carrier — RESOLVED: reuse `TotalMap<K,V>`** (`std/collection.dag:165`).
-   No `TotalArmMap`. "Keyed by reflected set" is a conformance witness
-   (`domain == coproduct_arm_keys(T)`), not a new type; smart-constructor emits
-   the witness. Reflected in §5.3 / §6.
-4. **Value-inhabitant boundary — CONFIRMED.** All-nullary only;
-   payload arms → fail closed; no inhabit-with-holes.
-
-**Doc-precision condition (condition 2) — APPLIED:** the primitive is **new v4
-substrate**, analogous to (not an extension of) the v3-Rust `substrate_reflection`
-seed, which shrinks while v4 grows (§4.3).
-
-**§5.2 re-read — CONFIRMED (snappy-crab-849, post-0071c645):** design-sign
-carries on the corrected gate. Binding sharpening applied: Path 3 is a **syntactic
-arm key-set** (label set-compared to `coproduct_arm_keys(T)`), not a cardinality
-count — count alone passes falsely on arity-preserving relabel. With Path 3 as
-key-set, **no third path is required** for non-roster/non-v3 coproducts; it
-discharges the independence obligation alone. Cross-generation is additive where
-v3 covers the carrier; frontier-discovery is roster-scoped only. The 2FA guarantee
-proves in Phase-2 when Path 3 (key-set) lands GREEN before any consumer migrates.
-
-**Operator gate (still open):** BAN-LIFT ruling (routed via zesty-swift-79),
-predicated on this corrected 3-factor gate.
diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index f4d4ab1b7a5..ade015db7c5 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -1,14 +1,15 @@
-//! Coproduct-arm reflection — Phase 2a compile-time enumeration (R-reflect).
+//! Coproduct-arm reflection — Phase 2a compile-time key enumeration (R-reflect).
 //!
-//! Reflection path: resolve `type_name` to a closed `Disj` in the compiled module graph.
-//! Path 3 (syntactic): scan the declaring source for `|`-separated arm labels before any
-//! shared resolver (design-coproduct-arm-reflection.md §5.2).
+//! Bootstrap seam: v2 interpreter intercept over the resolved compile graph (Disj walk).
+//! Path 3 (syntactic): raw source-text scan of `|`-separated arm labels — independent of the
+//! Disj resolver (design-coproduct-arm-reflection.md §5.2).
+//!
+//! Dissolve-on-arrival: substrate compiler builtin once type-name → resolved Disj Node is
+//! expressible in v4 `.dag` (analogous to node_labeled_child_edges for value-level queries).
 
-use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::v2_compiler_infer_items::ItemKind;
-use crate::v2_compiler_infer_types::child_type_node;
 use crate::v2_interpreter::{InterpContext, InterpError, InterpResult, Value};
 use crate::v2_std_core::{authored_name_at, Connective, Node};
 
@@ -74,15 +75,9 @@ fn symbol_list_value(labels: &[String]) -> Value {
     crate::v2_interpreter::list_value(items)
 }
 
-fn variant_is_nullary(variant: &Rc<Node>, _ctx: &InterpContext) -> bool {
-    let payload = child_type_node(variant.clone());
-    match payload.connective {
-        Connective::NoConnective => payload.children.is_empty(),
-        Connective::Conj => payload.children.is_empty(),
-        _ => false,
-    }
-}
-
+/// Bootstrap only: resolve declaring source path via cwd walk + optional GUNBC_ROOT.
+/// Dissolve-on-arrival: compile-graph span.file is the sole authority once claim-run
+/// transport no longer needs off-disk reads for Path-3 witnesses.
 fn resolve_source_file_path(file: &str) -> InterpResult<String> {
     let path = std::path::Path::new(file);
     if path.is_absolute() && path.exists() {
@@ -126,8 +121,8 @@ pub fn syntactic_coproduct_arm_labels(file: &str, type_name: &str) -> InterpResu
 
 /// Scan source for `type <name> = <arm> (| <arm>)*` without invoking the type resolver.
 fn extract_type_sum_arm_labels(source: &str, type_name: &str) -> Option<Vec<String>> {
+    let start = find_type_decl_start(source, type_name)?;
     let needle = format!("type {type_name}");
-    let start = source.find(&needle)?;
     let after_type = &source[start + needle.len()..];
     let eq_rel = after_type.find('=')?;
     let mut rest = after_type[eq_rel + 1..].trim_start();
@@ -158,6 +153,30 @@ fn extract_type_sum_arm_labels(source: &str, type_name: &str) -> Option<Vec<Stri
     }
 }
 
+/// Word-boundary match: `type Connective` must not match `type ConnectiveCoproductVariant`.
+fn find_type_decl_start(source: &str, type_name: &str) -> Option<usize> {
+    let needle = format!("type {type_name}");
+    let mut search_from = 0usize;
+    while let Some(rel) = source[search_from..].find(&needle) {
+        let start = search_from + rel;
+        let after = start + needle.len();
+        let boundary_ok = source
+            .as_bytes()
+            .get(after)
+            .is_none_or(|b| matches!(*b, b' ' | b'=' | b'{'));
+        let prefix_ok = start == 0
+            || source
+                .as_bytes()
+                .get(start.saturating_sub(1))
+                .is_some_and(|b| b.is_ascii_whitespace());
+        if boundary_ok && prefix_ok {
+            return Some(start);
+        }
+        search_from = start + 1;
+    }
+    None
+}
+
 fn read_identifier_prefix(s: &str) -> Option<(String, &str)> {
     let mut end = 0;
     for (i, ch) in s.char_indices() {
@@ -193,104 +212,35 @@ fn skip_braced(s: &str) -> Option<&str> {
 pub fn eval_coproduct_arm_keys(
     ctx: &InterpContext,
     args: &[(Option<String>, Value)],
-) -> InterpResult<Option<Value>> {
+) -> InterpResult<Value> {
     let type_name = expect_symbol(args.first().map(|(_, v)| v), "coproduct_arm_keys")?;
     let (item, _) = type_item_by_name(ctx, type_name)?;
     let labels = disj_variant_labels(item, ctx)?;
-    Ok(Some(symbol_list_value(&labels)))
+    Ok(symbol_list_value(&labels))
 }
 
 pub fn eval_syntactic_coproduct_arm_keys(
     ctx: &InterpContext,
     args: &[(Option<String>, Value)],
-) -> InterpResult<Option<Value>> {
-    let type_name = expect_symbol(args.first().map(|(_, v)| v), "syntactic_coproduct_arm_keys")?;
+) -> InterpResult<Value> {
+    let type_name = expect_symbol(
+        args.first().map(|(_, v)| v),
+        "syntactic_coproduct_arm_keys",
+    )?;
     let (_, file) = type_item_by_name(ctx, type_name)?;
     let labels = syntactic_coproduct_arm_labels(&file, type_name)?;
-    Ok(Some(symbol_list_value(&labels)))
+    Ok(symbol_list_value(&labels))
 }
 
-pub fn eval_coproduct_arms(
+/// Mechanism-drift probe: drop the last Disj child and compare key sets (test-only).
+pub fn eval_coproduct_arm_keys_with_dropped_last_arm(
     ctx: &InterpContext,
-    args: &[(Option<String>, Value)],
-) -> InterpResult<Option<Value>> {
-    let type_name = expect_symbol(args.first().map(|(_, v)| v), "coproduct_arms")?;
-    let (item, _) = type_item_by_name(ctx, type_name)?;
-    let si = ctx.source_indices();
-    let labels = disj_variant_labels(item, ctx)?;
-    let mut arms = Vec::with_capacity(labels.len());
-    for (variant, label) in item.children.iter().zip(labels.iter()) {
-        let payload_shape = if variant_is_nullary(variant, ctx) {
-            Value::Variant {
-                type_name: ctx.sym("NodeKind"),
-                variant_name: ctx.sym("ComputationNode"),
-                fields: Rc::new(HashMap::from([(
-                    ctx.sym("behavior"),
-                    Value::Variant {
-                        type_name: ctx.sym("Behavior"),
-                        variant_name: ctx.sym(label),
-                        fields: Rc::new(HashMap::new()),
-                    },
-                )])),
-            }
-        } else {
-            let payload = child_type_node(variant.clone());
-            Value::Variant {
-                type_name: ctx.sym("NodeKind"),
-                variant_name: ctx.sym("TypeNode"),
-                fields: Rc::new(HashMap::from([(
-                    ctx.sym("connective"),
-                    Value::Variant {
-                        type_name: ctx.sym("Connective"),
-                        variant_name: ctx.sym(&authored_name_at(si.clone(), payload.clone())),
-                        fields: Rc::new(HashMap::new()),
-                    },
-                )])),
-            }
-        };
-        arms.push(Value::Record {
-            type_name: ctx.sym("CoproductArm"),
-            fields: Rc::new(HashMap::from([
-                (ctx.sym("label"), Value::Str(label.clone())),
-                (
-                    ctx.sym("payload"),
-                    Value::Record {
-                        type_name: ctx.sym("NodeShape"),
-                        fields: Rc::new(HashMap::from([(ctx.sym("kind"), payload_shape)])),
-                    },
-                ),
-            ])),
-        });
-    }
-    Ok(Some(crate::v2_interpreter::list_value(arms)))
-}
-
-pub fn eval_coproduct_nullary_inhabitants(
-    ctx: &InterpContext,
-    args: &[(Option<String>, Value)],
-) -> InterpResult<Option<Value>> {
-    let type_name = expect_symbol(
-        args.first().map(|(_, v)| v),
-        "coproduct_nullary_inhabitants",
-    )?;
+    type_name: &str,
+) -> InterpResult<Value> {
     let (item, _) = type_item_by_name(ctx, type_name)?;
-    let si = ctx.source_indices();
-    for variant in item.children.iter() {
-        if !variant_is_nullary(variant, ctx) {
-            return Err(InterpError::TypeError {
-                msg: format!(
-                    "coproduct_nullary_inhabitants: arm `{}` carries a payload — fail closed",
-                    authored_name_at(si.clone(), variant.clone())
-                ),
-            });
-        }
-    }
-    let inhabitants: Vec<Value> = item
-        .children
-        .iter()
-        .map(|variant| Value::Str(authored_name_at(si.clone(), variant.clone())))
-        .collect();
-    Ok(Some(crate::v2_interpreter::list_value(inhabitants)))
+    let mut labels = disj_variant_labels(item, ctx)?;
+    labels.pop();
+    Ok(symbol_list_value(&labels))
 }
 
 #[cfg(test)]
@@ -324,4 +274,18 @@ mod tests {
         let arms = extract_type_sum_arm_labels(&source, "Behavior").expect("Behavior arms");
         assert_eq!(arms, vec!["Value", "Transform", "Branch", "Loop", "Bind"]);
     }
+
+    #[test]
+    fn syntactic_extractor_rejects_connective_prefix_of_longer_type_name() {
+        let source =
+            "type ConnectiveCoproductVariant = Foo | Bar\ntype Connective = Atom | Conj\n";
+        assert_eq!(
+            extract_type_sum_arm_labels(source, "ConnectiveCoproductVariant").expect("variant"),
+            vec!["Foo", "Bar"]
+        );
+        assert_eq!(
+            extract_type_sum_arm_labels(source, "Connective").expect("Connective"),
+            vec!["Atom", "Conj"]
+        );
+    }
 }
diff --git a/src/v2/stage0/src/v2_interpreter.rs b/src/v2/stage0/src/v2_interpreter.rs
index 4347b29e5ea..9a5e43a750f 100644
--- a/src/v2/stage0/src/v2_interpreter.rs
+++ b/src/v2/stage0/src/v2_interpreter.rs
@@ -2131,31 +2131,14 @@ fn eval_call(node: &Rc<Node>, env: &Rc<Env>, ctx: &InterpContext) -> InterpResul
         })
         .collect::<InterpResult<_>>()?;
 
-    // R-reflect Phase 2a: compile-time coproduct-arm reflection (intercept before module fn).
+    // R-reflect Phase 2a: compile-time coproduct-arm reflection (intercept-only; stub bodies
+    // self-recurse fail-closed if bypassed — see std/node.dag).
     match func_name.as_str() {
         "coproduct_arm_keys" => {
-            if let Some(v) = crate::coproduct_reflection::eval_coproduct_arm_keys(ctx, &args)? {
-                return Ok(v);
-            }
+            return crate::coproduct_reflection::eval_coproduct_arm_keys(ctx, &args);
         }
         "syntactic_coproduct_arm_keys" => {
-            if let Some(v) =
-                crate::coproduct_reflection::eval_syntactic_coproduct_arm_keys(ctx, &args)?
-            {
-                return Ok(v);
-            }
-        }
-        "coproduct_arms" => {
-            if let Some(v) = crate::coproduct_reflection::eval_coproduct_arms(ctx, &args)? {
-                return Ok(v);
-            }
-        }
-        "coproduct_nullary_inhabitants" => {
-            if let Some(v) =
-                crate::coproduct_reflection::eval_coproduct_nullary_inhabitants(ctx, &args)?
-            {
-                return Ok(v);
-            }
+            return crate::coproduct_reflection::eval_syntactic_coproduct_arm_keys(ctx, &args);
         }
         _ => {}
     }
diff --git a/src/v4/std/node.dag b/src/v4/std/node.dag
index 824e371e0a7..1ce54e52565 100644
--- a/src/v4/std/node.dag
+++ b/src/v4/std/node.dag
@@ -43,28 +43,20 @@ type Behavior
   | Bind
 
 
-// R-reflect Phase 2a — coproduct-arm reflection substrate (docs/design-coproduct-arm-reflection.md §4).
-// Compile-time only: arm keys/projections resolve from closed Disj declarations; bodies are
-// intercepted by the v2 reflection builtin (fail-closed stubs if intercept is bypassed).
-type CoproductArm {
-  label: Symbol
-  payload: NodeShape
-}
-
+// R-reflect Phase 2a — coproduct-arm reflection substrate (design-coproduct-arm-reflection.md §4).
+// Compile-time only: arm keys resolve from closed Disj declarations at the v2 interpreter
+// intercept (bootstrap Rust in src/v2/stage0/src/coproduct_reflection.rs). Dissolve-on-arrival:
+// substrate compiler builtin once type-name → resolved Disj is expressible in v4 .dag.
+// 🟡 gated — feature:coproduct-reflection-intercept-only — bind gunbc#4863 — dissolve-on-arrival:
+// substrate reflection builtin; forbidden: silent empty-list default ([]) on bypass.
 fn coproduct_arm_keys(type_name: Symbol) -> List<Symbol> {
-  []
+  coproduct_arm_keys(type_name: type_name)
 }
 
+// 🟡 gated — feature:coproduct-reflection-intercept-only — bind gunbc#4863 — dissolve-on-arrival:
+// substrate reflection builtin; forbidden: silent empty-list default ([]) on bypass.
 fn syntactic_coproduct_arm_keys(type_name: Symbol) -> List<Symbol> {
-  []
-}
-
-fn coproduct_arms(type_name: Symbol) -> List<CoproductArm> {
-  []
-}
-
-fn coproduct_nullary_inhabitants(type_name: Symbol) -> List<Symbol> {
-  []
+  syntactic_coproduct_arm_keys(type_name: type_name)
 }
 
 
diff --git a/src/v4/test/claim/manual/coproduct_reflection_conformance.dag b/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
index 3b96710ff9c..257b5364289 100644
--- a/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
+++ b/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
@@ -11,7 +11,6 @@ import v4.std.logic { Bool }
 import v4.std.node {
   Symbol,
   coproduct_arm_keys,
-  coproduct_nullary_inhabitants,
   syntactic_coproduct_arm_keys
 }
 
@@ -43,13 +42,18 @@ fn witness_behavior_arm_key_set_path3() -> Bool {
 }
 
 
-fn witness_behavior_nullary_inhabitants_count() -> Bool {
-  count(coproduct_nullary_inhabitants(type_name: reflect_behavior_type)) == 5
+// Discrimination: Connective and Behavior arm key-sets must differ (proves bag_eq is not vacuous).
+fn witness_connective_behavior_arm_sets_are_distinct() -> Bool {
+  !bag_eq(
+    xs: coproduct_arm_keys(type_name: reflect_connective_type),
+    ys: coproduct_arm_keys(type_name: reflect_behavior_type),
+    eq: symbol_eq
+  )
 }
 
 
 fn coproduct_reflection_conformance_holds() -> Bool {
   witness_connective_arm_key_set_path3()
     && witness_behavior_arm_key_set_path3()
-    && witness_behavior_nullary_inhabitants_count()
+    && witness_connective_behavior_arm_sets_are_distinct()
 }
diff --git a/src/v4/workflow/lens_ci_gate.dag b/src/v4/workflow/lens_ci_gate.dag
index defec6a6736..a5f3fd2c482 100644
--- a/src/v4/workflow/lens_ci_gate.dag
+++ b/src/v4/workflow/lens_ci_gate.dag
@@ -78,6 +78,31 @@ data lens_ci_claim_run_row_complexity_gate_budget_roster_completeness: LensCiCla
   function: "complexity_budget_roster_family_gate_holds"
 }
 
+// R-reflect Phase 2a: Path-3 key-set conformance (2FA proof) — Connective/Behavior FIRST.
+data lens_ci_claim_run_row_coproduct_reflection_connective_path3: LensCiClaimRunRow = LensCiClaimRunRow {
+  label: "coproduct_reflection/connective_path3",
+  entry: "src/v4/test/claim/manual/coproduct_reflection_conformance.dag",
+  function: "witness_connective_arm_key_set_path3"
+}
+
+data lens_ci_claim_run_row_coproduct_reflection_behavior_path3: LensCiClaimRunRow = LensCiClaimRunRow {
+  label: "coproduct_reflection/behavior_path3",
+  entry: "src/v4/test/claim/manual/coproduct_reflection_conformance.dag",
+  function: "witness_behavior_arm_key_set_path3"
+}
+
+data lens_ci_claim_run_row_coproduct_reflection_distinct_arm_sets: LensCiClaimRunRow = LensCiClaimRunRow {
+  label: "coproduct_reflection/distinct_arm_sets",
+  entry: "src/v4/test/claim/manual/coproduct_reflection_conformance.dag",
+  function: "witness_connective_behavior_arm_sets_are_distinct"
+}
+
+data lens_ci_claim_run_row_coproduct_reflection_conformance: LensCiClaimRunRow = LensCiClaimRunRow {
+  label: "coproduct_reflection/conformance",
+  entry: "src/v4/test/claim/manual/coproduct_reflection_conformance.dag",
+  function: "coproduct_reflection_conformance_holds"
+}
+
 data lens_ci_claim_run_rows: List<LensCiClaimRunRow> = [
   lens_ci_claim_run_row_cost_atom_zero,
   lens_ci_claim_run_row_synthesis_polynomial_dominates_linear,
@@ -86,7 +111,11 @@ data lens_ci_claim_run_rows: List<LensCiClaimRunRow> = [
   lens_ci_claim_run_row_provenance_occurrence_id_model,
   lens_ci_claim_run_row_provenance_parse_stamp_span_index,
   lens_ci_claim_run_row_complexity_gate_source_bridged_add,
-  lens_ci_claim_run_row_complexity_gate_budget_roster_completeness
+  lens_ci_claim_run_row_complexity_gate_budget_roster_completeness,
+  lens_ci_claim_run_row_coproduct_reflection_connective_path3,
+  lens_ci_claim_run_row_coproduct_reflection_behavior_path3,
+  lens_ci_claim_run_row_coproduct_reflection_distinct_arm_sets,
+  lens_ci_claim_run_row_coproduct_reflection_conformance
 ]
 
 // Uniform CI claim-gate transport: one TSV line per row, `label\tentry\tfunction`.

From 6152c8995a28e8b0ca251c9dae3a33e246c5c2c1 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 03:59:02 +0000
Subject: [PATCH 14/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs     |  8 +--
 .../coproduct_reflection_conformance_test.rs  | 67 +++++++++++++++++--
 2 files changed, 64 insertions(+), 11 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index ade015db7c5..f2bf696fa01 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -160,10 +160,10 @@ fn find_type_decl_start(source: &str, type_name: &str) -> Option<usize> {
     while let Some(rel) = source[search_from..].find(&needle) {
         let start = search_from + rel;
         let after = start + needle.len();
-        let boundary_ok = source
-            .as_bytes()
-            .get(after)
-            .is_none_or(|b| matches!(*b, b' ' | b'=' | b'{'));
+        let boundary_ok = source[after..]
+            .chars()
+            .next()
+            .is_none_or(|c| c.is_whitespace() || c == '=' || c == '{');
         let prefix_ok = start == 0
             || source
                 .as_bytes()
diff --git a/src/v2/tests/src/coproduct_reflection_conformance_test.rs b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
index 18ec2625b6f..50c4004d6c7 100644
--- a/src/v2/tests/src/coproduct_reflection_conformance_test.rs
+++ b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
@@ -2,6 +2,8 @@
 
 use std::rc::Rc;
 
+use v2_compiler::cli_run;
+use v2_compiler::coproduct_reflection;
 use v2_compiler::v2_compiler_compile::{compile_to_resolved, ResolvedPipelineResult, SourceFile};
 use v2_compiler::v2_interpreter::{self, Value};
 
@@ -45,20 +47,71 @@ fn assert_resolved_ok(resolved: &ResolvedPipelineResult) {
     );
 }
 
+fn run_witness(resolved: &ResolvedPipelineResult, function: &str) -> Value {
+    let graph = resolved
+        .graph
+        .as_ref()
+        .expect("graph after successful resolve");
+    v2_interpreter::run(graph, resolved.source_indices.clone(), function)
+        .unwrap_or_else(|e| panic!("run {function}: {e}"))
+}
+
 #[test]
 fn coproduct_reflection_path3_connective_behavior_conformance_holds() {
-    // gunbc claim-run resolves sources relative to workspace root; mirror that here.
     std::env::set_var("GUNBC_ROOT", workspace_root());
     let resolved = compile_to_resolved(Rc::new(cert_sources()));
     assert_resolved_ok(&resolved);
-    let graph = resolved
-        .graph
-        .as_ref()
-        .expect("graph after successful resolve");
-    match v2_interpreter::run(graph, resolved.source_indices.clone(), WITNESS_FN) {
-        Ok(Value::Bool(true)) => {}
+    match run_witness(&resolved, WITNESS_FN) {
+        Value::Bool(true) => {}
         other => panic!(
             "expected Bool(true) from {WITNESS_FN} (Path-3 key-set conformance), got {other:?}"
         ),
     }
 }
+
+#[test]
+fn coproduct_reflection_connective_behavior_arm_sets_are_distinct() {
+    std::env::set_var("GUNBC_ROOT", workspace_root());
+    let resolved = compile_to_resolved(Rc::new(cert_sources()));
+    assert_resolved_ok(&resolved);
+    match run_witness(&resolved, "witness_connective_behavior_arm_sets_are_distinct") {
+        Value::Bool(true) => {}
+        other => panic!("expected distinct arm sets, got {other:?}"),
+    }
+}
+
+#[test]
+fn coproduct_reflection_path3_witness_fails_on_dropped_disj_arm() {
+    std::env::set_var("GUNBC_ROOT", workspace_root());
+    let resolved = compile_to_resolved(Rc::new(cert_sources()));
+    assert_resolved_ok(&resolved);
+    let graph = resolved
+        .graph
+        .as_ref()
+        .expect("graph after successful resolve");
+    let ctx = cli_run::make_eval_context(graph, resolved.source_indices.clone());
+    let connective = (None, Value::Str("Connective".to_string()));
+
+    let reflection_keys =
+        coproduct_reflection::eval_coproduct_arm_keys(&ctx, &[connective.clone()])
+            .expect("reflection keys");
+    let corrupted = coproduct_reflection::eval_coproduct_arm_keys_with_dropped_last_arm(
+        &ctx,
+        "Connective",
+    )
+    .expect("corrupted keys");
+    let syntactic = coproduct_reflection::eval_syntactic_coproduct_arm_keys(
+        &ctx,
+        &[connective],
+    )
+    .expect("syntactic keys");
+
+    assert_ne!(
+        reflection_keys, corrupted,
+        "dropped-arm corruption must change reflection output"
+    );
+    assert_ne!(
+        corrupted, syntactic,
+        "mechanism drift (dropped Disj arm) must break Path-3 bag_eq witness"
+    );
+}

From f20a85d9700ec95ae10f94e38cbdf4f9c528565b Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 04:08:05 +0000
Subject: [PATCH 15/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs     |  8 ++------
 .../coproduct_reflection_conformance_test.rs  | 20 +++++++++----------
 2 files changed, 11 insertions(+), 17 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index f2bf696fa01..5c63971cb66 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -223,10 +223,7 @@ pub fn eval_syntactic_coproduct_arm_keys(
     ctx: &InterpContext,
     args: &[(Option<String>, Value)],
 ) -> InterpResult<Value> {
-    let type_name = expect_symbol(
-        args.first().map(|(_, v)| v),
-        "syntactic_coproduct_arm_keys",
-    )?;
+    let type_name = expect_symbol(args.first().map(|(_, v)| v), "syntactic_coproduct_arm_keys")?;
     let (_, file) = type_item_by_name(ctx, type_name)?;
     let labels = syntactic_coproduct_arm_labels(&file, type_name)?;
     Ok(symbol_list_value(&labels))
@@ -277,8 +274,7 @@ mod tests {
 
     #[test]
     fn syntactic_extractor_rejects_connective_prefix_of_longer_type_name() {
-        let source =
-            "type ConnectiveCoproductVariant = Foo | Bar\ntype Connective = Atom | Conj\n";
+        let source = "type ConnectiveCoproductVariant = Foo | Bar\ntype Connective = Atom | Conj\n";
         assert_eq!(
             extract_type_sum_arm_labels(source, "ConnectiveCoproductVariant").expect("variant"),
             vec!["Foo", "Bar"]
diff --git a/src/v2/tests/src/coproduct_reflection_conformance_test.rs b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
index 50c4004d6c7..b5dd4b654eb 100644
--- a/src/v2/tests/src/coproduct_reflection_conformance_test.rs
+++ b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
@@ -74,7 +74,10 @@ fn coproduct_reflection_connective_behavior_arm_sets_are_distinct() {
     std::env::set_var("GUNBC_ROOT", workspace_root());
     let resolved = compile_to_resolved(Rc::new(cert_sources()));
     assert_resolved_ok(&resolved);
-    match run_witness(&resolved, "witness_connective_behavior_arm_sets_are_distinct") {
+    match run_witness(
+        &resolved,
+        "witness_connective_behavior_arm_sets_are_distinct",
+    ) {
         Value::Bool(true) => {}
         other => panic!("expected distinct arm sets, got {other:?}"),
     }
@@ -95,16 +98,11 @@ fn coproduct_reflection_path3_witness_fails_on_dropped_disj_arm() {
     let reflection_keys =
         coproduct_reflection::eval_coproduct_arm_keys(&ctx, &[connective.clone()])
             .expect("reflection keys");
-    let corrupted = coproduct_reflection::eval_coproduct_arm_keys_with_dropped_last_arm(
-        &ctx,
-        "Connective",
-    )
-    .expect("corrupted keys");
-    let syntactic = coproduct_reflection::eval_syntactic_coproduct_arm_keys(
-        &ctx,
-        &[connective],
-    )
-    .expect("syntactic keys");
+    let corrupted =
+        coproduct_reflection::eval_coproduct_arm_keys_with_dropped_last_arm(&ctx, "Connective")
+            .expect("corrupted keys");
+    let syntactic = coproduct_reflection::eval_syntactic_coproduct_arm_keys(&ctx, &[connective])
+        .expect("syntactic keys");
 
     assert_ne!(
         reflection_keys, corrupted,

From 5ac54edcfb7a2cc5c629c905ee3d537b52934baa Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 04:15:33 +0000
Subject: [PATCH 16/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/v2_interpreter.rs | 37 +++++++++++++++++++++--------
 src/v2/tests/src/lib.rs             |  1 +
 src/v4/std/node.dag                 |  4 ++++
 3 files changed, 32 insertions(+), 10 deletions(-)

diff --git a/src/v2/stage0/src/v2_interpreter.rs b/src/v2/stage0/src/v2_interpreter.rs
index 9a5e43a750f..3b24d5a8ded 100644
--- a/src/v2/stage0/src/v2_interpreter.rs
+++ b/src/v2/stage0/src/v2_interpreter.rs
@@ -2113,6 +2113,21 @@ fn match_pattern(
     }
 }
 
+// ---------------------------------------------------------------------------
+// v4.std.node coproduct reflection intercept (module-scoped bootstrap seam)
+// ---------------------------------------------------------------------------
+
+const STD_NODE_REFLECTION_FNS: &[&str] = &["coproduct_arm_keys", "syntactic_coproduct_arm_keys"];
+
+fn is_v4_std_node_reflection_call(ctx: &InterpContext, func_name: &str) -> bool {
+    if !STD_NODE_REFLECTION_FNS.contains(&func_name) {
+        return false;
+    }
+    ctx.item_registry
+        .get(func_name)
+        .is_some_and(|info| info.module_name == "v4.std.node")
+}
+
 // ---------------------------------------------------------------------------
 // Function call (ExprCall)
 // ---------------------------------------------------------------------------
@@ -2131,16 +2146,18 @@ fn eval_call(node: &Rc<Node>, env: &Rc<Env>, ctx: &InterpContext) -> InterpResul
         })
         .collect::<InterpResult<_>>()?;
 
-    // R-reflect Phase 2a: compile-time coproduct-arm reflection (intercept-only; stub bodies
-    // self-recurse fail-closed if bypassed — see std/node.dag).
-    match func_name.as_str() {
-        "coproduct_arm_keys" => {
-            return crate::coproduct_reflection::eval_coproduct_arm_keys(ctx, &args);
-        }
-        "syntactic_coproduct_arm_keys" => {
-            return crate::coproduct_reflection::eval_syntactic_coproduct_arm_keys(ctx, &args);
-        }
-        _ => {}
+    // R-reflect Phase 2a: compile-time coproduct-arm reflection (intercept-only for
+    // v4.std.node substrate fns; self-recursive .dag stubs trap if bypassed).
+    if is_v4_std_node_reflection_call(ctx, &func_name) {
+        return match func_name.as_str() {
+            "coproduct_arm_keys" => {
+                crate::coproduct_reflection::eval_coproduct_arm_keys(ctx, &args)
+            }
+            "syntactic_coproduct_arm_keys" => {
+                crate::coproduct_reflection::eval_syntactic_coproduct_arm_keys(ctx, &args)
+            }
+            _ => unreachable!("reflection fn set mismatch"),
+        };
     }
 
     // Check for built-in runtime functions
diff --git a/src/v2/tests/src/lib.rs b/src/v2/tests/src/lib.rs
index 0f048963ae4..d710c483c41 100644
--- a/src/v2/tests/src/lib.rs
+++ b/src/v2/tests/src/lib.rs
@@ -31,6 +31,7 @@ mod diagnostics;
 mod effects;
 #[cfg(test)]
 mod fn_as_value_test;
+#[cfg(test)]
 mod fold_list_generic_instantiation_test;
 #[cfg(test)]
 mod generator_match_arm_test;
diff --git a/src/v4/std/node.dag b/src/v4/std/node.dag
index 1ce54e52565..acc83759508 100644
--- a/src/v4/std/node.dag
+++ b/src/v4/std/node.dag
@@ -49,12 +49,16 @@ type Behavior
 // substrate compiler builtin once type-name → resolved Disj is expressible in v4 .dag.
 // 🟡 gated — feature:coproduct-reflection-intercept-only — bind gunbc#4863 — dissolve-on-arrival:
 // substrate reflection builtin; forbidden: silent empty-list default ([]) on bypass.
+// Body self-recurses (non-terminating) if the v2 intercept is bypassed — not a typed
+// diagnostic (node.dag is import-free), but never returns [].
 fn coproduct_arm_keys(type_name: Symbol) -> List<Symbol> {
   coproduct_arm_keys(type_name: type_name)
 }
 
 // 🟡 gated — feature:coproduct-reflection-intercept-only — bind gunbc#4863 — dissolve-on-arrival:
 // substrate reflection builtin; forbidden: silent empty-list default ([]) on bypass.
+// Body self-recurses (non-terminating) if the v2 intercept is bypassed — not a typed
+// diagnostic (node.dag is import-free), but never returns [].
 fn syntactic_coproduct_arm_keys(type_name: Symbol) -> List<Symbol> {
   syntactic_coproduct_arm_keys(type_name: type_name)
 }

From 2580c1e48657394a3754108799267f1ddf571de6 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 04:21:33 +0000
Subject: [PATCH 17/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs     | 193 ++++++++++++++----
 src/v2/stage0/src/v2_interpreter.rs           |  19 +-
 .../coproduct_reflection_conformance_test.rs  |  87 ++++++--
 src/v4/std/node.dag                           |  26 +--
 src/v4/std/node_query.dag                     |  17 +-
 .../coproduct_reflection_conformance.dag      |   7 +-
 6 files changed, 264 insertions(+), 85 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index 5c63971cb66..b2feec7b31a 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -1,12 +1,10 @@
-//! Coproduct-arm reflection — Phase 2a compile-time key enumeration (R-reflect).
+//! R-reflect Phase 2a — minimal dissolving bridges (substrate-native target).
 //!
-//! Bootstrap seam: v2 interpreter intercept over the resolved compile graph (Disj walk).
-//! Path 3 (syntactic): raw source-text scan of `|`-separated arm labels — independent of the
-//! Disj resolver (design-coproduct-arm-reflection.md §5.2).
-//!
-//! Dissolve-on-arrival: substrate compiler builtin once type-name → resolved Disj Node is
-//! expressible in v4 `.dag` (analogous to node_labeled_child_edges for value-level queries).
+//! - `resolve_type_node`: compiler Disj type item → substrate `Node` Value (dissolves when v4
+//!   gains compile-graph access).
+//! - `syntactic_coproduct_arm_keys`: Path-3 raw-source text scan (irreducible I/O boundary; stays Rust).
 
+use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::v2_compiler_infer_items::ItemKind;
@@ -22,7 +20,7 @@ fn expect_symbol<'a>(value: Option<&'a Value>, what: &str) -> InterpResult<&'a s
     }
 }
 
-fn type_item_by_name<'a>(
+pub(crate) fn type_item_by_name<'a>(
     ctx: &'a InterpContext,
     type_name: &str,
 ) -> InterpResult<(&'a Rc<Node>, String)> {
@@ -49,30 +47,95 @@ fn type_item_by_name<'a>(
         }
     }
     Err(InterpError::TypeError {
-        msg: format!("coproduct reflection: unknown closed type `{type_name}`"),
+        msg: format!("resolve_type_node: unknown closed type `{type_name}`"),
     })
 }
 
-fn disj_variant_labels(item: &Rc<Node>, ctx: &InterpContext) -> InterpResult<Vec<String>> {
+fn nullary_connective_variant(ctx: &InterpContext, name: &str) -> Value {
+    Value::Variant {
+        type_name: ctx.sym("Connective"),
+        variant_name: ctx.sym(name),
+        fields: Rc::new(HashMap::new()),
+    }
+}
+
+fn node_kind_type_node(ctx: &InterpContext, connective: Value) -> Value {
+    Value::Variant {
+        type_name: ctx.sym("NodeKind"),
+        variant_name: ctx.sym("TypeNode"),
+        fields: Rc::new(HashMap::from([(ctx.sym("connective"), connective)])),
+    }
+}
+
+fn synthetic_occurrence(ctx: &InterpContext) -> Value {
+    Value::Variant {
+        type_name: ctx.sym("NodeOccurrenceId"),
+        variant_name: ctx.sym("SyntheticOccurrence"),
+        fields: Rc::new(HashMap::new()),
+    }
+}
+
+fn node_record(ctx: &InterpContext, kind: Value, children: Vec<Value>) -> Value {
+    Value::Record {
+        type_name: ctx.sym("Node"),
+        fields: Rc::new(HashMap::from([
+            (ctx.sym("kind"), kind),
+            (
+                ctx.sym("children"),
+                crate::v2_interpreter::list_value(children),
+            ),
+            (ctx.sym("occurrence_id"), synthetic_occurrence(ctx)),
+        ])),
+    }
+}
+
+fn edge_named(ctx: &InterpContext, name: &str, target: Value) -> Value {
+    Value::Record {
+        type_name: ctx.sym("Edge"),
+        fields: Rc::new(HashMap::from([
+            (
+                ctx.sym("label"),
+                Value::Variant {
+                    type_name: ctx.sym("EdgeLabel"),
+                    variant_name: ctx.sym("Named"),
+                    fields: Rc::new(HashMap::from([(
+                        ctx.sym("name"),
+                        Value::Str(name.to_string()),
+                    )])),
+                },
+            ),
+            (ctx.sym("target"), target),
+        ])),
+    }
+}
+
+fn placeholder_arm_target(ctx: &InterpContext) -> Value {
+    node_record(
+        ctx,
+        node_kind_type_node(ctx, nullary_connective_variant(ctx, "Conj")),
+        vec![],
+    )
+}
+
+/// Marshal a resolved closed-coproduct (Disj) type item to substrate `Node` with Named arm edges.
+pub fn marshal_disj_type_item(ctx: &InterpContext, item: &Rc<Node>) -> InterpResult<Value> {
     if item.connective != Connective::Disj {
         return Err(InterpError::TypeError {
-            msg: "coproduct reflection: type is not a closed coproduct (Disj)".to_string(),
+            msg: "resolve_type_node: type is not a closed coproduct (Disj)".to_string(),
         });
     }
     let si = ctx.source_indices();
-    Ok(item
-        .children
-        .iter()
-        .map(|child| authored_name_at(si.clone(), child.clone()))
-        .collect())
-}
-
-fn symbol_list_value(labels: &[String]) -> Value {
-    let items: Vec<Value> = labels
-        .iter()
-        .map(|label| Value::Str(label.clone()))
-        .collect();
-    crate::v2_interpreter::list_value(items)
+    let placeholder = placeholder_arm_target(ctx);
+    let mut edges = Vec::with_capacity(item.children.len());
+    for child in item.children.iter() {
+        let label = authored_name_at(si.clone(), child.clone());
+        edges.push(edge_named(ctx, &label, placeholder.clone()));
+    }
+    Ok(node_record(
+        ctx,
+        node_kind_type_node(ctx, nullary_connective_variant(ctx, "Disj")),
+        edges,
+    ))
 }
 
 /// Bootstrap only: resolve declaring source path via cwd walk + optional GUNBC_ROOT.
@@ -119,7 +182,6 @@ pub fn syntactic_coproduct_arm_labels(file: &str, type_name: &str) -> InterpResu
     })
 }
 
-/// Scan source for `type <name> = <arm> (| <arm>)*` without invoking the type resolver.
 fn extract_type_sum_arm_labels(source: &str, type_name: &str) -> Option<Vec<String>> {
     let start = find_type_decl_start(source, type_name)?;
     let needle = format!("type {type_name}");
@@ -153,7 +215,6 @@ fn extract_type_sum_arm_labels(source: &str, type_name: &str) -> Option<Vec<Stri
     }
 }
 
-/// Word-boundary match: `type Connective` must not match `type ConnectiveCoproductVariant`.
 fn find_type_decl_start(source: &str, type_name: &str) -> Option<usize> {
     let needle = format!("type {type_name}");
     let mut search_from = 0usize;
@@ -209,35 +270,90 @@ fn skip_braced(s: &str) -> Option<&str> {
     None
 }
 
-pub fn eval_coproduct_arm_keys(
+pub fn eval_resolve_type_node(
     ctx: &InterpContext,
     args: &[(Option<String>, Value)],
 ) -> InterpResult<Value> {
-    let type_name = expect_symbol(args.first().map(|(_, v)| v), "coproduct_arm_keys")?;
+    let type_name = expect_symbol(args.first().map(|(_, v)| v), "resolve_type_node")?;
     let (item, _) = type_item_by_name(ctx, type_name)?;
-    let labels = disj_variant_labels(item, ctx)?;
-    Ok(symbol_list_value(&labels))
+    marshal_disj_type_item(ctx, item)
 }
 
 pub fn eval_syntactic_coproduct_arm_keys(
     ctx: &InterpContext,
     args: &[(Option<String>, Value)],
 ) -> InterpResult<Value> {
-    let type_name = expect_symbol(args.first().map(|(_, v)| v), "syntactic_coproduct_arm_keys")?;
+    let type_name = expect_symbol(
+        args.first().map(|(_, v)| v),
+        "syntactic_coproduct_arm_keys",
+    )?;
     let (_, file) = type_item_by_name(ctx, type_name)?;
     let labels = syntactic_coproduct_arm_labels(&file, type_name)?;
-    Ok(symbol_list_value(&labels))
+    let items: Vec<Value> = labels
+        .iter()
+        .map(|label| Value::Str(label.clone()))
+        .collect();
+    Ok(crate::v2_interpreter::list_value(items))
 }
 
-/// Mechanism-drift probe: drop the last Disj child and compare key sets (test-only).
-pub fn eval_coproduct_arm_keys_with_dropped_last_arm(
+/// Mechanism-drift probe: drop the last Named arm edge from a marshaled Disj node.
+pub fn eval_resolve_type_node_with_dropped_last_arm(
     ctx: &InterpContext,
     type_name: &str,
 ) -> InterpResult<Value> {
     let (item, _) = type_item_by_name(ctx, type_name)?;
-    let mut labels = disj_variant_labels(item, ctx)?;
-    labels.pop();
-    Ok(symbol_list_value(&labels))
+    let node = marshal_disj_type_item(ctx, item)?;
+    let Value::Record { fields, .. } = node else {
+        return Err(InterpError::TypeError {
+            msg: "resolve_type_node: expected Node record".to_string(),
+        });
+    };
+    let children = fields
+        .get(&ctx.sym("children"))
+        .ok_or_else(|| InterpError::TypeError {
+            msg: "resolve_type_node: Node missing children".to_string(),
+        })?;
+    let Some(items) = crate::v2_interpreter::free_monoid_to_vec(children) else {
+        return Err(InterpError::TypeError {
+            msg: "resolve_type_node: children not a list".to_string(),
+        });
+    };
+    if items.is_empty() {
+        return Err(InterpError::TypeError {
+            msg: "resolve_type_node: Disj has no arms".to_string(),
+        });
+    }
+    let mut trimmed = items[..items.len() - 1].to_vec();
+    if trimmed.is_empty() {
+        trimmed = vec![];
+    }
+    Ok(Value::Record {
+        type_name: ctx.sym("Node"),
+        fields: Rc::new(HashMap::from([
+            (
+                ctx.sym("kind"),
+                fields
+                    .get(&ctx.sym("kind"))
+                    .cloned()
+                    .ok_or_else(|| InterpError::TypeError {
+                        msg: "resolve_type_node: Node missing kind".to_string(),
+                    })?,
+            ),
+            (
+                ctx.sym("children"),
+                crate::v2_interpreter::list_value(trimmed),
+            ),
+            (
+                ctx.sym("occurrence_id"),
+                fields
+                    .get(&ctx.sym("occurrence_id"))
+                    .cloned()
+                    .ok_or_else(|| InterpError::TypeError {
+                        msg: "resolve_type_node: Node missing occurrence_id".to_string(),
+                    })?,
+            ),
+        ])),
+    })
 }
 
 #[cfg(test)]
@@ -274,7 +390,8 @@ mod tests {
 
     #[test]
     fn syntactic_extractor_rejects_connective_prefix_of_longer_type_name() {
-        let source = "type ConnectiveCoproductVariant = Foo | Bar\ntype Connective = Atom | Conj\n";
+        let source =
+            "type ConnectiveCoproductVariant = Foo | Bar\ntype Connective = Atom | Conj\n";
         assert_eq!(
             extract_type_sum_arm_labels(source, "ConnectiveCoproductVariant").expect("variant"),
             vec!["Foo", "Bar"]
diff --git a/src/v2/stage0/src/v2_interpreter.rs b/src/v2/stage0/src/v2_interpreter.rs
index 3b24d5a8ded..0b6bf8e0a79 100644
--- a/src/v2/stage0/src/v2_interpreter.rs
+++ b/src/v2/stage0/src/v2_interpreter.rs
@@ -2117,10 +2117,10 @@ fn match_pattern(
 // v4.std.node coproduct reflection intercept (module-scoped bootstrap seam)
 // ---------------------------------------------------------------------------
 
-const STD_NODE_REFLECTION_FNS: &[&str] = &["coproduct_arm_keys", "syntactic_coproduct_arm_keys"];
+const STD_NODE_BRIDGE_FNS: &[&str] = &["resolve_type_node", "syntactic_coproduct_arm_keys"];
 
-fn is_v4_std_node_reflection_call(ctx: &InterpContext, func_name: &str) -> bool {
-    if !STD_NODE_REFLECTION_FNS.contains(&func_name) {
+fn is_v4_std_node_bridge_call(ctx: &InterpContext, func_name: &str) -> bool {
+    if !STD_NODE_BRIDGE_FNS.contains(&func_name) {
         return false;
     }
     ctx.item_registry
@@ -2146,17 +2146,14 @@ fn eval_call(node: &Rc<Node>, env: &Rc<Env>, ctx: &InterpContext) -> InterpResul
         })
         .collect::<InterpResult<_>>()?;
 
-    // R-reflect Phase 2a: compile-time coproduct-arm reflection (intercept-only for
-    // v4.std.node substrate fns; self-recursive .dag stubs trap if bypassed).
-    if is_v4_std_node_reflection_call(ctx, &func_name) {
+    // R-reflect Phase 2a: minimal v4.std.node bridges (resolve_type_node + Path-3 syntactic scan).
+    if is_v4_std_node_bridge_call(ctx, &func_name) {
         return match func_name.as_str() {
-            "coproduct_arm_keys" => {
-                crate::coproduct_reflection::eval_coproduct_arm_keys(ctx, &args)
-            }
+            "resolve_type_node" => crate::coproduct_reflection::eval_resolve_type_node(ctx, &args),
             "syntactic_coproduct_arm_keys" => {
                 crate::coproduct_reflection::eval_syntactic_coproduct_arm_keys(ctx, &args)
             }
-            _ => unreachable!("reflection fn set mismatch"),
+            _ => unreachable!("bridge fn set mismatch"),
         };
     }
 
@@ -4196,7 +4193,7 @@ fn record_flatten(items: usize) {
 /// builtins (fold/map/filter/foreach) accept either. Fails closed (P3): a non-list value —
 /// including Null and a Cons with a missing/non-list `tail` — returns None so the caller
 /// raises a type error rather than fabricating an empty/partial list.
-fn free_monoid_to_vec(val: &Value) -> Option<Vec<Value>> {
+pub(crate) fn free_monoid_to_vec(val: &Value) -> Option<Vec<Value>> {
     let mut out = Vec::new();
     let mut cur = val.clone();
     let monoid_syms = active_ctx().map(|ctx| {
diff --git a/src/v2/tests/src/coproduct_reflection_conformance_test.rs b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
index b5dd4b654eb..f85459f3ec2 100644
--- a/src/v2/tests/src/coproduct_reflection_conformance_test.rs
+++ b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
@@ -1,5 +1,6 @@
 //! R-reflect Phase 2a: Path-3 key-set conformance on Connective/Behavior by execution.
 
+use std::collections::HashMap;
 use std::rc::Rc;
 
 use v2_compiler::cli_run;
@@ -56,6 +57,58 @@ fn run_witness(resolved: &ResolvedPipelineResult, function: &str) -> Value {
         .unwrap_or_else(|e| panic!("run {function}: {e}"))
 }
 
+fn symbol_list_strings(val: &Value) -> Vec<String> {
+    let items = match val {
+        Value::List(xs) => xs.iter().cloned().collect::<Vec<_>>(),
+        _ => panic!("expected list, got {val:?}"),
+    };
+    items
+        .iter()
+        .map(|v| match v {
+            Value::Str(s) => s.clone(),
+            other => panic!("expected Str in symbol list, got {other:?}"),
+        })
+        .collect()
+}
+
+fn edge_list_from_node_children(children: &Value) -> Vec<Value> {
+    match children {
+        Value::List(xs) => xs.iter().cloned().collect(),
+        _ => panic!("expected edge list, got {children:?}"),
+    }
+}
+
+fn arm_key_list_from_node(node: &Value) -> Vec<String> {
+    let Value::Record { fields, .. } = node else {
+        panic!("expected Node record, got {node:?}");
+    };
+    let children = fields.get("children").expect("children field");
+    let edges = edge_list_from_node_children(children);
+    let mut keys = Vec::with_capacity(edges.len());
+    for edge in edges {
+        let Value::Record { fields: ef, .. } = edge else {
+            panic!("expected Edge record");
+        };
+        let label = ef.get("label").expect("label");
+        let Value::Variant {
+            variant_name,
+            fields: lf,
+            ..
+        } = label
+        else {
+            panic!("expected EdgeLabel variant");
+        };
+        if variant_name.0 != "Named" {
+            continue;
+        }
+        let Value::Str(name) = lf.get("name").expect("name field") else {
+            panic!("expected Symbol string");
+        };
+        keys.push(name.clone());
+    }
+    keys
+}
+
 #[test]
 fn coproduct_reflection_path3_connective_behavior_conformance_holds() {
     std::env::set_var("GUNBC_ROOT", workspace_root());
@@ -95,21 +148,27 @@ fn coproduct_reflection_path3_witness_fails_on_dropped_disj_arm() {
     let ctx = cli_run::make_eval_context(graph, resolved.source_indices.clone());
     let connective = (None, Value::Str("Connective".to_string()));
 
-    let reflection_keys =
-        coproduct_reflection::eval_coproduct_arm_keys(&ctx, &[connective.clone()])
-            .expect("reflection keys");
-    let corrupted =
-        coproduct_reflection::eval_coproduct_arm_keys_with_dropped_last_arm(&ctx, "Connective")
-            .expect("corrupted keys");
-    let syntactic = coproduct_reflection::eval_syntactic_coproduct_arm_keys(&ctx, &[connective])
-        .expect("syntactic keys");
+    let reflection_node =
+        coproduct_reflection::eval_resolve_type_node(&ctx, &[connective.clone()])
+            .expect("resolved node");
+    let corrupted = coproduct_reflection::eval_resolve_type_node_with_dropped_last_arm(
+        &ctx,
+        "Connective",
+    )
+    .expect("corrupted node");
+    let syntactic = coproduct_reflection::eval_syntactic_coproduct_arm_keys(
+        &ctx,
+        &[connective],
+    )
+    .expect("syntactic keys");
 
+    let good_keys = arm_key_list_from_node(&reflection_node);
+    let bad_keys = arm_key_list_from_node(&corrupted);
+    let syntactic_keys = symbol_list_strings(&syntactic);
+
+    assert_eq!(good_keys, syntactic_keys, "baseline keys must match syntactic");
     assert_ne!(
-        reflection_keys, corrupted,
-        "dropped-arm corruption must change reflection output"
-    );
-    assert_ne!(
-        corrupted, syntactic,
-        "mechanism drift (dropped Disj arm) must break Path-3 bag_eq witness"
+        bad_keys, syntactic_keys,
+        "dropped Disj arm must break Path-3 bag_eq witness"
     );
 }
diff --git a/src/v4/std/node.dag b/src/v4/std/node.dag
index acc83759508..5b5cbae99a9 100644
--- a/src/v4/std/node.dag
+++ b/src/v4/std/node.dag
@@ -43,22 +43,16 @@ type Behavior
   | Bind
 
 
-// R-reflect Phase 2a — coproduct-arm reflection substrate (design-coproduct-arm-reflection.md §4).
-// Compile-time only: arm keys resolve from closed Disj declarations at the v2 interpreter
-// intercept (bootstrap Rust in src/v2/stage0/src/coproduct_reflection.rs). Dissolve-on-arrival:
-// substrate compiler builtin once type-name → resolved Disj is expressible in v4 .dag.
-// 🟡 gated — feature:coproduct-reflection-intercept-only — bind gunbc#4863 — dissolve-on-arrival:
-// substrate reflection builtin; forbidden: silent empty-list default ([]) on bypass.
-// Body self-recurses (non-terminating) if the v2 intercept is bypassed — not a typed
-// diagnostic (node.dag is import-free), but never returns [].
-fn coproduct_arm_keys(type_name: Symbol) -> List<Symbol> {
-  coproduct_arm_keys(type_name: type_name)
-}
-
-// 🟡 gated — feature:coproduct-reflection-intercept-only — bind gunbc#4863 — dissolve-on-arrival:
-// substrate reflection builtin; forbidden: silent empty-list default ([]) on bypass.
-// Body self-recurses (non-terminating) if the v2 intercept is bypassed — not a typed
-// diagnostic (node.dag is import-free), but never returns [].
+// R-reflect Phase 2a — dissolving bridge + Path-3 I/O boundary (design §4.3 substrate-native).
+// resolve_type_node: minimal Rust bridge (compiler Disj → substrate Node Value); dissolves when
+// v4 gains compile-graph access. Enumeration lives in v4.std.node_query (node_labeled_child_edges).
+// syntactic_coproduct_arm_keys: irreducible raw-source scan (Path 3 independence from parse+resolve).
+// 🟡 gated — feature:coproduct-reflection-bridge — bind gunbc#4863 — dissolve-on-arrival: v4
+// compile-graph access replaces resolve_type_node intercept; forbidden: parallel enumeration in Rust.
+fn resolve_type_node(type_name: Symbol) -> Node {
+  resolve_type_node(type_name: type_name)
+}
+
 fn syntactic_coproduct_arm_keys(type_name: Symbol) -> List<Symbol> {
   syntactic_coproduct_arm_keys(type_name: type_name)
 }
diff --git a/src/v4/std/node_query.dag b/src/v4/std/node_query.dag
index b3db8775986..cab3c3b8645 100644
--- a/src/v4/std/node_query.dag
+++ b/src/v4/std/node_query.dag
@@ -33,7 +33,22 @@ import v4.std.node {
   Symbol,
   TypeNode,
   arrow_body_target_lookup,
-  name_occurrences
+  name_occurrences,
+  named_edge_sort_key,
+  resolve_type_node
+}
+
+// R-reflect Phase 2a: pure .dag enumeration over resolved Disj Node (substrate-native).
+fn coproduct_arm_key_list_from_node(node: Node) -> List<Symbol> {
+  fold(
+    xs: node_labeled_child_edges(node: node),
+    init: Empty,
+    f: fn(acc, e) { list_snoc_item(xs: acc, item: named_edge_sort_key(e: e)) }
+  )
+}
+
+fn coproduct_arm_keys(type_name: Symbol) -> List<Symbol> {
+  coproduct_arm_key_list_from_node(node: resolve_type_node(type_name: type_name))
 }
 // 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: node-positional-child-targets — bind node://adhoc-sg2-positional-child-targets — dissolve-on-arrival: substrate canonical positional-child target projection on Node.children; lives in node_query (node.dag is import-free substrate root). forbidden: parallel edge-label filters outside std/node_query (e.g. translate-local conj_positional_targets folds).
 fn node_positional_child_targets(node: Node) -> List<Node> {
diff --git a/src/v4/test/claim/manual/coproduct_reflection_conformance.dag b/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
index 257b5364289..29cfdc3def6 100644
--- a/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
+++ b/src/v4/test/claim/manual/coproduct_reflection_conformance.dag
@@ -8,11 +8,8 @@ module v4.test.claim.manual.coproduct_reflection_conformance
 
 import v4.std.algebra { bag_eq }
 import v4.std.logic { Bool }
-import v4.std.node {
-  Symbol,
-  coproduct_arm_keys,
-  syntactic_coproduct_arm_keys
-}
+import v4.std.node { Symbol, syntactic_coproduct_arm_keys }
+import v4.std.node_query { coproduct_arm_keys }
 
 data reflect_connective_type: Symbol = ^Connective
 data reflect_behavior_type: Symbol = ^Behavior

From 78a5af2166b6d1c49920b18fddd41fb3e193982e Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 04:23:02 +0000
Subject: [PATCH 18/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs     | 49 +++++++++++++++++++
 .../coproduct_reflection_conformance_test.rs  | 47 +++---------------
 2 files changed, 55 insertions(+), 41 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index b2feec7b31a..f412f2d9f69 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -296,6 +296,55 @@ pub fn eval_syntactic_coproduct_arm_keys(
     Ok(crate::v2_interpreter::list_value(items))
 }
 
+/// Extract Named arm labels from a marshaled substrate Node Value (test / drift probe).
+pub fn arm_labels_from_marshaled_node(
+    ctx: &InterpContext,
+    node: &Value,
+) -> InterpResult<Vec<String>> {
+    let Value::Record { fields, .. } = node else {
+        return Err(InterpError::TypeError {
+            msg: "expected Node record".to_string(),
+        });
+    };
+    let children = fields.get(&ctx.sym("children")).ok_or_else(|| InterpError::TypeError {
+        msg: "Node missing children".to_string(),
+    })?;
+    let edges = crate::v2_interpreter::free_monoid_to_vec(children).ok_or_else(|| {
+        InterpError::TypeError {
+            msg: "children not a list".to_string(),
+        }
+    })?;
+    let mut labels = Vec::with_capacity(edges.len());
+    for edge in edges {
+        let Value::Record { fields: ef, .. } = edge else {
+            return Err(InterpError::TypeError {
+                msg: "expected Edge record".to_string(),
+            });
+        };
+        let label = ef.get(&ctx.sym("label")).ok_or_else(|| InterpError::TypeError {
+            msg: "Edge missing label".to_string(),
+        })?;
+        let Value::Variant {
+            variant_name,
+            fields: lf,
+            ..
+        } = label
+        else {
+            return Err(InterpError::TypeError {
+                msg: "expected EdgeLabel variant".to_string(),
+            });
+        };
+        if ctx.resolve(*variant_name) != "Named" {
+            continue;
+        }
+        let Value::Str(name) = lf.get(&ctx.sym("name")).ok_or_else(|| InterpError::TypeError {
+            msg: "Named edge missing name".to_string(),
+        })?;
+        labels.push(name.clone());
+    }
+    Ok(labels)
+}
+
 /// Mechanism-drift probe: drop the last Named arm edge from a marshaled Disj node.
 pub fn eval_resolve_type_node_with_dropped_last_arm(
     ctx: &InterpContext,
diff --git a/src/v2/tests/src/coproduct_reflection_conformance_test.rs b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
index f85459f3ec2..84c6fc7febc 100644
--- a/src/v2/tests/src/coproduct_reflection_conformance_test.rs
+++ b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
@@ -1,6 +1,5 @@
 //! R-reflect Phase 2a: Path-3 key-set conformance on Connective/Behavior by execution.
 
-use std::collections::HashMap;
 use std::rc::Rc;
 
 use v2_compiler::cli_run;
@@ -71,44 +70,6 @@ fn symbol_list_strings(val: &Value) -> Vec<String> {
         .collect()
 }
 
-fn edge_list_from_node_children(children: &Value) -> Vec<Value> {
-    match children {
-        Value::List(xs) => xs.iter().cloned().collect(),
-        _ => panic!("expected edge list, got {children:?}"),
-    }
-}
-
-fn arm_key_list_from_node(node: &Value) -> Vec<String> {
-    let Value::Record { fields, .. } = node else {
-        panic!("expected Node record, got {node:?}");
-    };
-    let children = fields.get("children").expect("children field");
-    let edges = edge_list_from_node_children(children);
-    let mut keys = Vec::with_capacity(edges.len());
-    for edge in edges {
-        let Value::Record { fields: ef, .. } = edge else {
-            panic!("expected Edge record");
-        };
-        let label = ef.get("label").expect("label");
-        let Value::Variant {
-            variant_name,
-            fields: lf,
-            ..
-        } = label
-        else {
-            panic!("expected EdgeLabel variant");
-        };
-        if variant_name.0 != "Named" {
-            continue;
-        }
-        let Value::Str(name) = lf.get("name").expect("name field") else {
-            panic!("expected Symbol string");
-        };
-        keys.push(name.clone());
-    }
-    keys
-}
-
 #[test]
 fn coproduct_reflection_path3_connective_behavior_conformance_holds() {
     std::env::set_var("GUNBC_ROOT", workspace_root());
@@ -162,8 +123,12 @@ fn coproduct_reflection_path3_witness_fails_on_dropped_disj_arm() {
     )
     .expect("syntactic keys");
 
-    let good_keys = arm_key_list_from_node(&reflection_node);
-    let bad_keys = arm_key_list_from_node(&corrupted);
+    let good_keys =
+        coproduct_reflection::arm_labels_from_marshaled_node(&ctx, &reflection_node)
+            .expect("good keys");
+    let bad_keys =
+        coproduct_reflection::arm_labels_from_marshaled_node(&ctx, &corrupted)
+            .expect("bad keys");
     let syntactic_keys = symbol_list_strings(&syntactic);
 
     assert_eq!(good_keys, syntactic_keys, "baseline keys must match syntactic");

From aaec94c78399f99922b89dd0d5b59b7076b59a30 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 04:24:33 +0000
Subject: [PATCH 19/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index f412f2d9f69..b04f2cc34a9 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -330,16 +330,14 @@ pub fn arm_labels_from_marshaled_node(
             ..
         } = label
         else {
-            return Err(InterpError::TypeError {
-                msg: "expected EdgeLabel variant".to_string(),
-            });
+            continue;
         };
         if ctx.resolve(*variant_name) != "Named" {
             continue;
         }
-        let Value::Str(name) = lf.get(&ctx.sym("name")).ok_or_else(|| InterpError::TypeError {
-            msg: "Named edge missing name".to_string(),
-        })?;
+        let Some(Value::Str(name)) = lf.get(&ctx.sym("name")) else {
+            continue;
+        };
         labels.push(name.clone());
     }
     Ok(labels)

From fdf23f216c226bc896546f9b5aab27bb4d14dfb5 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 04:26:06 +0000
Subject: [PATCH 20/21] WIP: R-reflect Phase-2a: variant-enumeration primitive
 in std+compiler + Path

---
 src/v2/stage0/src/coproduct_reflection.rs     | 24 +++++++-------
 .../coproduct_reflection_conformance_test.rs  | 33 ++++++++-----------
 2 files changed, 26 insertions(+), 31 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index b04f2cc34a9..4b384e71e38 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -283,10 +283,7 @@ pub fn eval_syntactic_coproduct_arm_keys(
     ctx: &InterpContext,
     args: &[(Option<String>, Value)],
 ) -> InterpResult<Value> {
-    let type_name = expect_symbol(
-        args.first().map(|(_, v)| v),
-        "syntactic_coproduct_arm_keys",
-    )?;
+    let type_name = expect_symbol(args.first().map(|(_, v)| v), "syntactic_coproduct_arm_keys")?;
     let (_, file) = type_item_by_name(ctx, type_name)?;
     let labels = syntactic_coproduct_arm_labels(&file, type_name)?;
     let items: Vec<Value> = labels
@@ -306,9 +303,11 @@ pub fn arm_labels_from_marshaled_node(
             msg: "expected Node record".to_string(),
         });
     };
-    let children = fields.get(&ctx.sym("children")).ok_or_else(|| InterpError::TypeError {
-        msg: "Node missing children".to_string(),
-    })?;
+    let children = fields
+        .get(&ctx.sym("children"))
+        .ok_or_else(|| InterpError::TypeError {
+            msg: "Node missing children".to_string(),
+        })?;
     let edges = crate::v2_interpreter::free_monoid_to_vec(children).ok_or_else(|| {
         InterpError::TypeError {
             msg: "children not a list".to_string(),
@@ -321,9 +320,11 @@ pub fn arm_labels_from_marshaled_node(
                 msg: "expected Edge record".to_string(),
             });
         };
-        let label = ef.get(&ctx.sym("label")).ok_or_else(|| InterpError::TypeError {
-            msg: "Edge missing label".to_string(),
-        })?;
+        let label = ef
+            .get(&ctx.sym("label"))
+            .ok_or_else(|| InterpError::TypeError {
+                msg: "Edge missing label".to_string(),
+            })?;
         let Value::Variant {
             variant_name,
             fields: lf,
@@ -437,8 +438,7 @@ mod tests {
 
     #[test]
     fn syntactic_extractor_rejects_connective_prefix_of_longer_type_name() {
-        let source =
-            "type ConnectiveCoproductVariant = Foo | Bar\ntype Connective = Atom | Conj\n";
+        let source = "type ConnectiveCoproductVariant = Foo | Bar\ntype Connective = Atom | Conj\n";
         assert_eq!(
             extract_type_sum_arm_labels(source, "ConnectiveCoproductVariant").expect("variant"),
             vec!["Foo", "Bar"]
diff --git a/src/v2/tests/src/coproduct_reflection_conformance_test.rs b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
index 84c6fc7febc..b4868bd772e 100644
--- a/src/v2/tests/src/coproduct_reflection_conformance_test.rs
+++ b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
@@ -109,29 +109,24 @@ fn coproduct_reflection_path3_witness_fails_on_dropped_disj_arm() {
     let ctx = cli_run::make_eval_context(graph, resolved.source_indices.clone());
     let connective = (None, Value::Str("Connective".to_string()));
 
-    let reflection_node =
-        coproduct_reflection::eval_resolve_type_node(&ctx, &[connective.clone()])
-            .expect("resolved node");
-    let corrupted = coproduct_reflection::eval_resolve_type_node_with_dropped_last_arm(
-        &ctx,
-        "Connective",
-    )
-    .expect("corrupted node");
-    let syntactic = coproduct_reflection::eval_syntactic_coproduct_arm_keys(
-        &ctx,
-        &[connective],
-    )
-    .expect("syntactic keys");
+    let reflection_node = coproduct_reflection::eval_resolve_type_node(&ctx, &[connective.clone()])
+        .expect("resolved node");
+    let corrupted =
+        coproduct_reflection::eval_resolve_type_node_with_dropped_last_arm(&ctx, "Connective")
+            .expect("corrupted node");
+    let syntactic = coproduct_reflection::eval_syntactic_coproduct_arm_keys(&ctx, &[connective])
+        .expect("syntactic keys");
 
-    let good_keys =
-        coproduct_reflection::arm_labels_from_marshaled_node(&ctx, &reflection_node)
-            .expect("good keys");
+    let good_keys = coproduct_reflection::arm_labels_from_marshaled_node(&ctx, &reflection_node)
+        .expect("good keys");
     let bad_keys =
-        coproduct_reflection::arm_labels_from_marshaled_node(&ctx, &corrupted)
-            .expect("bad keys");
+        coproduct_reflection::arm_labels_from_marshaled_node(&ctx, &corrupted).expect("bad keys");
     let syntactic_keys = symbol_list_strings(&syntactic);
 
-    assert_eq!(good_keys, syntactic_keys, "baseline keys must match syntactic");
+    assert_eq!(
+        good_keys, syntactic_keys,
+        "baseline keys must match syntactic"
+    );
     assert_ne!(
         bad_keys, syntactic_keys,
         "dropped Disj arm must break Path-3 bag_eq witness"

From 8db2b687afebcaf1d9a3261983ebc89b2c91a649 Mon Sep 17 00:00:00 2001
From: Brian Searls <briansearls1@gmail.com>
Date: Sun, 14 Jun 2026 05:41:13 +0000
Subject: [PATCH 21/21] fix(reflect): F1-F4 RC batch on fdf23f216c signed base

Address claude RC 29001: self-ground coordination carve-out (gunbc#4861),
fail-loud Path-3 scanner, in-memory source_indices, bridge intercept
sentinel, dissolve-on-2b born-mark note on placeholder_arm_target.

Co-authored-by: Cursor <cursoragent@cursor.com>
---
 src/v2/stage0/src/coproduct_reflection.rs     | 141 +++++++++++-------
 src/v2/stage0/src/v2_interpreter.rs           |   8 +-
 .../coproduct_reflection_conformance_test.rs  |  18 ++-
 .../claim/extdeps/coordination_claims.dag     |   6 +-
 4 files changed, 114 insertions(+), 59 deletions(-)

diff --git a/src/v2/stage0/src/coproduct_reflection.rs b/src/v2/stage0/src/coproduct_reflection.rs
index 4b384e71e38..37572a39d18 100644
--- a/src/v2/stage0/src/coproduct_reflection.rs
+++ b/src/v2/stage0/src/coproduct_reflection.rs
@@ -2,7 +2,7 @@
 //!
 //! - `resolve_type_node`: compiler Disj type item → substrate `Node` Value (dissolves when v4
 //!   gains compile-graph access).
-//! - `syntactic_coproduct_arm_keys`: Path-3 raw-source text scan (irreducible I/O boundary; stays Rust).
+//! - `syntactic_coproduct_arm_keys`: Path-3 raw-source text scan over in-memory compile source.
 
 use std::collections::HashMap;
 use std::rc::Rc;
@@ -109,6 +109,7 @@ fn edge_named(ctx: &InterpContext, name: &str, target: Value) -> Value {
     }
 }
 
+// dissolve-on-2b: INERT placeholder target until coproduct_arms reads real arm targets (gunbc#4863).
 fn placeholder_arm_target(ctx: &InterpContext) -> Value {
     node_record(
         ctx,
@@ -138,81 +139,97 @@ pub fn marshal_disj_type_item(ctx: &InterpContext, item: &Rc<Node>) -> InterpRes
     ))
 }
 
-/// Bootstrap only: resolve declaring source path via cwd walk + optional GUNBC_ROOT.
-/// Dissolve-on-arrival: compile-graph span.file is the sole authority once claim-run
-/// transport no longer needs off-disk reads for Path-3 witnesses.
-fn resolve_source_file_path(file: &str) -> InterpResult<String> {
-    let path = std::path::Path::new(file);
-    if path.is_absolute() && path.exists() {
-        return Ok(file.to_string());
-    }
-    if path.exists() {
-        return Ok(file.to_string());
-    }
-    if let Ok(mut dir) = std::env::current_dir() {
-        loop {
-            let candidate = dir.join(file);
-            if candidate.exists() {
-                return Ok(candidate.to_string_lossy().into_owned());
-            }
-            if !dir.pop() {
-                break;
-            }
-        }
-    }
-    if let Ok(root) = std::env::var("GUNBC_ROOT") {
-        let candidate = std::path::Path::new(&root).join(file);
-        if candidate.exists() {
-            return Ok(candidate.to_string_lossy().into_owned());
-        }
-    }
-    Err(InterpError::TypeError {
-        msg: format!("coproduct reflection: cannot resolve source path `{file}`"),
-    })
+fn source_text_from_ctx(ctx: &InterpContext, file: &str) -> InterpResult<String> {
+    let indices = ctx.source_indices();
+    let index = indices.get(file).ok_or_else(|| InterpError::TypeError {
+        msg: format!("syntactic coproduct arm keys: no in-memory source for `{file}`"),
+    })?;
+    let len = index.char_codes.len() as i64;
+    Ok(crate::v2_rt::chars_to_string(&index.char_codes, 0, len))
 }
 
 /// Path 3: grammar-level arm labels from `type Name = Arm | Arm | ...` in source text.
-pub fn syntactic_coproduct_arm_labels(file: &str, type_name: &str) -> InterpResult<Vec<String>> {
-    let resolved = resolve_source_file_path(file)?;
-    let content = std::fs::read_to_string(&resolved).map_err(|e| InterpError::TypeError {
-        msg: format!("syntactic coproduct arm keys: cannot read `{resolved}`: {e}"),
-    })?;
-    extract_type_sum_arm_labels(&content, type_name).ok_or_else(|| InterpError::TypeError {
-        msg: format!("syntactic coproduct arm keys: `{type_name}` not found in `{file}`"),
-    })
+pub fn syntactic_coproduct_arm_labels(
+    ctx: &InterpContext,
+    file: &str,
+    type_name: &str,
+) -> InterpResult<Vec<String>> {
+    let content = source_text_from_ctx(ctx, file)?;
+    extract_type_sum_arm_labels(&content, type_name).map_err(|msg| InterpError::TypeError { msg })
+}
+
+fn same_line_leading_comment(s: &str) -> bool {
+    match s.find('\n') {
+        Some(0) => false,
+        Some(nl) => s[..nl].trim().starts_with("//"),
+        None => s.trim().starts_with("//"),
+    }
 }
 
-fn extract_type_sum_arm_labels(source: &str, type_name: &str) -> Option<Vec<String>> {
-    let start = find_type_decl_start(source, type_name)?;
+fn extract_type_sum_arm_labels(source: &str, type_name: &str) -> Result<Vec<String>, String> {
+    let start = find_type_decl_start(source, type_name).ok_or_else(|| {
+        format!("syntactic coproduct arm keys: `{type_name}` not found in source")
+    })?;
     let needle = format!("type {type_name}");
     let after_type = &source[start + needle.len()..];
-    let eq_rel = after_type.find('=')?;
+    let eq_rel = after_type
+        .find('=')
+        .ok_or_else(|| format!("syntactic coproduct arm keys: `{type_name}` missing `=`"))?;
     let mut rest = after_type[eq_rel + 1..].trim_start();
     let mut arms = Vec::new();
     loop {
         rest = rest.trim_start();
-        if rest.is_empty() || rest.starts_with("//") {
+        if rest.is_empty() {
             break;
         }
         if rest.starts_with('|') {
             rest = rest[1..].trim_start();
         }
-        let arm_name = read_identifier_prefix(rest)?;
+        let arm_name = read_identifier_prefix(rest).ok_or_else(|| {
+            format!("syntactic coproduct arm keys: expected arm identifier for `{type_name}`")
+        })?;
         arms.push(arm_name.0);
-        rest = arm_name.1.trim_start();
+        rest = arm_name.1;
+        if same_line_leading_comment(rest) {
+            return Err(format!(
+                "syntactic coproduct arm keys: unexpected `//` comment mid-declaration for `{type_name}`"
+            ));
+        }
+        rest = rest.trim_start();
         if rest.starts_with('{') {
-            rest = skip_braced(rest)?;
+            rest = skip_braced(rest).ok_or_else(|| {
+                format!("syntactic coproduct arm keys: unclosed `{{` in `{type_name}` arm payload")
+            })?;
         }
         rest = rest.trim_start();
-        if !rest.starts_with('|') {
+        if rest.is_empty() {
+            break;
+        }
+        if rest.starts_with("//") {
             break;
         }
+        if !rest.starts_with('|') {
+            let suffix = rest.trim_start();
+            if suffix.starts_with("//")
+                || suffix.starts_with("type ")
+                || suffix.starts_with("fn ")
+                || suffix.starts_with("module ")
+                || suffix.starts_with("import ")
+            {
+                break;
+            }
+            let peek = rest.chars().next().unwrap_or('\0');
+            return Err(format!(
+                "syntactic coproduct arm keys: unexpected token `{peek}` mid-declaration for `{type_name}`"
+            ));
+        }
     }
     if arms.is_empty() {
-        None
-    } else {
-        Some(arms)
+        return Err(format!(
+            "syntactic coproduct arm keys: `{type_name}` has no arms"
+        ));
     }
+    Ok(arms)
 }
 
 fn find_type_decl_start(source: &str, type_name: &str) -> Option<usize> {
@@ -285,7 +302,7 @@ pub fn eval_syntactic_coproduct_arm_keys(
 ) -> InterpResult<Value> {
     let type_name = expect_symbol(args.first().map(|(_, v)| v), "syntactic_coproduct_arm_keys")?;
     let (_, file) = type_item_by_name(ctx, type_name)?;
-    let labels = syntactic_coproduct_arm_labels(&file, type_name)?;
+    let labels = syntactic_coproduct_arm_labels(ctx, &file, type_name)?;
     let items: Vec<Value> = labels
         .iter()
         .map(|label| Value::Str(label.clone()))
@@ -448,4 +465,24 @@ mod tests {
             vec!["Atom", "Conj"]
         );
     }
+
+    #[test]
+    fn syntactic_extractor_fails_loud_on_mid_decl_comment() {
+        let source = "type Connective = Atom | Conj // trailing\n";
+        let err = extract_type_sum_arm_labels(source, "Connective").unwrap_err();
+        assert!(
+            err.contains("//"),
+            "expected mid-decl comment diagnostic, got: {err}"
+        );
+    }
+
+    #[test]
+    fn syntactic_extractor_fails_loud_on_unexpected_token_mid_decl() {
+        let source = "type Connective = Atom , Conj\n";
+        let err = extract_type_sum_arm_labels(source, "Connective").unwrap_err();
+        assert!(
+            err.contains("unexpected token"),
+            "expected unexpected-token diagnostic, got: {err}"
+        );
+    }
 }
diff --git a/src/v2/stage0/src/v2_interpreter.rs b/src/v2/stage0/src/v2_interpreter.rs
index 0b6bf8e0a79..6dda35040e9 100644
--- a/src/v2/stage0/src/v2_interpreter.rs
+++ b/src/v2/stage0/src/v2_interpreter.rs
@@ -2117,7 +2117,13 @@ fn match_pattern(
 // v4.std.node coproduct reflection intercept (module-scoped bootstrap seam)
 // ---------------------------------------------------------------------------
 
-const STD_NODE_BRIDGE_FNS: &[&str] = &["resolve_type_node", "syntactic_coproduct_arm_keys"];
+pub(crate) const STD_NODE_BRIDGE_FNS: &[&str] =
+    &["resolve_type_node", "syntactic_coproduct_arm_keys"];
+
+/// Sentinel surface for tests: every name here must be wired in `eval_call`'s bridge intercept.
+pub fn std_node_bridge_fn_names() -> &'static [&'static str] {
+    STD_NODE_BRIDGE_FNS
+}
 
 fn is_v4_std_node_bridge_call(ctx: &InterpContext, func_name: &str) -> bool {
     if !STD_NODE_BRIDGE_FNS.contains(&func_name) {
diff --git a/src/v2/tests/src/coproduct_reflection_conformance_test.rs b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
index b4868bd772e..1c0f4c9afd3 100644
--- a/src/v2/tests/src/coproduct_reflection_conformance_test.rs
+++ b/src/v2/tests/src/coproduct_reflection_conformance_test.rs
@@ -70,9 +70,23 @@ fn symbol_list_strings(val: &Value) -> Vec<String> {
         .collect()
 }
 
+#[test]
+fn coproduct_reflection_std_node_bridge_fns_are_intercept_wired() {
+    let source = include_str!("../../stage0/src/v2_interpreter.rs");
+    for name in v2_interpreter::std_node_bridge_fn_names() {
+        assert!(
+            source.contains(&format!("\"{name}\" =>")),
+            "eval_call intercept must wire v4.std.node bridge `{name}`"
+        );
+    }
+    assert!(
+        source.contains("is_v4_std_node_bridge_call"),
+        "eval_call must gate v4.std.node bridge dispatch"
+    );
+}
+
 #[test]
 fn coproduct_reflection_path3_connective_behavior_conformance_holds() {
-    std::env::set_var("GUNBC_ROOT", workspace_root());
     let resolved = compile_to_resolved(Rc::new(cert_sources()));
     assert_resolved_ok(&resolved);
     match run_witness(&resolved, WITNESS_FN) {
@@ -85,7 +99,6 @@ fn coproduct_reflection_path3_connective_behavior_conformance_holds() {
 
 #[test]
 fn coproduct_reflection_connective_behavior_arm_sets_are_distinct() {
-    std::env::set_var("GUNBC_ROOT", workspace_root());
     let resolved = compile_to_resolved(Rc::new(cert_sources()));
     assert_resolved_ok(&resolved);
     match run_witness(
@@ -99,7 +112,6 @@ fn coproduct_reflection_connective_behavior_arm_sets_are_distinct() {
 
 #[test]
 fn coproduct_reflection_path3_witness_fails_on_dropped_disj_arm() {
-    std::env::set_var("GUNBC_ROOT", workspace_root());
     let resolved = compile_to_resolved(Rc::new(cert_sources()));
     assert_resolved_ok(&resolved);
     let graph = resolved
diff --git a/src/v4/test/claim/extdeps/coordination_claims.dag b/src/v4/test/claim/extdeps/coordination_claims.dag
index 21d5e9896ee..a4bbe5f5162 100644
--- a/src/v4/test/claim/extdeps/coordination_claims.dag
+++ b/src/v4/test/claim/extdeps/coordination_claims.dag
@@ -15,9 +15,9 @@
 // .rs smoke are deleted in the same PR (their content is proven here by execution). The
 // remaining B-class receipts (WireContractFacts/WireContract record-field shapes,
 // SettlementGuarantee/ConsistencyGuarantee shared-discriminant) were deleted with the smoke
-// file per the white-box sweep. Reflection stays banned outside the scoped lift in
-// docs/design-coproduct-arm-reflection.md §7 (compile-time closed-coproduct projection +
-// gate-covered fail-closed only); decl-shape mirrors remain 2FA-for-code elsewhere.
+// file per the white-box sweep. Reflection stays banned outside the scoped lift
+// ratified in gunbc#4861 (compile-time closed-coproduct projection + gate-covered fail-closed
+// only; inline scope bound here is authoritative); decl-shape mirrors remain 2FA-for-code elsewhere.
 // Importing v4.extdeps.coordination forces v2 to tokenize/parse/infer it, so the
 // parse-surface fact rides every witness below.