briansrls · May 10, 2026 · May 10, 2026 · May 10, 2026 · May 10, 2026 · May 10, 2026
diff --git a/ROADMAP.md b/ROADMAP.md
@@ -644,7 +644,6 @@ Eight novel-finding rows surfaced by the 2026-05-07/2026-05-08 paired Explorator
 - **Predicate registry `KNOWN_PREDICATES` is central Rust-side semantic authority**: `src/v3/compiler/src/lower.rs` `KNOWN_PREDICATES` (added in PR #abf5f24d) is a Rust constant with string carrier names (`"Int"`, `"Nat"`, `"String"`, etc.). Better than the prior file-path shim it replaced, but still not the final substrate authority — adding a predicate means editing Rust, not one `.dag` file. Dissolution: dissolve to `.dag` predicate declarations OR reflected predicate bodies; consume from substrate, not Rust constant. Owner: substrate-reflection / predicate-substrate lane.
 - **Domain refinements regressed pending `Q-Regex-Primitive`**: `dsl/std/types.dag` removed `pattern`/`format`/`content` refinements from `CommitSha`, `Sha256`, `Email`, `Url`, `SemVer`, `Timestamp`, `ServiceAccountEmail`, `TextFilePath`, `BinaryFilePath`, `MimeType` — fail-closed posture relative to unsupported predicates is correct, but consumers now have weaker structural protection. Dissolution: ground regex/content predicates per `Q-Regex-Primitive` (don't let it drift behind lower-priority docs/brief waves) + restore refinements OR explicitly accept the relaxed types as terminal. Owner: substrate-capability lane (regex/content typing).
 - **`SymbolicCostExprEquals` typed shape but `NotYetImplemented` in runner**: `src/v3/std/verification.dag` defines the `SymbolicCostExprEquals` `TestClaim` shape, but the test_runner currently reports `NotYetImplemented`. "Typed carrier landed" ≠ "verification landed". Dissolution: implement runner evaluation (consume `SymbolicCost` algebra) OR fail-closed reject; don't credit R3 closure gate #40 (`symbolic_cost_expr_equals_executable`) on shape-only. Owner: R3 Verification Mgr (gate #40 owner).
-- **R3 — gate #37 emit-time slice (beyond ε integration receipt)**: `docs/r3-program-plan.md` gate **#37** records **INTEGRATION_RECEIPT (partial — ε-slice)** backed by `src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs`; the **emit-time** / `LanguageSpec`-indexed cost-lens consumer for realization-row `cost` remains **deferred** on **T-CostLens-Composition** to **R3 gates #40 / #70** (same program plan). Dissolution: land the production consumer path per those gates; retire reliance on test-only structural walks for gate credit. Owner: R3 Verification Mgr.
 - **`EmitModelVariants` centralized Rust mirror needs generation or ratchet**: `src/v3/compiler/src/dag.rs` `EmitModelVariants` is a manually-enumerated cache of variant labels, better than scattered local `named_variant_id` walkers but still hand-maintained. Dissolution: either generate the cache from `src/v3/std/emit_model.dag` at bootstrap-regen time, OR add an exhaustiveness ratchet test asserting every declared `emit_model.dag` variant is either cached or intentionally unsupported. Owner: emit-model substrate consolidation lane.
 - **L6 projection errors swallowed via `unwrap_or_default()`**: `src/v3/grounding_cross_target_meta/src/coverage.rs` introduces `ProjectionCoverageError` typed errors, but the public `language_spec_emission_cells_covered` path returns `unwrap_or_default()`. Fail-closed in the sense of "malformed projections give no coverage" but loses the typed reason unless tests call the checked path. P3 weakening (typed diagnostics shouldn't be defaulted away at public boundary). Dissolution: surface `ProjectionCoverageError` to the L6 gate that reports failure; remove `unwrap_or_default()` on public API. Owner: T-Ground-CrossTarget-Meta lane (R2 territory).
 - **`src/v3/std/cross_target_coverage.dag` doc/code drift**: file labels populated table section as `emission_path_projections (empty data state)` even though it now contains 41 projection rows; `src/v3/compiler/tests/integration/sg0_census_test.rs` comments still describe L6 carrier slice as `emission_path_projections == []`. P1 Modeling Faithfulness violation: documentation must describe live state. Dissolution: cleanup pass updating both file comments + sg0_census_test.rs comments to reflect post-population state. Owner: small-scope cleanup; could fold into next Substrate Mgr / Grounding Mgr canvas absorption.

diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md
@@ -260,7 +260,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 34 | `bridge_include_str_side_channels_retired` | state-check | T-Bridge-Retirement | DECLARED | substrate query surface |
 | 35 | `bridge_exact_string_patching_residual_retired` | state-check | T-Bridge-Retirement | **PASSING** | PB lower-helper slice retired in `bridge_ledger.dag`; residual Row-4 classes → `bridge_exact_string_semantic_patching_residual` (Open) |
 | 36 | `bridge_retirement_ledger_zero` | ledger-count | T-Bridge-Retirement | DECLARED | unified ledger reports 0 |
-| 37 | `cost_lens_reads_target_realization` | structural-fold | T-CostLens-Composition | **INTEGRATION_RECEIPT (partial — ε-slice)** — PR #2181 ε path: `lens_cost_target_realization_test.rs` proves (i) **TypeRealization** slice: Rust-side `symbolic_cost_of` on a tiny program × `rust_int` row `cost` composed via `Semiring<SymbolicCost>` `sequential`; (ii) **CallableRealization** slice: bootstrap `rust_is_empty_callable` row `cost` readable as a lowered structural field (same row-shape discipline as (i), **without** a second `sequential` composition pin in that subtest). **Not** full emit-time / `LanguageSpec`-indexed cost-lens consumer (that closure remains with gates **#40** / **#70** / follow-on slices per program plan). Historical gate id; lens output stays abstract `SymbolicCost`. | ε-slice receipt; emit-time fold follow-on |
+| 37 | `cost_lens_reads_target_realization` | structural-fold | T-CostLens-Composition | **INTEGRATION_RECEIPT (partial — ε-slice)** — `src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs` pins `cost_lens_composes_symbolic_cost_with_rust_type_realization_row` (Rust-side `symbolic_cost_of` × `Semiring<SymbolicCost>::sequential` × bootstrap `rust_int.TypeRealization.cost`) and `cost_lens_reads_cost_field_on_rust_callable_realization_row` (`rust_is_empty_callable.CallableRealization.cost`). ε ratification (Q-Cost-Composition-Layering / PR #2181): lens output stays abstract `SymbolicCost`; per-primitive realization rows remain emit-time facts — full executable parity for gate **#40** / demonstration **#70** stays tracked separately. | Rust-side composition consumer + cited integration tests |
 | 38 | `coercion_cost_equals_complexity_by_construction` | structural-fold | T-CostLens-Composition | **SATISFIED-BY-CONSTRUCTION** (α-narrow PR #2171; `Semiring<SymbolicCost>` `sequential`/`iterate` at `src/v3/std/algebra.dag:181-188` is sole composition authority — no parallel "complexity-vs-cost" reconciliation surface exists) | thesis unification holds structurally |
 | 39 | `no_coercion_cost_dimension` | substrate-shape | T-CostLens-Composition | **SATISFIED-BY-CONSTRUCTION** (α-narrow PR #2171; `SymbolicCost` 7-variant at `src/v3/std/algebra.dag:181` is the sole cost dimension; no parallel `CoercionCost` carrier exists at HEAD per grep) | no separate cost dimension |
 | 40 | `symbolic_cost_expr_equals_executable` | SymbolicCost-typed | T-CostLens-Composition | DECLARED — ε path RATIFIED 2026-05-07 (Q-Cost-Composition-Layering canvas); closes via Verification Mgr (#2075) ratchet authoring on Rust-side composition consumer + executable predicate per ε path | runtime prereq: cost lens consumer per ε |
@@ -425,7 +425,7 @@ Each retires per its natural-owner program prerequisites. Verification Mgr's `br
 | T-Omni-Shape-B | RED | (post-R2-Evaluator + Shape A targets) | dependencies | (TBD) |
 | T-Anthropic-Wire | YELLOW | 3 coproduct worker briefs dispatched on PR #1782 wait-window + 2 OPEN closure tags at HEAD (`dsl/extdeps/llm/anthropic.dag` `:189` + `:68`) | three coproduct slices land + variant-aware projection carrier authored | post-#1782 merge + 3 follow-up paydown PRs |
 | T-Bridge-Retirement | YELLOW | per-bridge dispatches | 5 sub-bridges retire | post-T-FixedPoint |
-| T-CostLens-Composition | YELLOW | α-narrow ratified at gunb-ai/gunbc#828 #issuecomment-4400772335 — gates **#38** + **#39** structurally satisfied at HEAD by construction (`SymbolicCost` sole cost dimension; `Semiring<SymbolicCost>` sole composition authority); receipts landed via PR #2171. **ε path RATIFIED 2026-05-07** (Q-Cost-Composition-Layering canvas at PR #2181, canonical-not-transitional) — **#37** has **INTEGRATION_RECEIPT (partial ε-slice)** (Rust composition proof in `lens_cost_target_realization_test.rs`; not emit-time `LanguageSpec` consumer); gates **#40** + **#70** remain follow-on slice. **Q-Lens-Target-Context β-extended path DEFERRED** to N=2 trigger event (when second lens surfaces target-context need; emission_provenance most likely candidate per cross-cutting analysis); not active R3 ratification gate. | R2-Evaluator + R2-T-Substrate-Lens-Primitive + T-CostLens follow-on slice (Rust-side composition per ε) | partial close per α + #37 ε-slice receipt; #40/#70 post-ε-slice |
+| T-CostLens-Composition | YELLOW | α-narrow ratified at gunb-ai/gunbc#828 #issuecomment-4400772335 — gates **#38** + **#39** structurally satisfied at HEAD by construction (`SymbolicCost` sole cost dimension; `Semiring<SymbolicCost>` sole composition authority); receipts landed via PR #2171. **ε path RATIFIED 2026-05-07** (Q-Cost-Composition-Layering canvas at PR #2181, canonical-not-transitional) — **gate #37** documents the **partial** Rust-side composition consumer (`symbolic_cost` × `sequential` × bootstrap realization rows; see §1.8 row #37). **Gates #40** and **#70** remain **DECLARED** in §1.8 (Verification Mgr / follow-on slice + demonstration); full executable parity for #40 and closure for #70 are **not** claimed by #37’s ε-slice and stay **tracked separately** per row #37. **Q-Lens-Target-Context β-extended path DEFERRED** to N=2 trigger event (when second lens surfaces target-context need; emission_provenance most likely candidate per cross-cutting analysis); not active R3 ratification gate. | R2-Evaluator + R2-T-Substrate-Lens-Primitive + T-CostLens follow-on slice (Rust-side composition per ε) + Verification Mgr ratchet for #40 / demo closure for #70 | α close at HEAD; #37 partial ε-slice receipt only; #40 and #70 still open per §1.8 until their rows promote |
 | T-V2-Retirement | RED | `r3-tv2-*` briefs | T-FixedPoint + T-LensProducer | longest-path |
 | T-Free-Consequences-Demonstration | YELLOW | `r3-v-free-consequences-worker` | R2-Evaluator + T-CostLens-Composition | post-deps |
 | T-E-P-Producer-Broadening | YELLOW | (TBD from Substrate canvas) | (foundational; in flight) | weeks |

diff --git a/dsl/extdeps/cron.dag b/dsl/extdeps/cron.dag
@@ -1,98 +1,14 @@
-// extdeps/cron.dag -- POSIX crontab scheduler
+// extdeps/cron.dag — crontab shell transport (`cron.Tab` operations).
 //
-// Spec: POSIX.1-2017 crontab(1)
-// https://pubs.opengroup.org/onlinepubs/9699919799/utilities/crontab.html
+// Typed schedule carriers + render helpers live in `cron_schedule_model.dag`
+// (`module extdeps.cron.schedule_model`) so v3 bootstrap can depend on schedule
+// shapes without parsing `service` blocks.
 //
-// Models the local user crontab as a set of entries keyed by a tag
-// comment. Upsert and Remove are idempotent by construction:
-// Upsert matches on tag, replaces if present, appends if absent.
-// Remove matches on tag, no-ops if absent.
-//
-// Consumers:
-//   gunbc/tools/review.dag -- review workflow self-registers its schedule
+// External authority: POSIX.1-2017 user crontab interface (crontab utility / on-disk entries)
+// — schedule-shaped data cites the same POSIX volume as the carrier module header.
 
 module extdeps.cron
 
-import std.integer { NonNegativeInt, PositiveInt }
-
-// -- Cron entry model -------------------------------------------------
-// Typed cron expression. Each of the 5 standard POSIX fields is a
-// `CronField` rather than an opaque string. The sum type collapses
-// the *string-vs-typed* parse fork into a single authority: there is
-// one path from fixture to wire-format, not two (DSL parse + runtime
-// re-parse). Field payloads are refined to `NonNegativeInt` /
-// `PositiveInt` (no negative cron values; non-zero step interval),
-// but per-field upper bounds (minute 0..59, hour 0..23, day_of_month
-// 1..31, etc.) and `Listed` non-empty refinement remain unenforced --
-// bounded refinements at that level are a separate substrate-shape
-// question warranting ratification.
-//
-// Wire format is recovered via `render_cron_field` / `render_cron_schedule`
-// for transports that take a string-shaped schedule (e.g., crontab(1)).
-//
-// Field-count is exactly 5 (POSIX.1-2017). Expansion to 6 (seconds) or
-// 7 (year) is a substrate-shape question warranting ratification.
-
-// Coproduct dissolution classification (modeling-discipline.md Practice 4):
-// 🟢 TERMINAL. The variant set covers the wildcard / exact / comma-list /
-// range grammar from POSIX.1-2017 crontab(1) plus the slash-step form
-// (e.g. `*/10`) from the Vixie-cron extension that all mainstream cron
-// implementations (vixie, cronie, busybox, systemd OnCalendar, GitHub
-// Actions schedule triggers) accept and that the existing consumers in
-// this codebase rely on (`review.dag`, `review_codex.dag` use `*/N`).
-// The set is bounded by these merged grammars, not a scaffold for a
-// future model. Field-payload integer types are refined to
-// NonNegativeInt / PositiveInt: cron field values are never negative
-// in POSIX, and step interval is strictly positive (zero-step is
-// undefined). Per-field POSIX bounds (minute 0..59, hour 0..23, etc.)
-// remain unenforced -- bounded refinements are a separate substrate
-// shape question and would compose at this layer.
-type CronField
-  = Wildcard                                                       // *
-  | Exact { value: NonNegativeInt }                                // N
-  | Listed { values: List<NonNegativeInt> }                        // a,b,c (empty-list representable; renders as ""; non-empty refinement deferred with per-field bounds)
-  | Ranged { start: NonNegativeInt, end: NonNegativeInt }          // a-b
-  | Step { start: NonNegativeInt, step: PositiveInt }              // a/N  (start: 0 renders as "*/N")
-
-type CronSchedule {
-  minute: CronField
-  hour: CronField
-  day_of_month: CronField
-  month: CronField
-  day_of_week: CronField
-}
-
-type CronEntry {
-  tag: String
-  schedule: CronSchedule
-  command: String
-}
-
-// Wire-format render. Consumers calling `cron.Tab.Upsert` pass
-// `render_cron_schedule(typed_schedule)` to satisfy the String-shaped
-// transport input.
-
-fn render_cron_field(f: CronField) -> String {
-  match f {
-    Wildcard => "*"
-    Exact { value } => "{value}"
-    Listed { values } => values |> map(v => "{v}") |> join(separator: ",")
-    Ranged { start, end } => "{start}-{end}"
-    Step { start, step } => if start == 0 { "*/{step}" } else { "{start}/{step}" }
-  }
-}
-
-fn render_cron_schedule(s: CronSchedule) -> String {
-  let mn = render_cron_field(s.minute)
-  let hr = render_cron_field(s.hour)
-  let dm = render_cron_field(s.day_of_month)
-  let mo = render_cron_field(s.month)
-  let dw = render_cron_field(s.day_of_week)
-  "{mn} {hr} {dm} {mo} {dw}"
-}
-
-// -- Service: shell transport -----------------------------------------
-
 service cron.Tab {
   operation List {
     input {}