briansrls · May 15, 2026 · May 15, 2026 · May 15, 2026 · May 15, 2026 · May 15, 2026
diff --git a/THESIS.md b/THESIS.md
@@ -223,7 +223,7 @@ Every claim the thesis makes, in one place. The ROADMAP tracks progress toward e
 - See [`docs/thesis/what-else-falls-out.md`](docs/thesis/what-else-falls-out.md) §"Two shapes of omni-emission" for the full Shape A vs Shape B treatment, including the per-target cost structure and the load-bearing reason the distinction must not be blurred.
 
 **Meta-process modeling:**
-- Bootstrap, CI, build orchestration, dev process modeled as .dag workflows.
+- Bootstrap, CI, and build orchestration modeled as .dag workflows (`workflow/bootstrap.dag`, `workflow/ci.dag`). (The "dev/work-direction process modeled as .dag" claim was retracted 2026-05-15, operator-ratified — see facet 4 below; the project does not model its own work-direction.)
 - `dag run` is the primary execution path.
 - Adding a CI gate, a Node field, or a target language requires editing one .dag file.
 
@@ -257,20 +257,27 @@ Self-hosting is not one capability; it's four. All four are targets.
    declarations. Everything ports to `.dag`. **Pure Bootstrap's secondary
    deliverable, couples to testgen.**
 
-4. **Recursive-flex / self-application** (NEW 2026-05-04; per Director
-   ratification at [gunbc#828 inbox-4374342708](https://github.com/gunb-ai/gunbc/issues/828)).
-   gunbc applies its own correctness/cost/parallelism/timing lenses to
-   its own build pipeline. The compiler that compiles gunbc programs
-   validates the workflow that produces gunbc itself. The same lens
-   framework users get for their own programs applies recursively to
-   gunbc's own runtime behavior — modeling its CI workflow as `.dag`
-   data, applying typed lenses for cost / complexity / parallelism /
-   timing, surfacing dependency-tracking and observation-driven
-   validation as structural facts. **R3 deliverable** (T-Workflow-As-Data
-   substrate + T-Lens-Self-Application demonstration; per `r3-structure.md`
-   §T-Workflow-As-Data + §T-Lens-Self-Application). Distinguishes
-   gunbc from compilers that don't validate their own production
-   pipeline — observation-driven lens-shape class is sui-generis.
+4. **Recursive-flex / self-application** (NEW 2026-05-04; **narrowed
+   2026-05-15, operator-ratified**). gunbc applies its own correctness/
+   cost/parallelism/timing lenses to its own **build/CI pipeline**, which
+   is modeled as `.dag` data (`workflow/bootstrap.dag`,
+   `workflow/ci.dag`). The same lens framework users get for their own
+   programs applies recursively to gunbc's own build/CI behavior —
+   typed lenses for cost / complexity / parallelism / timing over the
+   pipeline that produces gunbc itself. This distinguishes gunbc from
+   compilers that don't validate their own production pipeline.
+
+   **Retracted (2026-05-15, operator-ratified):** the original
+   "T-Workflow-As-Data substrate" sub-claim — modeling gunbc's *own
+   work-direction* (briefs / worker-outputs / cycles / retirement /
+   doc-anchors) as `.dag` data. The project does not model its own
+   work-direction; the compiler model self-justifies (rationale
+   emergent from composition), so there is no meta-layer to narrate it.
+   Honest framing per this thesis's own no-fabrication discipline: this
+   facet now claims only lens self-application to the build/CI pipeline
+   (which survives via `bootstrap.dag`/`ci.dag`), not process-self-
+   modeling. The `workflow/` substrate is correspondingly `{ bootstrap,
+   ci }` only (STRUCTURE.md invariant 6).
 
 Cost-of-change: editing any compiler concept — a new pass, substrate fact,
 target-language detail, or pipeline/contract test assertion — stays at

diff --git a/src/v4/BRIEF_TEMPLATE.md b/src/v4/BRIEF_TEMPLATE.md
@@ -49,8 +49,6 @@ DEFINITION OF DONE:
   - Implementation present in declared file
   - Compiles via v2 binary (bootstrap)
   - TestClaim suite covers golden + Diagnostic paths
-  - WorkerOutput instance authored: declares which substrate fact dissolves
-    which prior residual (workflow/worker_output.dag schema)
   - Round-trips through any downstream pipeline stage already implemented
 
 YOUR DECISIONS (the actual modeling work):
@@ -101,9 +99,16 @@ The shape is the structural fix to v3's failure mode. Every constraint exists be
 - **Immutable I/O contract** — v3 had drift in worker outputs because contracts were prose; here they're declared in the file header before any work begins.
 - **Substrate whitelist** — v3 workers reached into adjacent substrate ad-hoc, creating the cascade-edit problem; here the substrate surface is closed.
 - **No new files** — v3's paper-shrink V1 (template-relocation to `tools/*.rs.in`) and V2 (module-relocation to `pub mod`) both required adding files; here both are syntactically impossible because the worker has no authority to add files.
-- **WorkerOutput instance with `dissolves` field** — v3's "retirement" was a list-length ratchet; here it's a structural predicate the worker declares + the system verifies.
 - **Escalation triggers explicit** — v3 had no clear "stop and surface" discipline; here it's a list, and triggering escalation is a feature, not a failure.
 
+(The former "WorkerOutput instance with `dissolves` field" point was removed
+2026-05-15, operator-ratified: the work-direction meta-layer
+(`workflow/worker_output.dag` et al.) was cut — the project does not model
+its own work-direction, and the compiler model self-justifies. v3's
+paper-shrink failure mode is now contained by the immutable-contract +
+no-new-files + closed-substrate constraints above plus the bootstrap
+reproduction guarantee, not a worker-output substrate.)
+
 ## Authoring discipline (for the operator)
 
 When filling in a brief from this template:

diff --git a/src/v4/STRUCTURE.md b/src/v4/STRUCTURE.md
@@ -83,12 +83,12 @@ src/v4/
     affected_set.dag     # incremental re-exec frontier; replaces detect-affected shell (Phase 1.5)
     application.dag      # apply_lens surface — opt-in depth + ONLY advisory→fail-closed bridge
 
-  workflow/              # recursive-flex — work-direction in .dag (7 files)
-    brief.dag            # typed Brief schema
-    worker_output.dag    # WorkerOutput { dissolves: Set<HandResidual>, cited_anchor }
-    doc_anchor.dag       # typed DocAnchor pointers into authority docs
-    retirement.dag       # structural Retirement predicate (no list-length gaming)
-    cycle.dag            # work cycle as data, lens-readable
+  workflow/              # meta-process as data (2 files; the v3-derived
+                         # work-direction substrate — brief/worker_output/
+                         # cycle/retirement/doc_anchor — was cut
+                         # 2026-05-15, operator-ratified: the project does
+                         # not model its own work-direction; the compiler
+                         # model self-justifies, no meta-layer narrates it)
     bootstrap.dag        # bootstrap orchestration AS DATA (seed-once → self-host
                          # → fixed-point); v2 interprets it; no build.rs/shell
     ci.dag               # CI pipeline AS DATA; .github/workflows/ci.yml is derived
@@ -108,9 +108,10 @@ src/v4/
     fixture/             # canonical input programs
 ```
 
-**Total: 68 .dag files + 5 docs + 5 .gitkeep = 78 files.** (Per invariant
+**Total: 63 .dag files + 5 docs + 5 .gitkeep = 73 files.** (Per invariant
 #1 the enumeration above — not the count — is authoritative; the count is
-a checksum, updated on every operator-ratified file addition.)
+a checksum, updated on every operator-ratified file addition/removal.
+−5 .dag 2026-05-15: work-direction meta-layer cut, operator-ratified.)
 
 ## Scalar/numeric concept decomposition
 
@@ -289,7 +290,7 @@ These are non-negotiable across all v4 work:
 3. **No file-splitting without operator ratification.** Each file is a typed pure function. If a worker thinks `04_infer.dag` should be five files, that's a substrate-design question, not a worker decision.
 4. **Cost-of-change = 1.** Adding a new type/expression/transport edits exactly one file. If a change ripples, the substrate is wrong.
 5. **Tests are TestClaim data.** Zero hand-Rust tests. Test surface lives in `test/claim/`.
-6. **Workflow substrate first.** `workflow/*.dag` is implemented BEFORE any compiler work, so worker outputs are typed Brief/WorkerOutput/Retirement instances from day 1. The recursive-flex move is structural, not aspirational.
+6. **Meta-process as data (narrowed 2026-05-15, operator-ratified).** `workflow/` is now exactly `bootstrap.dag` (the bootstrap chain — load-bearing per invariant 7) and `ci.dag` (CI pipeline) — both `.dag` data, never `build.rs`/shell/hand-authored YAML. The v3-derived **work-direction substrate** (briefs / worker-outputs / cycles / retirement / doc-anchors modeled as data — the original "recursive-flex implement-before-compiler" claim) is **retracted**: the project does not model its own work-direction, and the compiler model self-justifies (rationale emergent from composition), so no meta-layer narrates it. Lens self-application to gunbc's own build/CI pipeline survives via `bootstrap.dag`/`ci.dag`; modeling our own *process* does not.
 7. **`.dag` is the sole editable authority; Rust is never authority.**
    "Off Rust" means: no Rust is editable authority — not "no Rust exists
    anywhere" (the CPU always has a host; the seed is always *some*

diff --git a/src/v4/TASKS.md b/src/v4/TASKS.md
@@ -22,7 +22,8 @@ Phase 1 (parallel — substrate foundation):
   T-4.12 extdeps/languages/llvm_ir.dag   [needs T-1, T-2; B2-OMNI probe — generalize DOWN the stack (SSA IR)]
   T-4.13 extdeps/languages/machine_code.dag  [needs T-1; B2-OMNI probe — bottom of stack; disassembly = extreme fail-closed]
   T-4.14 extdeps/languages/ptx.dag       [needs T-1, T-2; B2-OMNI + IN-B probe — SIMT data-parallel vs the 5 behaviors]
-  T-5   workflow/* (5 files)             [needs T-1; FIRST IN EXECUTION]
+  T-5   REMOVED 2026-05-15 (operator-ratified) — work-direction meta-layer
+        cut; only workflow/bootstrap.dag (T-20) + workflow/ci.dag (T-24) remain
 
 Phase 1.5 (test + bootstrap substrate — early, before compiler stages):
   T-19  lens/testgen.dag                 [needs T-1, T-2, T-3]
@@ -177,20 +178,24 @@ flat — dispatch in waves):
 
 ---
 
-### T-5: workflow/* — recursive-flex (FIRST IN EXECUTION ORDER)
+### T-5: REMOVED — work-direction meta-layer cut (operator-ratified 2026-05-15)
 
-**File**: 5 files in `src/v4/workflow/`
-**Why FIRST**: this IS the structural fix to v3's hierarchy/gaming failure. Implement workflow substrate before any compiler work, so every subsequent task's WorkerOutput is a typed instance.
+T-5 ("workflow/* — recursive-flex": `brief.dag`, `worker_output.dag`,
+`cycle.dag`, `retirement.dag`, `doc_anchor.dag`) is **deleted**. Rationale
+(operator-ratified): modeling gunbc's *own work-direction* as `.dag` data
+is not used by the project; the compiler model self-justifies (rationale
+emergent from composition), so no meta-layer is needed to narrate it.
+Tombstone retained (not silently dropped) so the decision is on record.
 
-**Modeling decisions**:
-- Brief contract shape (what fields are mandatory?)
-- Retirement predicate (A3, operator-ratified 2026-05-15): `retired` is a REPRODUCTION, never a count. `retired ⟺ rebuild-from-(.dag + frozen-pinned seed)-only reproduces the pinned hash ∧ the seed's own hash matches its pin`. `HandResidual` = the Rust the .dag-rebuild cannot reproduce — empty by reproduction, not by count (defeats paper-shrink: relocation/inlining is non-seed Rust, removed by the test). NOT un-gameable (Trusting-Trust — pin/CI/seed are editable); its job is early/loud surfacing per-PR on the affected set so gaming is un-missable + operator-routed. Seed trust = named axiom, not proof. Enforcement = operator-ratification + STOP-culture; structure makes defection conspicuous, not impossible. Typed workflow substrate, NOT a CI grep (feedback_no_textual_enforcement_bridges).
-- Cycle data: lens-readable progression vs prose status
+What survives in `workflow/`, as standalone tasks — these are *compiler
+build infrastructure*, not the work-direction meta-layer:
+- **`workflow/bootstrap.dag` → T-20** (the bootstrap chain; load-bearing
+  for the anti-regression guarantee, STRUCTURE.md invariant 7).
+- **`workflow/ci.dag` → T-24** (CI pipeline as data).
 
-**Reference**:
-- This conversation (the failure mode that motivated this substrate)
-- `feedback_doc_authority_must_propagate_to_execution_authority` (memory)
-- `feedback_paper_shrink_variants` (memory) — the failure modes to refuse
+THESIS facet 4 / STRUCTURE.md invariant 6 narrowed correspondingly.
+The 5 deleted files were never filled (scaffolds only); nothing in the
+substrate imported them, so the cut is a pure scope reduction.
 
 ---
 

diff --git a/src/v4/std/node.dag b/src/v4/std/node.dag
@@ -159,6 +159,28 @@ type Hash
 // declaration — a visible diff routed to operator ratification (per
 // STRUCTURE.md A3: the substrate does not magically refuse it; the edit
 // is loud and un-missable). There is no `Other` / open-ended variant.
+//
+// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) —
+// 🟢 GREEN (terminal). Ledger — five patterns attempted:
+//   1. Fact placement — FAILS: every pipeline stage (parse/normalize/
+//      infer/emit) dispatches on the connective; it is the shared
+//      classifier, not a per-consumer scattered fact.
+//   2. Variant-is-data — FAILS: the six are structurally distinct
+//      (Atom carries a Symbol; Conj/Disj labeled; Arrow/Cardinality/
+//      Instantiation positional) — no uniform label space to fold.
+//   3. Algebraic form — N/A by construction: this IS the type-substrate
+//      root (THESIS:202); the connectives do not trace to a richer
+//      std/ algebra — they are the source other structure grounds in.
+//   4. Dimensional — FAILS: a node carries EXACTLY ONE connective;
+//      genuine alternatives, never simultaneous coordinates.
+//   5. Parameterized family — FAILS: the six are structurally
+//      heterogeneous (Atom carries a Symbol; Conj/Disj labeled;
+//      Arrow/Cardinality/Instantiation positional, distinct arities/
+//      semantics) — NOT one generic `F<X>` / projection over a source
+//      set X (Practice 7). No enumeration-to-projection collapse exists.
+// Terminal: the closed 6 type connectives; a 7th is the C1 stop-signal
+// (a visible ratified edit to this declaration, STRUCTURE.md
+// commitment #1). Irreducible substrate root.
 type Connective
   = Atom { identity: Symbol }
   | Conj
@@ -179,6 +201,25 @@ type Connective
 //
 // CLOSED (C1 stop-signal). A sixth behavior is an edit to THIS
 // declaration — a visible diff routed to operator ratification.
+//
+// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) —
+// 🟢 GREEN (terminal). Ledger — five patterns attempted:
+//   1. Fact placement — FAILS: every computation-substrate consumer
+//      dispatches on the behavior; shared classifier, not scattered.
+//   2. Variant-is-data — FAILS: the five are distinct computation
+//      kinds (the typed-total-λ fragment per INVARIANTS — Transform=
+//      application, Bind=let, Branch=sums, Loop=bounded rec, Value);
+//      no uniform label space.
+//   3. Algebraic form — N/A by construction: this IS the computation-
+//      substrate root (THESIS:202); no richer std/ source.
+//   4. Dimensional — FAILS: a computation node carries EXACTLY ONE
+//      behavior; alternatives, not coordinates.
+//   5. Parameterized family — FAILS: the five are distinct computation
+//      kinds (the typed-total-λ fragment — Transform=application,
+//      Bind=let, Branch=sums, Loop=bounded rec, Value) — NOT one
+//      generic `F<X>` / projection over a source set (Practice 7).
+// Terminal: the closed 5 L1 behaviors; a 6th is the C1 stop-signal
+// (STRUCTURE.md commitment #1). Irreducible substrate root.
 type Behavior
   = Value
   | Transform
@@ -197,6 +238,25 @@ type Behavior
 // enums stay orthogonal closed sets; `NodeKind` merely selects which
 // one applies (THESIS:198-203 — computation references type by edge, it
 // does not co-locate the two coordinates on one node).
+//
+// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) —
+// 🟢 GREEN (terminal). Ledger — five patterns attempted:
+//   1. Fact placement — FAILS: every Node consumer branches on kind
+//      to know which substrate it is in; shared, not scattered.
+//   2. Variant-is-data — FAILS: TypeNode carries a Connective,
+//      ComputationNode a Behavior — disjoint payloads, no uniform
+//      label space.
+//   3. Algebraic form — N/A by construction: the two-coordinated-
+//      substrate split IS the substrate shape (THESIS:198-203); no
+//      richer source.
+//   4. Dimensional — FAILS: Shape S — a Node is in EXACTLY ONE
+//      substrate, never both; alternatives, not coordinates (co-
+//      locating both would conflate the two independent C1 closures).
+//   5. Parameterized family — FAILS: TypeNode/ComputationNode carry
+//      disjoint payloads (Connective vs Behavior) — not one generic
+//      `F<X>` / projection over a source set (Practice 7); it is the
+//      irreducible two-coordinated-substrate selector.
+// Terminal: the binary type/computation substrate split; irreducible.
 type NodeKind
   = TypeNode { connective: Connective }
   | ComputationNode { behavior: Behavior }
@@ -218,6 +278,26 @@ type NodeKind
 // negative / gapped / duplicate / out-of-order indices representable.
 // With no index field those illegal states are STRUCTURALLY
 // UNREPRESENTABLE — not "rejected by a checker."
+//
+// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) —
+// 🟢 GREEN (terminal). Ledger — five patterns attempted:
+//   1. Fact placement — FAILS: every edge consumer branches on the
+//      label kind uniformly; shared, not scattered.
+//   2. Variant-is-data — FAILS: `Named` carries a Symbol; `Positional`
+//      is a bare marker whose identity IS list position. Folding to a
+//      uniform record means a stored index — the INVARIANTS P2
+//      duplicate-authority anti-pattern this type exists to forbid.
+//   3. Algebraic form — N/A by construction: the two child-addressing
+//      modes are the edge-discipline primitive; no richer std/ source.
+//   4. Dimensional — FAILS: an edge is EITHER named OR positional,
+//      never both; alternatives, not coordinates.
+//   5. Parameterized family — FAILS: `Named` carries a Symbol,
+//      `Positional` is a bare marker (identity = list position) —
+//      heterogeneous, NOT one generic `F<X>` / projection over a
+//      source set (Practice 7).
+// Terminal: the two child-addressing modes; the no-stored-index design
+// makes illegal index states unrepresentable — this IS already the
+// dissolved form, not a compression of one.
 type EdgeLabel
   = Named { name: Symbol }
   | Positional
@@ -269,6 +349,27 @@ type Node {
 // stays a check here is the D3 no-redesign call, not an A3-style
 // impossibility. (Contrast: the closed `Connective` enum below — a 7th
 // connective genuinely IS the A3 case, an edit to this file.)
+//
+// Coproduct dissolution (Practice 4 / modeling-discipline.md §4) —
+// 🟢 GREEN (terminal). Ledger — five patterns attempted:
+//   1. Fact placement — FAILS: derived uniformly from the connective
+//      via `connective_edge_discipline` and consumed by
+//      `node_well_formed`; single authority, not scattered.
+//   2. Variant-is-data — FAILS: the three are distinct structural
+//      rules (no edges / labeled+distinct / positional), not a uniform
+//      label space.
+//   3. Algebraic form — N/A by construction: it is the projection of
+//      the closed `Connective` set's edge rule; it IS the rule, no
+//      richer source.
+//   4. Dimensional — FAILS: a connective fixes EXACTLY ONE discipline;
+//      alternatives, not coordinates.
+//   5. Parameterized family — FAILS: the three are distinct structural
+//      rules (no edges / labeled+distinct / positional) — NOT one
+//      generic `F<X>` / projection over a source set (Practice 7);
+//      it is the irreducible projection OF the closed `Connective` set
+//      onto its edge rule, already in dissolved form.
+// Terminal: the three connective edge-disciplines; a closed classifier
+// over the closed `Connective` set — irreducible with it.
 type EdgeDiscipline
   = NoEdges
   | LabeledEdges