SG-5/SG-6: worksheet §6 closure + falsification receipts (substrate on main)

_internal/INVARIANTS_OPS.md

@@ -63,7 +63,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX
 | `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`**) plus Lens-CI activation (`src/v4/workflow/ci.dag` consumes registry-backed `LensIdV0` rows). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **P2 / Practice 5:** this host harness is a **parse-surface structural ratchet** for `src/v4/lens/registry.dag` + its `src/v4/workflow/ci.dag` consumer + the live `.github/workflows/ci.yml` Lens-CI signal binding, while preserving the staged T-23/P9 registry parse-cleanliness receipts; the semantic interface is checked in CI by `gunbc compile` over a temporary `ci.dag` entry root plus `src/v4` dependency root (not `--target dag`, which is blocked by the known DAG-artifact hang). **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 / CI pairing. **Dissolution:** remove when `registry.dag` and Lens-CI workflow wiring are exercised only by `.dag` `TestClaim` rows / a generated harness that mechanically reads registry rows and workflow commands without this per-file Rust parse ratchet. **Interim ratchet:** `v4_lens_registry_dag_tokenizes_and_parses` tokenizes/parses the pinned registry source and asserts module path, `LensIdV0`/`LensModulePathV0`, `lens_registry_v0`, `lens_registry_ids_resolve`, `lens_registry_row_count`, and `lens_registry_bound_row_count`; `v4_lens_registry_t23_closed_lens_ids_present` pins the eight-arm closed set; `v4_lens_registry_structural_resolution_bound_to_module` pins `StructuralResolution` → `Bound { path: "v4.lens.structural_resolution" }`; `v4_lens_registry_p9_owned_fn_surface_present` pins the P9 `LensOwnedFnV0` / `lens_owned_fn_registry_v0` substrate rows; `v4_ci_workflow_consumes_lens_registry_for_lens_ci_signal` tokenizes/parses `ci.dag`, asserts the `lens_registry_ids_resolve` import, `LensCiCommand.required_lenses: List<LensIdV0>`, the six required `LensIdV0` policy rows, `lens_ci_registry_signal` gate data, `lens_ci_registry_execution.needs == [v2_compile_src_v4]`, and `lens_ci_live_workflow_signal` as the modeled live-step binding without re-authoring the `ci_pipeline` signal/job/policy facts. It then parses `.github/workflows/ci.yml` and checks those modeled step names execute the registry smoke plus rust-target semantic compile. **Paired CI semantic gate:** `Lens-CI registry semantic v4 compile (rust target)` copies `src/v4/workflow/ci.dag` into a temporary entry root, copies `src/v4` into a dependency root with `workflow/ci.dag` removed, and runs `target/release/gunbc compile --source-root "$entry_root" --source-root "$deps_root" --output-dir "$RUNNER_TEMP/v4-lens-ci-rust" --target rust` so lowering/inference of `ci_command_authority_ok -> lens_registry_ids_resolve` is checked through the workflow consumer and its transitive v4 imports without making unrelated v4 extdeps entry modules for this Lens-CI signal. |
 | `src/v3/compiler/tests/integration/v4_lens_testgen_dag_smoke_test.rs` | **ROADMAP:** `_internal/ROADMAP_OPS.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 remains keyed by **`ManualAnchorKey`**; **`Generator.anchor`** now reuses the same **`ClaimAnchorKey`** carrier as **`TestClaim.anchor`**, with manual rows wrapped by **`ManualClaimAnchor`** after **`Outcome`** rejects **`ManualAnchorAbsent`** on lookup and generated rows partitioned under **`GeneratedClaimAnchor`** (**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_anchor_field_is_claim_anchor_key`; `v4_lens_testgen_wave0_concept_projection_matches_claim_anchor`; `v4_lens_testgen_wave0_generator_carries_claim_classification_and_anchor`; `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.anchor: ClaimAnchorKey` 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); plus the **T-19 witness-validity generator-category guard** (PR #3565 same-file expansion, **+0 census paths**, P5 Mechanism (b) same-path ratchet): `v4_lens_testgen_witness_validity_modules_tokenize_and_parse`, `v4_lens_testgen_witness_validity_helper_returns_outcome_testclaim`, `v4_lens_testgen_witness_validity_module_imports_helper_from_lens_testgen`, `v4_lens_testgen_witness_validity_module_pins_four_row_corpus_via_helper`, `v4_lens_testgen_witness_validity_module_authors_no_testclaim_literals` — pin both `src/v4/lens/testgen.dag` + `src/v4/test/claim/generated/witness_validity.dag` parse, `testgen_emit_witness_validity_claim` return type `Outcome<TestClaim>`, helper-routing import, exact 4-row corpus (1 positive + 3 negative arms), and the no-`TestClaim`-literal tautology-skip discipline on the generated module. Parse-only structural ratchet; `Generator` carries `kind`, `anchor`, `classification`, and `slot` per TASKS T-19. plus the **T-19 anchor-strip + AlgebraLaw subject helper guard** (PR #3636 same-file expansion, **+0 census paths**, P5 Mechanism (b) same-path ratchet): `v4_lens_testgen_wave0_generator_anchor_field_is_claim_anchor_key` asserts `Generator.kind: TestClaimCoproductVariant` and `Generator.anchor: ClaimAnchorKey`; `v4_lens_testgen_wave0_concept_projection_matches_claim_anchor` asserts match on `test_claim_anchor(c: claim)`; `v4_lens_testgen_wave0_generator_carries_claim_classification_and_anchor` adds `kind: test_claim_coproduct_variant(c: claim)` substring check; `assert_six_algebra_law_subject_paths_in_testgen` asserts `algebra_law_subject_for_manual_anchor` helper exists, match dispatch in `testgen_concept_for_manual_claim`, single `value: AlgebraLaw {` constructor site, all six `ManualNat*` anchor names (`ManualNatAddLeftIdentity`, `ManualNatAddRightIdentity`, `ManualNatAddAssociativity`, `ManualNatMulLeftIdentity`, `ManualNatMulAnnihilator`, `ManualNatMulAssociativity`) in helper body, and six `value: AlgebraLawSubject {` projection arms; `assert_nat_algebra_law_subject_symbols_in_substrate` adds six forbidden `nat_algebra_law_subject_symbol_*` substring checks (nat substrate must not re-export mirror operation/value symbols); `generator_field_ty` (parametric field-name lookup) and `between<'a>` helper added. |
 | `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`, T-33-Q10 `EffectSignature` / `ResourceAccess`, and effect/partiality scaffolds). **ROADMAP:** `_internal/ROADMAP_OPS.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_effect_signature_resource_access_shape`; `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`, `EffectSignature`, `ResourceAccess`, `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.operation` / `PartialOperationDecl.operation` `Node` authority, `PrimitiveOperationRef.effect_signature: EffectSignature`, `EffectSignature { signature: Node }` with resource authority kept on `BoundaryAllowance.resource`, `ResourceAccess { resource: Node }`, 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/v4_std_target_realization_dag_smoke_test.rs` | **SG-1** (`src/v4/std/target_model.dag` — `TargetAtomRealization` canonical carrier per design-target-realization-canonical-home.md Option A, catalog encode/decode, `TargetValueTemplate` fail-closed `Outcome` application; Rust Symbol/Bool/Char rows in `src/v4/extdeps/languages/rust.dag`; `src/v4/compiler/06_translate.dag` consumer). **ROADMAP:** `_internal/ROADMAP_OPS.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 `target_model.dag` SG-1 realization surface is exercised only by `.dag` `TestClaim` rows / a generated harness / merged M2 multi-module lowering without this host `parse_for_test` structural ratchet. **Interim ratchet:** `v4_std_target_realization_dag_tokenizes_and_parses`; `v4_std_target_realization_declares_target_atom_realization_carrier`; `v4_std_target_realization_declares_catalog_lookup`; `v4_translate_dag_imports_target_atom_realization_consumer`; `v4_rust_language_model_declares_target_atom_realization_rows` — tokenize/parse `target_model.dag`, assert `TargetAtomRealization` field bundle (`source_carrier`, `type_form`, `value_form`), catalog lookup + row-driven type/value consumers, translate imports + `translate_target_atom_realization_for_carrier`, Rust atom-realization rows without parallel `rust_std_projection_*` sentinels. |
+| `src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs` | **SG-1** (`src/v4/std/target_model.dag` — `TargetAtomRealization` canonical carrier per design-target-realization-canonical-home.md Option A, catalog encode/decode, `TargetValueTemplate` fail-closed `Outcome` application; Rust Symbol/Bool/Char rows in `src/v4/extdeps/languages/rust.dag`; `src/v4/compiler/06_translate.dag` consumer) + **SG-5/SG-6** (`TargetCollectionRealization` + `bounded_lattice_completeness.dag` / `04_infer` consumer gate — worksheet `docs/planning/v4-sg5-sg6-collection-bounded-lattice-worksheet-2026-05-30.md` §6; substrate #3957 / #4085 on `main`). **ROADMAP:** `_internal/ROADMAP_OPS.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. **This PR (+0 SG-0 paths):** expands the existing harness with three parse/tokenize smokes for SG-5 collection realization + translate consumer + SG-6 infer gate wiring (`v4_std_target_model_declares_target_collection_realization_carrier`, `v4_translate_dag_imports_collection_realization_consumer`, `v4_bounded_lattice_completeness_and_infer_gate_are_wired`); pairs with manual `CompilesClaim` falsification in `infer_bounded_lattice_completeness_anchor.dag` (no new census literal). **Dissolution:** remove when `target_model.dag` realization surfaces are exercised only by `.dag` `TestClaim` rows / a generated harness / merged M2 multi-module lowering without this host `parse_for_test` structural ratchet. **Interim ratchet:** `v4_std_target_realization_dag_tokenizes_and_parses`; `v4_std_target_realization_declares_target_atom_realization_carrier`; `v4_std_target_realization_declares_catalog_lookup`; `v4_translate_dag_imports_target_atom_realization_consumer`; `v4_rust_language_model_declares_target_atom_realization_rows`; `v4_std_target_model_declares_target_collection_realization_carrier`; `v4_translate_dag_imports_collection_realization_consumer`; `v4_bounded_lattice_completeness_and_infer_gate_are_wired` — tokenize/parse pinned `.dag` sources, assert SG-1 atom-realization + SG-5 collection carrier/coproducts + translate collection consumer + SG-6 completeness import/gate symbols. |
 | `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`. |
 | `src/v3/compiler/tests/integration/lens_application_substrate_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#89** `section_ref_substrate_landed` (T-Lens-Application-Surface — `SectionRef` disjoint sum over `DeclarationScope` and `NodeScope` in `src/v3/std/lens_application.dag`; design authority `docs/design-lens-application-surface.md` §1.2–§2). **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 harness. **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `SectionRef` variant labels, field names, and `DeclarationId` / `NodeId` nominal wiring against `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as gate **#62** `file_attachment_substrate_carrier_test.rs`). **Interim ratchet:** `gate_89_section_ref_is_disjoint_sum_from_lens_application_authority` pins variant order (`DeclarationScope` then `NodeScope`) and payload fields to `lens_application.dag`. |
 | `src/v3/compiler/tests/integration/workflow_substrate_carriers_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#53** `workflow_substrate_carriers_landed` (T-Workflow-As-Data Slice 1; worker brief `docs/briefs/r3-substrate-t-workflow-as-data-slice-1-worker.md`). **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `WorkflowSecret`, `SecretScope`, `CronSchedule`, and `CronField` structural shape against `generated_full_bootstrap_dag()` without this hand-Rust ratchet. **Interim ratchet:** `workflow_secret_shape_locked` + `secret_scope_variants_locked` + `cron_schedule_shape_locked` + `cron_field_variants_locked` pin the Slice 1 β-ratified carriers (STOP+PING discipline on `CronSchedule` field-count drift >5 per brief). |