briansrls · Jun 1, 2026 · Jun 1, 2026 · Jun 1, 2026 · Jun 1, 2026 · Jun 1, 2026
diff --git a/docs/planning/v4-active-authority-map-2026-06-01.md b/docs/planning/v4-active-authority-map-2026-06-01.md
@@ -0,0 +1,108 @@
+# v4 Active authority map (Modeling DFS Arbiter)
+
+> **Status:** LIVING — updated by Modeling DFS Arbiter (`proud-fox-405`) as worksheets ratify.
+> **Date:** 2026-06-01
+> **Purpose:** Prevent parallel carriers for the same concept across Rust / Go / Python / TS RCA lanes (operator directive post-#4137 §11.2).
+> **Companion:** `docs/planning/v4-predicate-dependency-graph-2026-06-01-eod.md` §11; per-class worksheets under `docs/planning/`.
+
+---
+
+## How to read this map
+
+| Column | Meaning |
+| ------ | ------- |
+| **Concept** | Shared modeling fact (not a lane name) |
+| **Canonical home** | Single `std/` / `extdeps/` / compiler file that owns the type or row shape |
+| **Per-target rows** | Where language-specific realization lives (`rust.dag`, `go.dag`, …) |
+| **§8 state** | `APPROVED` = impl dispatchable; `PENDING` = worksheet in review; `BLOCKED` = prerequisite |
+| **Forbidden** | Parallel authorities RCA managers must not invent |
+
+---
+
+## Cross-target substrate (shared carriers)
+
+| Concept | Canonical home | Per-target rows | §8 state | Forbidden |
+| ------- | -------------- | ----------------- | -------- | --------- |
+| **TargetAtomRealization** | `src/v4/std/target_model.dag` | `rust.dag`, `go.dag`, `python.dag`, `typescript.dag` | Rust APPROVED (#4099); Go APPROVED (#4149); TS PENDING (atom after type-expr; §8 follow-up) | `GoAtomRealization`, duplicate carrier in `go.dag` |
+| **TargetTypeExpressionProjection** | `src/v4/std/target_model.dag` | same extdeps | Rust APPROVED (#4124); Go APPROVED (#4149); TS PENDING (strict order **before** atom) | Name-keyed `Outcome`/`Witness` tables in emit |
+| **TargetCollectionRealization** | `src/v4/std/target_model.dag` | same extdeps | SG-5/6 APPROVED; **SG-COLLECTION-PROJECTION** PENDING (vivid-lynx-81) | `Vec<Rc<T>>` shim in emit without monoid→Vec row |
+| **TargetBundleEdge / RC layering** | `v4.std.target_model` (`TargetBundleEdge`) | emit consumes via `target_bundle_edge_*` | SG-RC APPROVED (#4100) | Conflating with collection projection |
+| **Module graph / export surface** | `03_name_resolve.dag` + `05_emit_rust.dag` (M1) | follow-on `TargetModuleExportSurface` in `target_model` | SG-8 §8 APPROVED (#4143) | Per-error `pub use` patch tables |
+| **LeafModelClaimId + fixtures** | `src/v4/std/leaf_model_verification.dag` | claim files under `test/claim/language_model/` | Framework APPROVED; per-target claims PENDING | Parallel claim modules outside std IDs |
+| **TargetCompileVerdict** | `leaf_model_verification.dag` | `target_diagnostic_*` + `leaf_model_toolchain_*` symbols | LANDED (Rust); Go/TS worksheets route here for compile-bound claims | `TargetGoCompileVerdict`, `TargetTypeScriptCompileVerdict` |
+| **TargetRuntimeExerciseVerdict** | `leaf_model_verification.dag` (**additive**, shared) | same pattern | PENDING (Go R2b, TS R2b worksheets propose) | Per-target `Target*RuntimeVerdict` types |
+| **TargetPythonExerciseVerdict** | `leaf_model_verification.dag` | Python L0 only | LANDED (#4117) | Replacing L1/L2 runtime with stdout grep |
+| **TargetStaticAnalysisInvocation** | `leaf_model_verification.dag` or `host_run` (**proposed**, Python worksheet A) | pyright/mypy profiles, later `tsc --noEmit` | PENDING (Python L1 static worksheet) | CI-only pyright without modeled profile |
+| **BootstrapEvaluatorCorpusRuntimeEval** | `testclaim_corpus_runner.dag` + consume `05_eval.dag` | `v4_evaluator_runtime_id` pin | APPROVED (#4143); impl PENDING (`neat-hawk-413`) | Authoring-time `data run_*` as runtime pass |
+| **CiUpsertStep / TestClaim corpus CI** | `src/v4/workflow/ci.dag` | host scripts dissolve-on-arrival | P5 Layer 2 APPROVED (#4115) | New `ci.yml` shell without Upsert row |
+| **P5 strict runtime gate** | `BootstrapEvaluatorCorpusRuntimeEval` (above) | `scripts/v4-testclaim-corpus-eval.sh` amend | Worksheet APPROVED; gate OPEN until impl | `authoring_time_verdict_surface` as P5 GREEN |
+
+---
+
+## Operator enforcement holds (cross-lane)
+
+| Hold | Enforced by | Violation signal |
+| ---- | ----------- | ---------------- |
+| No Go/TS shell in `ci.yml` without `CiUpsertStep` row | CI Manager + Arbiter | New `scripts/v4-leaf-model-{go,ts}-*` wired only in YAML |
+| No TS atom impl before TS `TargetTypeExpressionProjection` row | Arbiter dispatch order | Atom worker before type-expr §8 |
+| No Python L2 as stdout/stderr string shell compare | Python worksheet B + Arbiter | `grep`/`diff` on process output as final receipt |
+| No SG-2 residual carrier-name special-casing | Arbiter | New `if carrier == "Outcome"` in translate before SG-RC+SG-2 remeasure |
+
+---
+
+## Strict dispatch order (per lane)
+
+### Go (gentle-lynx-68, #4145)
+
+```text
+1. go_target_atom_realization_* rows (shared TargetAtomRealization)
+2. go_target_type_expr_projection_* rows (shared TargetTypeExpressionProjection)
+3. leaf_model R1/R2a/R2b/R3-external claims (TargetCompileVerdict + TargetRuntimeExerciseVerdict)
+4. CiUpsertStep rows (leaf-model CI worksheet)
+5. L1 compiler slice (nat_semiring rung2 recommended)
+```
+
+### TypeScript alpha (fierce-fox-719, #4147 on main — §8 ratification follow-up)
+
+```text
+1. ts_type_expression_projection() — BEFORE atom
+2. ts_target_atom_realization_* 
+3. ts algebra inhabitance widening
+4. leaf_model R2a/R2b/R3-external (shared verdict carriers — NOT TargetTypeScript*Verdict)
+5. grammar-inverse TestClaims (alpha, optional parallel)
+```
+
+### Python (witty-ram-95)
+
+```text
+L0: CLOSED (#4117)
+L1/L2: static analysis carrier (worksheet A) → runtime fixture execution (B) → cross-target parity (C)
+```
+
+### Rust (vivid-lynx-81)
+
+```text
+SG-COLLECTION-PROJECTION worksheet: REQUIRED before collection impl (FreeMonoid<T> → Vec<Rc<T>>)
+SG-8 impl: authorized (#4143)
+Other residuals: see #4148 routing worksheets (not impl without §8)
+```
+
+---
+
+## Worksheet §8 queue (Arbiter)
+
+| Priority | Item | PR / owner | Arbiter state |
+| -------- | ---- | ---------- | ------------- |
+| 1 | SG-COLLECTION-PROJECTION (new) | vivid-lynx-81 (pending author) | **BLOCKED** — awaiting worksheet |
+| 2 | Go L0/L1 bundle (5 worksheets) | #4149 (supersedes draft #4145 content + §8) | **ready-for-review** — all §8 CLOSED |
+| 3 | TS strict-order (5 worksheets) | #4147 merged; §8 follow-up PR TBD | **active** — shared verdict adjudication pending |
+| 4 | Python L1/L2 | witty-ram-95 | **active** — review queue |
+
+---
+
+## Amendment log
+
+| Date | Change | Arbiter |
+| ---- | ------ | ------- |
+| 2026-06-01 | Initial map; P5 + SG-8 APPROVED; Go/TS verdict carrier consolidation | proud-fox-405 |
+| 2026-06-01 | Go five worksheets §8 APPROVED on #4149; map Go rows → APPROVED | proud-fox-405 |
diff --git a/docs/planning/v4-go-l1-compiler-slice-compile-worksheet-2026-06-01.md b/docs/planning/v4-go-l1-compiler-slice-compile-worksheet-2026-06-01.md
@@ -0,0 +1,77 @@
+# v4 Go L1 Compiler-Slice Compile Worksheet — emit subset `go build` receipt
+
+> **Status:** **WORKSHEET APPROVED — READY-FOR-WORKER-DISPATCH** — Modeling DFS Arbiter §8 sign-off 2026-06-01 (`proud-fox-405`). **Slice id:** `go_l1_nat_semiring_rung2` (post-L0 PROVEN).
+> **Date:** 2026-06-01
+> **Dispatch anchor:** `docs/planning/v4-predicate-dependency-graph-2026-06-01-eod.md` §11.8.1 rung **L1**; Go row target "L0 complete + **L1 fixture-scale**".
+> **Prerequisites:** #4076 merged; L0 leaf-model claims PROVEN (sibling leaf-model worksheet); Go SG-1/SG-2 rows landed for atoms/generics touched by slice.
+
+---
+
+## Mechanical dispatch rule
+
+> **L1 is NOT full v4 compiler self-compile (L4).** Acceptance is: a **named, bounded compiler subset** emits to Go and **`go build` succeeds** on that artifact with a structured receipt.
+
+---
+
+## §10.0-adapted worksheet
+
+```text
+Migration class:        GO-L1-COMPILER-SLICE-COMPILE
+Representative failure:  #4076 fixed module layout for weather/nat_semiring but no receipt that a
+                         declared v4 compiler-subset emits and typechecks as Go under go build.
+Immediate local patch:   Manual go build of hand-patched emitted tree in PR description.
+Why forbidden:           Non-reproducible; no FileSet/affected gate; not L1 rung receipt.
+DFS path:
+  fixture authority:
+    - phase1/nat_semiring rungs (docs/planning/v4-ladder-rung-specs-2026-05-30.md R2-go-compile)
+    - OR new minimal go_compiler_slice fixture (Arbiter picks one — prefer existing nat_semiring
+      if post-#4076 green, else smallest add.dag-class slice)
+  emit path:
+    - v2→v4 Go emit for bounded ModuleGraph (not full 332-source closure on every PR)
+  verifier:
+    - go build (R2-go-compile bar); go test only if slice includes tests
+Deepest unsound boundary:
+  No structured L1 receipt tying emitted compiler-subset → go build PASS/FAIL headline.
+Systemic fix:
+  (1) Name compiler_slice_go_v1 ModuleGraph / FileSet in worksheet-approved fixture list.
+  (2) CiUpsertStep or ladder rung row: emit_go_compiler_slice → go_build_verdict.
+  (3) Receipt JSON: { slice_id, go_module_root, verdict, diagnostic_snippet? }.
+Non-goals:
+  - L2 cross-target eval equivalence (separate rung / #4081 Wc analog).
+  - L3 self-output fixed point.
+  - Replacing full v4-bootstrap-viability.sh.
+Falsification probe:
+  Deliberately break go.dag surface spelling for int in model; L1 step must FAIL before emit merge.
+Metric allowed only as secondary:
+  Full weather package go test count — not L1 acceptance.
+```
+
+---
+
+## §4 Proposed L1 slice candidates (Arbiter picks one)
+
+| Slice id | Fixture | Rationale | Blocked if |
+|---|---|---|---|
+| `go_l1_nat_semiring_rung2` | `phase1/nat_semiring` Go emit path | Post-#4076 layout fix; ladder R2-go-compile already defined | L0 go.dag claims not PROVEN |
+| `go_l1_mvp1_add` | `mvp1_go_add_translate` manual claim neighborhood | Smallest translate surface in tree | Missing atom/type_expr rows |
+| `go_l1_weather_pkg` | weather Go module | Real integration weight | Too large for first L1 — fallback only |
+
+**Recommendation (Go RCA):** start `go_l1_nat_semiring_rung2` after L0 R1 PROVEN — reuses ladder vocabulary.
+
+---
+
+## §8 Modeling DFS Arbiter approval checklist — CLOSED 2026-06-01
+
+- [x] Named slice id: **`go_l1_nat_semiring_rung2`** (`phase1/nat_semiring` Go emit path; ladder R2-go-compile)
+- [x] Distinct from L0 leaf-model claims (structured L1 receipt JSON)
+- [x] Does not claim L2/L3/L4
+- [x] Gated on L0 leaf-model claims PROVEN before dispatch
+- [x] **READY-FOR-WORKER-DISPATCH** (`proud-fox-405`)
+
+---
+
+## Related artifacts
+
+- `docs/planning/v4-ladder-rung-specs-2026-05-30.md` — `R2-go-compile`
+- PR **#4076** — module layout prerequisite
+- `docs/planning/v4-go-leaf-model-verification-worksheet-2026-06-01.md` — L0 gate
diff --git a/docs/planning/v4-go-leaf-model-ci-runner-worksheet-2026-06-01.md b/docs/planning/v4-go-leaf-model-ci-runner-worksheet-2026-06-01.md
@@ -0,0 +1,79 @@
+# v4 Go Leaf-Model CI Runner Worksheet — `go build` / `go test` host → `CiUpsertStep`
+
+> **Status:** **WORKSHEET APPROVED — READY-FOR-WORKER-DISPATCH** — Modeling DFS Arbiter §8 sign-off 2026-06-01 (`proud-fox-405`); CI Manager coordinates row registration.
+> **Date:** 2026-06-01
+> **Dispatch anchor:** `docs/planning/v4-predicate-dependency-graph-2026-06-01-eod.md` §11.6 category C/D; #4091 ratified elastic CI / `CiUpsertStep` pattern (#4115 positive-Y replacement).
+> **Sibling:** `docs/planning/v4-go-leaf-model-verification-worksheet-2026-06-01.md`
+
+---
+
+## Mechanical dispatch rule
+
+> **No new `scripts/v4-leaf-model-go-*.sh` may be added to ci.yml without a modeled `CiUpsertStep` row in the same PR** (standing `project_no_new_shell` + #4115 pattern).
+
+Interim shell bridges are allowed **only** with dissolve-on-arrival headers matching `scripts/v4-leaf-model-python-r1-verify.sh` until T-22 `run_target_verification` owns `go` invocation.
+
+---
+
+## §10.0-adapted worksheet
+
+```text
+Migration class:        GO-LEAFMODEL-CI-RUNNER (go build / go test boundary steps)
+Representative failure:  Leaf-model Go verification exists only as ad hoc shell; CI category C
+                         lists Python/Rust boundaries but no Go rows (dep graph §11.6).
+Immediate local patch:   Wire go verify scripts into ci.yml without CiUpsertStep backing.
+Why forbidden:           project_no_new_shell; no receipt parity; cannot skip-verify on unchanged claims.
+DFS path:
+  std/workflow authority:
+    - src/v4/workflow/ci.dag — CiUpsertStep rows (47 on main post-#4115)
+    - ci_pipeline_step_ids_shadow bijection for receipt parity
+  host transport (interim):
+    - scripts/v4-leaf-model-go-{r1,r2a,r2b,r3-external}-verify.sh
+    - dissolves when T-22 modeled go toolchain transport lands
+Deepest unsound boundary:
+  Go leaf-model claims have no CI Upsert row; Go L0 cannot gate PRs touching go.dag.
+Systemic fix:
+  For each Go leaf-model claim_id, add CiUpsertStep<VerificationReport> row:
+    inputs: FileSet(go.dag + claim .dag + lens fixture deps)
+    verify: cached_verification_holds(claim)
+    create: run_target_verification(go_fixture, go_toolchain{build, test?})
+    resolve: latest_verification_report(go.dag, claim_phase)
+  Map YAML category-C "leaf-model boundary" steps to these rows (gunbc#846 bypass retirement).
+Non-goals:
+  - Full v4-bootstrap-viability replacement (Class A exception per dep graph §11.6).
+  - Four-compile redundancy collapse (CI Manager scope).
+Falsification probe:
+  Touch only a comment in go_r1.dag; affected set runs exactly Go R1 step, not full ci_v4 compile farm.
+Metric allowed only as secondary:
+  ci_v4 wall time — not acceptance.
+```
+
+---
+
+## §4 Modeled step inventory (target)
+
+| Step id (sketch) | Toolchain | Claim / scope | Interim shell |
+|---|---|---|---|
+| `verify_go_dag_r1` | `go build` | `leaf_model_claim_go_r1_int_surface_spelling` | `v4-leaf-model-go-r1-verify.sh` |
+| `verify_go_dag_r2a` | `go build` | `leaf_model_claim_go_r2a_int_algebra_operations` | `v4-leaf-model-go-r2a-verify.sh` |
+| `verify_go_dag_r2b` | `go run` or `go test` | `leaf_model_claim_go_r2b_int_silent_overflow_truncates` | `v4-leaf-model-go-r2b-verify.sh` |
+| `verify_go_dag_r3_external` | `go build` | `leaf_model_claim_go_r3_external_symbol_projection` | `v4-leaf-model-go-r3-external-verify.sh` |
+
+**FileSet trigger:** `src/v4/extdeps/languages/go.dag`, `src/v4/test/claim/language_model/go_*.dag`, `src/v4/lens/leaf_model_verification.dag` (go_* sections).
+
+---
+
+## §8 Modeling DFS Arbiter approval checklist — CLOSED 2026-06-01
+
+- [x] Claim IDs match leaf-model verification worksheet
+- [x] Positive-Y `CiUpsertStep` only — no `ci.yml` shell without modeled row (operator hold)
+- [x] CI Manager: `ci_pipeline_step_ids_shadow` registration in impl PR
+- [x] **READY-FOR-WORKER-DISPATCH** (`proud-fox-405`)
+
+---
+
+## Related artifacts
+
+- `docs/planning/v4-w2.3-ci-upsert-step-migration-worksheet-2026-05-30.md`
+- `docs/planning/v4-p5-structural-bridge-replacement-worksheet-2026-05-30.md` — #4115 pattern
+- `docs/planning/elastic-ci-redesign-exploration-2026-05-31.md` — #4091 substrate