lens/structural_resolution.dag — registry-entry fill (LensIdV0::StructuralResolution currently Unbound; pattern T-13 mirror — lens-over-substrate per Practice 11 + monomorphism/prelude carve-out; reads InferredTree + dependency-graph projection; produces Witness<StructuralResolutionFact>; substrate-

INVARIANTS.md

@@ -372,7 +372,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX
 | `src/v3/compiler/tests/integration/v4_bin_main_dag_smoke_test.rs` | **T-15** (`src/v4/bin/main.dag` — trampoline **`String`** authority + B1 digest **placeholder** `Node`s; closed-tree invariant #2 / pure-bootstrap zero-floor per `docs/design-pure-bootstrap-zero.md`). **Grounded-indicator authoring on `main.dag` is HOLD** pending hub-relayed canonical spec (operator-direct format under-spec; neat-hawk-87 cascade 2026-05-19). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `main.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust probe. **Interim ratchet:** `v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor` runs `tokenize_for_test` + `parse_for_test` on the pinned `include_str!` source and asserts the trampoline / stub `data` identifiers plus the escaped `include!` spelling remain present in source text (full `compile_to_dag` on `main.dag` alone is deferred: `import v4.std.node` is not linked in the single-file harness). |
 | `src/v3/compiler/tests/integration/v4_compiler_emit_translate_smoke_test.rs` | **TASKS.md** T-10 / Wave-3-B (`src/v4/compiler/06_translate.dag` — `fold_node` translate + `coercion_fold` wrapper, `TargetSelectionPolicy` from target-model bundle; `src/v4/compiler/05_emit.dag` — `serialize_target ∘ translate`, grammar-as-bidir serialize via bundle `emitted`/`source` keys; `src/v4/test/claim/manual/mvp1_rust_add_translate.dag` structural TestClaim anchors). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when translate/emit/MVP-1 surfaces are exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust probe (full `compile_to_dag` over v4 compiler modules deferred until multi-module load). **Interim ratchet:** `v4_find_witness_dag_tokenizes_and_parses` / `v4_find_witness_dag_declares_find_witness_entrypoint` — find_witness primitive parse surface; `v4_translate_dag_tokenizes_and_parses` / `v4_emit_dag_tokenizes_and_parses` / `v4_mvp1_rust_add_claim_tokenizes_and_parses` — tokenize+parse only; `v4_translate_dag_module_path_is_compiler_translate` — module path; `v4_translate_dag_imports_coercion_fold_delegate` — `coercion_fold` import; `v4_translate_dag_imports_fold_node_traversal` — `fold_node` import; `v4_translate_dag_declares_coerce_grounded_node` — `coerce_grounded_node` decl; `v4_translate_dag_declares_translate_node_and_translate` — `translate_node`/`translate` decls; `v4_translate_dag_imports_find_witness_types_not_inline_fn` — `CandidateSet` import without `find_witness` fn; `v4_emit_dag_module_path_is_compiler_emit` — module path; `v4_emit_dag_imports_translate_stage` — `translate` import (`serialize_target ∘ translate`); `v4_emit_dag_declares_emit_entrypoint` — `emit` decl; `v4_emit_dag_does_not_import_find_witness` — emit must not import `find_witness`; `v4_mvp1_rust_add_claim_imports_translate_and_emit` — claim imports translate+emit. **Known substrate blocker (post-T-10 MVP-1):** `target_serialize_source_from_model` still fail-closed (`translate_target_source_not_realized`) — grammar-bidir inverse serialize deferred; Accepted MVP-1 emit end-to-end still awaits live `infer` descent + populated `InferredTree.facts` on real programs (T-9 cardinality propagation), not translate/coercion/find_witness bodies (landed: `find_witness` enumeration + `TargetSelection`, `canonical_grounding_for_node` reads infer-authored witnesses only). |
 | `src/v3/compiler/tests/integration/v4_compiler_compile_public_terminal_smoke_test.rs` | **Wave-5-A / P3 commitment 6** (`src/v4/compiler/00_compile.dag` — `validate_then_compile` public terminal, `Validated<CompileOutput>` carrier, `infer` → required-lens gates on `InferredTree` → `compile_inferred`; `src/v4/compiler/07_target_carriers.dag` — acyclic `TargetModel`/`TargetSource` authority; `src/v4/test/claim/manual/validate_then_compile_public_terminal.dag` manual TestClaim anchors). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `validate_then_compile` / compile-core surfaces are exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust probe (full `compile_to_dag` over v4 compiler modules deferred until multi-module load). **Interim ratchet:** `v4_compile_dag_tokenizes_and_parses` / `v4_compile_dag_module_path_is_compiler_compile` / `v4_compile_dag_declares_public_validate_then_compile` / `v4_compile_dag_declares_ratified_compile_core` / `v4_compile_dag_imports_target_carriers_not_emit_cycle` / `v4_compile_dag_does_not_import_specific_lens_modules` / `v4_emit_dag_does_not_import_compile_module` / `v4_validate_then_compile_claim_tokenizes_and_parses` / `v4_validate_then_compile_claim_imports_public_terminal_helpers` — tokenize+parse + import-row receipts for `compile_lens_gate_rejected_diagnostic`, `TranslateTo`, `validate_then_compile`. |
-| `src/v3/compiler/tests/integration/v4_lens_registry_dag_smoke_test.rs` | **Operator pin** `docs/briefs/r4-lane-a-lens-interface-freeze-pin.md` §3 / **PREFIX T-23 v0** (`src/v4/lens/registry.dag` — **`LensIdV0`** closed sum + **`LensModulePathV0`**). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **P2 / Practice 5:** this smoke is a **parse + inference cleanliness** probe for `src/v4/lens/registry.dag` only — it does **not** claim a **generated** substrate consumer for `LensRegistryEntryV0` (INVARIANTS §P2: declaration without generated consumer = staging; see **PR review** — no maintained manifest). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `registry.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness that mechanically reads registry rows without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_lens_registry_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
+| `src/v3/compiler/tests/integration/v4_lens_registry_dag_smoke_test.rs` | **Operator pin** `docs/briefs/r4-lane-a-lens-interface-freeze-pin.md` §3 / **PREFIX T-23 v0** (`src/v4/lens/registry.dag` — **`LensIdV0`** closed sum + **`LensModulePathV0`**). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **P2 / Practice 5:** this smoke is a **parse cleanliness** probe for `src/v4/lens/registry.dag` only — it does **not** claim a **generated** substrate consumer for `LensRegistryEntryV0` (INVARIANTS §P2: declaration without generated consumer = staging; see **PR review** — no maintained manifest). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `registry.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness that mechanically reads registry rows without this per-file Rust probe (full `compile_to_dag` deferred: post-#3503 P9 rows import `Symbol`/`List` from `v4.std.*`, which M1(2.7) single-file lowering does not link; see harness module comment). **Interim ratchet:** `v4_lens_registry_dag_tokenizes_and_parses` — tokenize+parse + `LensIdV0`/`LensModulePathV0` type-sum presence; `v4_lens_registry_t23_closed_lens_ids_present` — eight-arm closed-set substring receipt; `v4_lens_registry_structural_resolution_bound_to_module` — `StructuralResolution` → `Bound { path: "v4.lens.structural_resolution" }`; `v4_lens_registry_p9_owned_fn_surface_present` — P9 `LensOwnedFnV0` / `lens_owned_fn_registry_v0` substrate rows remain in registry home-of-record. |
 | `src/v3/compiler/tests/integration/v4_lens_testgen_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **`src/v4/TASKS.md` § T-19** (`lens/testgen.dag` — producer of `TestClaim` corpus from substrate; Wave-0 bootstrap / manual claim lookup keyed by **`T19ManualAnchorKey`**; **`Generator.t19_anchor`** reuses the same **`T19ManualAnchorKey`** carrier as **`TestClaim.t19_anchor`** after **`Outcome`** rejects **`T19ManualAnchorAbsent`** on lookup (**Practice 5** single-anchor schema; **LB-P4-3212** ratchet — cite PR #3212 / review thread). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/lens/testgen.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness / merged M2 multi-module lowering without this host `parse_for_test` structural ratchet (isolated `compile_to_dag` does not resolve `import v4.std.*` peers under M1(2.7); see harness module comment). **Interim ratchet:** focused `#[test]` slices in `v4_lens_testgen_dag_smoke_test.rs` (**openai-pro** review **#14812** / **TESTING.md** discipline): `v4_lens_testgen_wave0_modules_tokenize_and_parse`; `v4_lens_testgen_wave0_verification_manual_anchor_key_only`; `v4_lens_testgen_wave0_function_inventory_matches_wave0`; `v4_lens_testgen_wave0_nat_symbol_import_authority`; `v4_lens_testgen_wave0_outcome_return_surfaces`; `v4_lens_testgen_wave0_generator_t19_anchor_field_is_manual_key`; `v4_lens_testgen_wave0_concept_projection_matches_claim_t19_anchor`; `v4_lens_testgen_wave0_generator_carries_claim_kind_and_classification`; `v4_lens_testgen_wave0_bootstrap_threads_claim_anchor_into_generator`; `v4_lens_testgen_nat_law_manual_claims_use_compiles_stub`; `v4_lens_testgen_nat_substrate_carries_algebra_law_subject_symbols`; `v4_lens_testgen_testgen_carries_six_nat_algebra_law_scheduling_arms` — collectively tokenize/parse `src/v4/lens/testgen.dag` + `src/v4/std/verification.dag`, assert Wave-0 function inventory + `Outcome` return surfaces + `Generator.t19_anchor` carrier, substring wiring receipts on bootstrap join, `nat_law_anchors.dag` per-claim `kind: Compiles` on identical stub `input`/`expected` (law-bearing `Node` + `Equals` deferred to T-22; codex #14833), three `AlgebraLawSubject` `Symbol` rows in `src/v4/std/nat.dag`, and six `value: AlgebraLaw {` constructor sites in testgen (file-wide count). Parse-only structural ratchet; `Generator` carries `kind`, `t19_anchor`, `classification`, and `slot` per TASKS T-19. |
 | `src/v3/compiler/tests/integration/v4_std_model_core_dag_smoke_test.rs` | **TASKS.md** **T-33** (`src/v4/std/model_core.dag` — Ratified Q1 `ModelCore` shared substrate: primitive fact bundles, `AlgebraInhabitanceDecl`, `AlgebraLawObligation` over modeled inhabitance + law `Node`, effect/partiality scaffolds per Open Q10). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness; SG-0 census net +1 pairing `(c)` is mechanically prepended via `scripts/ci-merge/sg0-pr-body-append.3474.txt` in CI (`.github/workflows/ci.yml`). **Dissolution:** remove when `model_core.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness / merged M2 multi-module lowering without this host `parse_for_test` structural ratchet (isolated `compile_to_dag` does not resolve `import v4.std.*` peers under M1(2.7); see harness module comment). **Interim ratchet:** `v4_std_model_core_dag_tokenizes_and_parses`; `v4_std_model_core_declares_ratified_q1_carriers`; `v4_std_model_core_bundles_five_facets`; `v4_std_model_core_algebra_law_obligation_structural`; `v4_std_model_core_effect_partiality_ops_use_node_authority`; `v4_std_model_core_wave1_void_constructor_present` — tokenize/parse the pinned `include_str!` source, assert `v4.std.model_core` module path, closed carrier inventory (`ModelCore`, `PrimitiveFactBundle`, `AlgebraInhabitanceDecl`, `AlgebraLawObligation`, `EffectSemanticsDecl`, `PartialitySemanticsDecl`), five-facet `ModelCore` field bundle, `AlgebraLawObligation { inhabitance_witness: Node, law: Node }` (joins canonical `ModelCore.inhabitance` rows by witness; no embedded duplicate decl or Symbol labels), `PrimitiveOperationRef`/`PartialOperationDecl` `operation: Node` (not Symbol), and `wave1_void` scaffold constructor (🟡 `feature:model-core-wave1-void-scaffold`, dissolve-on T-4/T-34 non-empty `ModelCore`). |
 | `src/v3/compiler/tests/integration/file_attachment_substrate_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#62** `substrate_gap_file_ingestion_closed` (T-Workflow-As-Data substrate-gap class; worker brief `docs/briefs/r3-substrate-gate-62-file-attachment-carrier-worker.md`). **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `FileAttachment` field names + cross-module nominal wiring against `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as `timing_lens_substrate_carrier_test.rs` for gate #55). **Interim ratchet:** `file_attachment_shape_locked` + `file_attachment_field_types_locked` + `file_attachment_field_count_is_five` pin the ratified Refined-B-1 five-field subset of `WorkflowObservationAnchor` (`NodeId`, `ContentHash`, `WorkflowProducerId`, `WorkflowRunId`, `Nanoseconds`) exactly as declared in `src/v3/std/timing_lens.dag`; existence proof carrier construction stays in-module as `gate_62_file_attachment_demo_record`. |

docs/briefs/r4-lane-a-lens-interface-freeze-pin.md

@@ -51,9 +51,9 @@ Closed identifiers are **not** modeled as free `String` in substrate: **`LensIdV
 | `idempotency` | `Idempotency` | `v4.lens.idempotency` | |
 | `provenance` | `Provenance` | `v4.lens.ownership` | structural-readers batch; module name = ownership.dag today. |
 | `unused_parameters` | `UnusedParameters` | `v4.lens.unused_parameters` | |
-| `structural_resolution` | `StructuralResolution` | *(TBD v4 module)* | placeholder — ratify module path before impl. |
+| `structural_resolution` | `StructuralResolution` | `v4.lens.structural_resolution` | T-13 mirror — InferredTree + dependency projection (BindsTo use edges, T-9 resolve stamps). |
 
-**Substrate home-of-record (P2-staging — INVARIANTS §P2 / Practice 5):** **`src/v4/lens/registry.dag`** is the **canonical `.dag` surface** for closed rows: **`lens_id: LensIdV0`** (M4 closed set) plus **`module_path: LensModulePathV0`** as `Bound { path: … }` vs `Unbound`. A **landed** compiler **single authority** in the §P2 sense (declaration + realization + **generated** consumer) **does not exist yet** — same staging posture as `src/v4/std/fact_density.dag` until mechanical read; the paired **`v4_lens_registry_dag_smoke_test.rs`** receipt is **parse + inference cleanliness only** (INVARIANTS §P2 staging). The §3 markdown table is a **human mirror**; amend the `.dag` first, then align this table on operator-signed pin revision. Rows whose ratified v4 module is not yet fixed use **`Unbound`** in the substrate (same intent as *(TBD v4 module)* in the table); **never** encode that state as a fake `v4.lens.*` string or other string sentinel inside `path`.
+**Substrate home-of-record (P2-staging — INVARIANTS §P2 / Practice 5):** **`src/v4/lens/registry.dag`** is the **canonical `.dag` surface** for closed rows: **`lens_id: LensIdV0`** (M4 closed set) plus **`module_path: LensModulePathV0`** as `Bound { path: … }` vs `Unbound`. A **landed** compiler **single authority** in the §P2 sense (declaration + realization + **generated** consumer) **does not exist yet** — same staging posture as `src/v4/std/fact_density.dag` until mechanical read; the paired **`v4_lens_registry_dag_smoke_test.rs`** receipt is **parse cleanliness only** plus bounded **source-text** receipts for the closed `LensIdV0` set and key `Bound` rows (INVARIANTS §P2 staging; **not** an inference-stage or `compile_to_dag` guarantee — post-#3503 P9 `Symbol`/`List` imports defer single-file lowering until M2 multi-module load, same posture as `v4_bin_main_dag_smoke_test`). The §3 markdown table is a **human mirror**; amend the `.dag` first, then align this table on operator-signed pin revision. Rows whose ratified v4 module is not yet fixed use **`Unbound`** in the substrate (same intent as *(TBD v4 module)* in the table); **never** encode that state as a fake `v4.lens.*` string or other string sentinel inside `path`.
 
 **Runnable-AC column (today):** Rows requiring **closed `LENS_ID` names** cite **`src/v4/lens/registry.dag`**. Rows requiring **v4 parse bootstrap** cite the existing **v2 → v4** job in **`.github/workflows/ci.yml`** (`v2-compiler compile --source-root src/v4 …`). Rows that assert a **live CLI `LENS_ID` / whole-corpus compile gate** are **deferred** until **B2** — do not substitute an interim binary receipt. **Lens evaluation** (`Witness` / `DimensionOk` / `DimensionFail` on applied v4 `Lens<Output>` with **`--mode enforce|introspect`**) stays **`TBD …`** until the evaluation dispatch lands — do not treat compile-only receipts as evaluation substitutes.
 

src/v3/compiler/tests/integration/sg0_census_test.rs

@@ -845,8 +845,9 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[
     // `src/v4/extdeps/frameworks/react.dag` (zero module diagnostics).
     // SG-0 ratchet per INVARIANTS §P5(b) + typescript extdeps precedent.
     "src/v3/compiler/tests/integration/v4_extdeps_react_dag_smoke_test.rs",
-    // PREFIX T-23 v0: `compile_to_dag` smoke on `src/v4/lens/registry.dag` (P2-staging
-    // `LensIdV0` + `LensModulePathV0`; no generated consumer yet). SG-0 + INVARIANTS §P5(b) receipt.
+    // PREFIX T-23 v0: parse smoke on `src/v4/lens/registry.dag` (P2-staging `LensIdV0` +
+    // `LensModulePathV0`; post-#3503 P9 Symbol/List imports — isolated `compile_to_dag` deferred).
+    // SG-0 + INVARIANTS §P5(b) receipt.
     "src/v3/compiler/tests/integration/v4_lens_registry_dag_smoke_test.rs",
     // T-19 testgen Wave-0: parse ratchet on `src/v4/lens/testgen.dag` — T19ManualAnchorKey-driven
     // `bootstrap_claim_generator_for_manual_anchor` + `testgen_concept_for_manual_claim` +