fix(v3-compiler): gate #87 regen harness honesty (TESTING.md) + #74 scope doc

src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_cost_target_realization.dag

@@ -1,5 +1,9 @@
 // R3 gate #87 — `LensRegistryEntry` `cost_target_realization` (`.dag` harness placeholder).
-// Rust consumer receipts: `lens_cost_target_realization_test.rs`.
+// Rust consumer receipts: `lens_cost_target_realization_test.rs` and
+// `r3_gate_87_lens_cementing_regen_receipts_test::r3_gate_87_cost_target_realization_rust_receipt_resolves_type_realization_row`.
+//
+// **Discipline:** `Compiles` is wiring-only — not `type_realization_meta` / declaration-resolution
+// behavior. Unrelated runner predicates must not masquerade as this lens row.
 
 module v3.compiler.tests.t_r3.gate_87_cementing_regen_cost_target_realization
 

src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_effect_enumeration.dag

@@ -2,6 +2,11 @@
 // Executable `enumerate_effects` receipt on a minimized program lives in
 // `r3_gate_87_lens_cementing_regen_receipts_test.rs` until a `LensOutputEquals` carrier
 // can freeze `EffectEnumerationReport` without walking the full bootstrap roster.
+//
+// **Discipline:** This claim stays `Compiles` on a trivial program — it only ratchets that the
+// harness module lowers through the runner table. Do **not** swap in unrelated predicates
+// (e.g. `PortHasState` on `let lit: Int = 7`): they would read as lens behavior but would not
+// exercise `effect_enumeration` (`TESTING.md` — test names must match what is proven).
 
 module v3.compiler.tests.t_r3.gate_87_cementing_regen_effect_enumeration
 

src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_infer_helpers.dag

@@ -1,5 +1,9 @@
 // R3 gate #87 — `LensRegistryEntry` `infer_helpers` (`.dag` harness placeholder).
-// Structural / emit migration receipts: `m2_substrate_inhabitance_test` + `m2_lens_*` modules.
+// Structural / emit migration receipts: `m2_substrate_inhabitance_test` + `m2_lens_*` modules;
+// lens source compile: `r3_gate_87_infer_helpers_lens_source_compiles`.
+//
+// **Discipline:** `Compiles` on a trivial program is inventory/wiring only — not infer-helpers
+// lens application. Do not assert unrelated bind-resolution facts under this row name.
 
 module v3.compiler.tests.t_r3.gate_87_cementing_regen_infer_helpers
 

src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_lower_helpers.dag

@@ -1,6 +1,10 @@
 // R3 gate #87 — `LensRegistryEntry` `lower_helpers` (`.dag` harness placeholder).
 // Structural receipts: `bridge_lower_helpers_patch_zero_residual_test.rs`,
-// `m2_substrate_inhabitance_test.rs`.
+// `m2_substrate_inhabitance_test.rs`; lens source compile:
+// `r3_gate_87_lower_helpers_lens_source_compiles`.
+//
+// **Discipline:** `Compiles` here is wiring-only for the regen harness slot — not lower-helpers
+// lens behavior. Unrelated predicates must not stand in for that contract.
 
 module v3.compiler.tests.t_r3.gate_87_cementing_regen_lower_helpers
 

src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_provenance.dag

@@ -2,6 +2,9 @@
 // `origin_of` / `Origin` parity receipts stay in Rust (`cementing_lens_registry_dispatch_test`,
 // `m2_lens_provenance_migration_test`) until `LensOutputEquals` can compare stable `Origin`
 // literals on fixture ports.
+//
+// **Discipline:** `Compiles` here is harness wiring only — not provenance lens output. Do not
+// substitute unrelated predicates that imply provenance behavior without applying the lens.
 
 module v3.compiler.tests.t_r3.gate_87_cementing_regen_provenance
 

src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_structural_resolution.dag

@@ -1,7 +1,10 @@
 // R3 gate #87 — `LensRegistryEntry` `structural_resolution` (`.dag` harness placeholder).
 // `LensOutputEquals` over `List<UnresolvedArrowBody>` literals is not yet structurally
 // authorable in strict user modules (M1(2.8) opaque-body gate on imported lens row types).
-// Executable receipt: `r3_gate_87_lens_cementing_regen_receipts_test::r3_gate_87_structural_resolution_rust_receipt`.
+// Executable receipt: `r3_gate_87_lens_cementing_regen_receipts_test::r3_gate_87_structural_resolution_rust_receipt_on_literal_program`.
+//
+// **Discipline:** `Compiles` is wiring-only — not structural-resolution lens output. Do not
+// substitute unrelated bind-resolution checks under this row name.
 
 module v3.compiler.tests.t_r3.gate_87_cementing_regen_structural_resolution
 

src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_unused_parameters.dag

@@ -4,6 +4,9 @@
 // M1(2.8) opaque-body on `TestClaim` / carrier literals (same class as
 // `structural_resolution` + `List<UnresolvedArrowBody>`). Parity receipt:
 // `r3_gate_87_lens_cementing_regen_receipts_test::r3_gate_87_unused_parameters_rust_receipt_on_literal_program`.
+//
+// **Discipline:** `Compiles` is wiring-only — not unused-parameter lens output. Unrelated
+// predicates must not read as this lens under the row name.
 
 module v3.compiler.tests.t_r3.gate_87_cementing_regen_unused_parameters
 

src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_variant_payload.dag

@@ -1,5 +1,9 @@
 // R3 gate #87 — `LensRegistryEntry` `variant_payload` (`.dag` harness placeholder).
-// Emit / migration receipts: `m2_lens_variant_payload_migration_test.rs`.
+// Emit / migration receipts: `m2_lens_variant_payload_migration_test.rs`;
+// lens source compile: `r3_gate_87_variant_payload_lens_source_compiles`.
+//
+// **Discipline:** `Compiles` is wiring-only — not variant-payload lens output. Do not attach
+// unrelated resolver predicates under this registry row name.
 
 module v3.compiler.tests.t_r3.gate_87_cementing_regen_variant_payload
 

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

@@ -4,6 +4,8 @@
 //! `src/v3/compiler/regen.dag` registry lenses whose `tests/dag/t_r3_gate_87_cementing_regen_*.dag`
 //! harnesses are still `Compiles` placeholders (bootstrap-scale / multi-arg lenses where a frozen
 //! `LensOutputEquals` / `DifferentialEquals` witness is not yet authored as `.dag` data).
+//! Placeholder claims intentionally prove **harness wiring** only; they must not use unrelated
+//! runner predicates that read as lens behavior without applying the named lens (`TESTING.md`).
 //!
 //! **Lane-E + symbolic-cost** `.dag` receipts are exercised by `t_pb_b_1_dag_runner_test`.
 //! `unused_parameters` and `structural_resolution` stay `Compiles` placeholders in `.dag` until

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

@@ -254,6 +254,11 @@ fn r1_gates_testgen_structural_coverage_suite_passes_through_runner() {
     );
 }
 
+// R3 gate #74 (`tests_as_data_demonstration`) — executable `.dag` `TestClaim` + runner receipt
+// lives in `r3_tests_as_data_demonstration_suite_passes_through_runner` above (and
+// `tests/dag/t_r3_tests_as_data_demonstration.dag` on `main`). Gate-#87 regen harnesses below are a
+// separate ratchet; do not conflate the two in PR titles or census expectations.
+
 // R3 gate #87 — every `LensRegistryEntry` in `src/v3/compiler/regen.dag` has a
 // `tests/dag/t_r3_gate_87_cementing_regen_<name>.dag` harness evaluated here.
 const R3_GATE_87_CEMENTING_HARNESS_PATH_PREFIX: &str =