briansrls · May 2, 2026 · May 1, 2026 · May 1, 2026 · May 1, 2026 · May 1, 2026
diff --git a/docs/design-complexity-lens-behavioral-completeness.md b/docs/design-complexity-lens-behavioral-completeness.md
diff --git a/docs/design-cost-lens-sizevar-dimension-wiring.md b/docs/design-cost-lens-sizevar-dimension-wiring.md
diff --git a/docs/design-effect-enumeration-resource-threading.md b/docs/design-effect-enumeration-resource-threading.md
@@ -14,7 +14,7 @@
 
 > Audit verdict is path (ii): live primitives still require ambient resource/transport metadata rather than returned-modified-resource signatures (`dsl/std/resources.dag`, `dsl/std/primitives.dag`, `dsl/extdeps/shell.dag`, `dsl/extdeps/github/auth.dag`). Full `OperationEffect` retirement, resource-threading migration, and caller-side effect-set pinning are follow-up work.
 
-That sentence names four substrate-level moves bundled under one closure gate (`effect_enumeration_lens_behaviorally_complete`). This doc specifies them as one atomic migration. Per [`feedback_closed_system_effects`](../README.md#) and [`../INVARIANTS.md`](../INVARIANTS.md) §P1: effects are not a parallel taxonomy alongside the substrate — they derive structurally from typed primitive composition. Today's substrate violates that by carrying effect intent in three places (resource block, transport block, `OperationEffect` record); this design collapses all three onto one structural authority — the callable's arrow signature.
+That sentence names four substrate-level moves bundled under one closure gate (`effect_enumeration_lens_behaviorally_complete`). This doc specifies them as one atomic migration. Per [`feedback_closed_system_effects`](../README.md#) and [`../INVARIANTS.md`](../INVARIANTS.md) §P1: effects are not a parallel taxonomy alongside the substrate — they derive structurally from typed primitive composition. Today's substrate violates that by carrying effect intent in three places (resource block, transport block, `OperationEffect` record); this design collapses all three onto **two orthogonal structural authorities** (per §2.4): (a) the callable's arrow signature carries the **effect set** (which resource types are involved); (b) the callable's algebra inhabitance (`inhabits IdempotentRead<R>` / `inhabits Mutating<R>`) carries the **effect kind** (read/write/append). Neither is convention-level; both are structural. The signature alone cannot distinguish read from write since `R in / R out` and `R in / R' out` have the same typed signature.
 
 ## §1. Ambient-metadata audit (current state)
 
@@ -370,7 +370,7 @@ In one PR:
 
 Three structural reasons make this PR-shippable rather than requiring a multi-stage migration:
 
-- **The lens body does not change.** `src/v3/lenses/effect_enumeration.dag::callable_arrow_effect` already implements §2.4's rule. The migration is upstream of the lens; once the substrate threading lands, the lens fold becomes COMPLETE on the same fold body.
+- **The lens body changes only in its kind-classification dispatch.** `src/v3/lenses/effect_enumeration.dag::callable_arrow_effect` today derives kind from signature/body shape — that path retires. The new lens body reads the **effect set** directly from the callable's arrow signature (the existing substrate query — resource types in input ∩ output; structurally derivable per §2.4(a) without any lens-application-surface artifact) and dispatches on `callable_inhabits(callable, idempotent_read_for(resource))` / `callable_inhabits(callable, mutating_for(resource))` for the **kind classification** (per §2.4(b)). Both queries are within T-Lens-Behavioral-Parity slice 4 scope; **neither depends on `LensEnforcement` from T-Lens-Application-Surface** (the cascade flows the other direction — lens-behavioral-parity COMPLETE → lens-application-surface). The fold structure (per-callable walk; aggregation into the report carrier) is unchanged; only the per-callable kind classifier changes from signature-shape inference to inhabitance lookup. **This change is in scope and required** — without it, the new inhabitance facts §2.4 declares would not be consumed (facts-flow-forward / P2 violation per cursor BLOCKING at sha 96899484 line 17).
 - **`Operation` already exists.** `src/v3/std/services.dag:122` declares the carrier with `callable: CallableRef + inputs: Map + endpoint: RestEndpointBinding` — exactly what §3.2 needs. No new substrate type. The PR-β..ω lineage in `services.dag:9-14` is the dispatch frame for the per-extdep population work.
 - **`Arrow.body` E-9 binding is landed (DB-14).** The transport block migration target is already a live substrate facility per [`../INVARIANTS.md`](../INVARIANTS.md) §E-9 and DB-14. Moving `transport shell { argv: [...] }` to per-target binding is mechanical, not novel substrate work.
 
@@ -439,9 +439,9 @@ This preserves the existing `EffectShape = IsIdempotent(IdempotentShape) | IsBre
 
 **Question:** `dsl/extdeps/shell.dag` operations carry a `readonly` keyword on operations. Does that survive migration?
 
-**Resolved:** deleted. Per [`feedback_closed_system_effects`](../README.md#): *"effects are not annotations."* `readonly` is exactly the annotation pattern P1 names. After migration, `readonly` is structurally derivable: an operation is read-shaped iff every threaded resource appears unchanged in input and output. The keyword's only role today is to short-circuit the algebra; once the algebra reads the signature directly, the keyword is a redundant annotation that can drift from the structural fact (the [`feedback_state_space_vs_behavioral_invariants`](../README.md#) failure mode: a behavioral invariant maintained by convention, not by the type).
+**Resolved:** deleted. Per [`feedback_closed_system_effects`](../README.md#): *"effects are not annotations."* `readonly` is exactly the annotation pattern P1 names. After migration, **read kind is declared via algebra inhabitance** (`inhabits IdempotentRead<R>` per §2.4 + §8.1) — a structural fact on the callable declaration. The `readonly` keyword duplicates that inhabitance: same fact, two carriers. Per P2 single-authority and `feedback_no_annotations`, the annotation goes; the inhabitance stays. The keyword's only role today is short-circuiting the algebra ahead of the (heuristic) `derive_op_effect`; once the algebra reads the declared `inhabits IdempotentRead<R>` directly, the keyword is redundant *and* structurally drift-prone (`feedback_state_space_vs_behavioral_invariants`: a behavioral invariant maintained by convention rather than by the type — the keyword could disagree with the inhabitance).
 
-**Implementation note:** existing `is_idempotent_effect` / `operation_is_breaking` continue to work — they read the partition off the derived `EffectShape`, not off a keyword.
+**Implementation note:** existing `is_idempotent_effect` / `operation_is_breaking` continue to work — they read the partition off the `EffectShape` derived from algebra inhabitance (`IdempotentRead<R>` → `IsIdempotent(ReadShape)`), not off a keyword. The `readonly` deletion is mechanical: every operation currently using `readonly` already has a corresponding `inhabits IdempotentRead<R>` declared at the migration site (one-to-one mapping during the atomic migration PR per §6).
 
 ### §8.5 `OperationEffect.evidence: IdempotencyEvidence` — does it follow `OperationEffect` to deletion? — RESOLVED: yes, derived projection
 
@@ -476,7 +476,7 @@ This document does NOT modify:
 - The `CompositionVerdict` 2-variant shape (`ComposedEffect` reshape R3 lock; per §4.4).
 - The `EffectShape` partition (`IsIdempotent | IsBreaking`; per §4.3).
 - The `BoundedLattice<EffectShape>` algebra (per `src/v3/std/effects.dag` invariants).
-- The lens fold body (`callable_arrow_effect` already implements the §2.4 rule; per §6.2 first reason).
+- The lens fold structure (per-callable walk; report aggregation). The per-callable kind classifier IS modified — it changes from signature-shape inference to inhabitance lookup (per §6.2 first reason; required for facts-flow-forward of the new inhabitance authority).
 
 ## §10. Implementation order (sketch)
 
@@ -486,12 +486,13 @@ Within T-Lens-Behavioral-Parity slice 4 (per [`docs/r3-structure.md`](r3-structu
 2. **`uses` clause migration** (Substrate Manager). Migrate 20 `uses x: Resource` call-sites to threaded inputs/outputs per §2.3. Same PR as step 1 (atomic per §6).
 3. **Transport-block migration to E-9 binding** (Grounding Manager). Migrate 27 services × 67 operations across `dsl/extdeps/*.dag` from `transport <kind> { ... }` blocks to `Arrow.body` per-target realizations per §8.3. Same PR.
 4. **`OperationEffect` retirement** (Substrate Manager). Delete `OperationEffect` declaration + `derive_op_effect` + Rust mirror; reshape `compose_effects(List<Operation>) → CompositionVerdict`; reshape `WorkflowEffect.LinearEffect.ops: List<Operation>`. Same PR.
-5. **Cementing test** (Verification Manager). Author `effect_enumeration_lens_behaviorally_complete` cementing test under `src/v3/compiler/tests/integration/cementing/` per [`TESTING.md`](../TESTING.md) Band-C discipline. Tests minimal-`Dag` shapes asserting (a) read-shaped operations report `ReadShaped`, (b) write-shaped operations report `WriteShaped`, (c) operations with no resource thread report `NoEffect`, (d) coverage gaps surface explicitly. Same PR.
-6. **Capability-register row update** (Verification Manager). Flip `docs/v3-lens-capability-register.md` row for `effect_enumeration.dag` from `BEHAVIORALLY PARTIAL` to `BEHAVIORALLY COMPLETE`; clear the "What v2 has that v3 drops" cell per the discipline at register §"Discipline" item 2. Same PR.
+5. **Lens kind-classifier rewrite** (Substrate Manager). Rewrite `src/v3/lenses/effect_enumeration.dag::callable_arrow_effect`'s per-callable kind dispatch from signature/body shape inference to algebra-inhabitance lookup (`callable_inhabits(callable, idempotent_read_for(resource))` / `callable_inhabits(callable, mutating_for(resource))`). The fold structure (per-callable walk + report aggregation) is unchanged; only the per-callable kind classifier changes. Required for the new `inhabits IdempotentRead<R>` / `inhabits Mutating<R>` facts to flow forward into lens output. Same PR.
+6. **Cementing test** (Verification Manager). Author `effect_enumeration_lens_behaviorally_complete` cementing test under `src/v3/compiler/tests/integration/cementing/` per [`TESTING.md`](../TESTING.md) Band-C discipline. Tests minimal-`Dag` shapes asserting (a) read-shaped operations report `ReadShaped`, (b) write-shaped operations report `WriteShaped`, (c) operations with no resource thread report `NoEffect`, (d) coverage gaps surface explicitly. Same PR. **Cross-lens cementing format alignment**: this Rust cementing test is the staged form. Dissolution trigger: at T-Tests-As-Data-Completeness step 5 (per [`docs/design-tests-as-data-completeness.md`](design-tests-as-data-completeness.md) §6 step 5 — *cementing dispatch port*), the test ports to a `.dag` `TestClaim`/`QuantifiedTestClaim` declaration. All three behavioral-parity lenses (complexity / cost / effect-enumeration) follow the same staging — Rust cementing today, .dag port at migration step.
+7. **Capability-register row update** (Verification Manager). Flip `docs/v3-lens-capability-register.md` row for `effect_enumeration.dag` from `BEHAVIORALLY PARTIAL` to `BEHAVIORALLY COMPLETE`; clear the "What v2 has that v3 drops" cell per the discipline at register §"Discipline" item 2. Same PR.
 
-Steps 1–6 land as **one PR** per §6 atomic discipline. Internal sequencing within the PR is mechanical — substrate authoring (1) → consumer migration (2, 3) → algebra reshape (4) → tests (5) → docs (6) — but the PR is a single atomic unit per [`../INVARIANTS.md`](../INVARIANTS.md) §P5.
+Steps 1–7 land as **one PR** per §6 atomic discipline. Internal sequencing within the PR is mechanical — substrate authoring (1) → consumer migration (2, 3) → algebra reshape (4) → lens kind-classifier rewrite (5) → tests (6) → docs (7) — but the PR is a single atomic unit per [`../INVARIANTS.md`](../INVARIANTS.md) §P5.
 
-Total estimate (per L-XL sizing in lane row 146): substrate + extdeps consumer migration is the L-XL surface; lens-fold itself is unchanged; cementing test is M; doc is S. End-to-end: 3-5 weeks worker time at standard R3 cadence given coordinated cross-manager dispatch.
+Total estimate (per L-XL sizing in lane row 146): substrate + extdeps consumer migration is the L-XL surface; lens-fold structure is unchanged; per-callable kind classifier rewrite (signature-shape → inhabitance lookup) is S; cementing test is M; doc is S. End-to-end: 3-5 weeks worker time at standard R3 cadence given coordinated cross-manager dispatch.
 
 ---