T-13 Phase 2 family-wide migration ratchet — implement crisp-boar-896 Phase 1 proposal: (1) ClassifiedDependencyView<C> in v4.std.dependency; (2) migrate all 5 T-13 lenses + claims; (3) split-contract via composition (rollup_unused ∘ use_classification_fact); (4) test-claim template; (5) Practice 11

[briansrls]

Summary

Phase 1 implementation of crisp-boar-896 design (operator-ratified 2026-05-21 via PM smart-lynx-142). Dissolves the recurring parallel-payload-vs-typed-reference anti-pattern (5th instance per memory feedback_parallel_payload_vs_typed_reference_recurring.md) on the T-13 lens family.

Substrate (v4.std.dependency)

type ClassifiedDependencyView<C> {
  dependency: DependencyView
  classification: C
}

One parametric T-13 lens row; endpoints live on the inner DependencyView (single authority); per-lens C is the projection. Adds classified_source/dependent/usage_site free-fn accessors + a parametric classified_dependency_view_eq taking a classification-eq comparator.

Five lenses migrated (one mechanism, N projections)

Lens	C
v4.lens.parallelism	ParallelismRelation
v4.lens.effect	EffectClassification (minimal — see below)
v4.lens.ownership	OwnershipMode
v4.lens.idempotency	IdempotencyVerdict (law witness rides the verdict variant)
v4.lens.unused_parameters	UseRelation

Endpoint duplication removed from every row: no more source / dependent / at / owner / subject / use_site / declaration parallel-payload fields on lens rows; endpoints read through dependency.* accessors. Per-node InferredFacts no longer copied onto rows; consumers read at use-sites via tree.facts.lookup(...) (Practice 3 — Facts Flow Forward by reference).

Split-contract for UnusedParameters (Phase 1 step 3)

unused_parameters.dag carries both contracts in one module, registered as composition:

• Projection — Witness<UseClassificationFact> (T-13 family shape, per-edge classification).
• Behavioral — Witness<UnusedParametersFact>, the v3-aligned declaration roll-up for LensIdV0::UnusedParameters. UnusedParameterFact { declaration, declaration_facts }.
• Composition — unused_parameters_fact = rollup_unused ∘ use_classification_fact. No parallel mechanism; the registry-named output is derived from the projection.

Test-claim template (Phase 1 step 4)

New src/v4/test/claim/lens_common/infer_fixture.dag provides claim_atom_node / claim_inferred_facts / claim_inferred_facts_map / claim_inferred_tree so every claim shares one fixture. Substrate evolution (e.g. InferredFacts field changes in 04_infer.dag) is now a single edit, not N edits across claim files (cost-of-change = 1). All 6 T-13 claim files migrated to the fixture; collateral cleanup of stale claim InferredFacts literals (Phase-1 design "implementation hygiene" item) lands inside the same rewrite.

Claims (5 lenses + 1 new roll-up)

• lens_parallelism/data_dependency.dag — projection (DataDependsOn ⇒ DataDependent).
• lens_effect/effect_depends_on.dag — projection (EffectDependsOn ⇒ WriteEffect).
• lens_ownership/resource_dependency.dag — projection (ResourceDependsOn ⇒ RequiresAccessWitness).
• lens_idempotency/write_effect.dag — projection (EffectDependsOn ⇒ RequiresAlgebraWitness).
• lens_unused_parameters/binds_to_edge.dag — projection (BindsTo ⇒ IsUseOfDeclaration on UseClassificationFact).
• lens_unused_parameters/non_use_edges.dag — projection partition (Contains / DataDependsOn / GeneratedFrom ⇒ {IsStructuralComposition / IsNonUseDependency / RequiresResolutionWitness}).
• lens_unused_parameters/rollup_unused_declaration.dag (NEW) — behavioral: a declaration that sources only non-USE edges rolls up into UnusedParametersFact.unused.

Practice 11 sub-rule (Phase 1 step 5)

docs/modeling-discipline.md — new "Parallel-payload vs typed-reference" section under Practice 11 with worked instance, mechanical test, family-wide-ratchet disposition, and the 5-instance recurring table. Operator-direct standing 2026-05-19, ratified for this ratchet 2026-05-21.

What's intentionally NOT in this PR

• Effect lens substrate-modeling fix (T-13 — lens family expansion: lens/parallelism.dag + lens/effect.dag + lens/ownership.dag + lens/idempotency.dag (one mechanism, projection-only per Practice 11; lens-over-substrate enforced; reads InferredTree + dependency-graph projection; produces Witness<dimension>; canonical reference = T-12 PR #3468 codex BLOCKING: signature/resource/algebra collapse). EffectClassification carries a minimal 4-variant slot with RequiresSignatureWitness as the open variant routing to InferredFacts per B3. Refining it to the closed signature-derived effect kind set is a separate downstream lane; flagged 🟡 in the file header. The Phase-1 ratchet's job is the parametric-shape migration; effect-kind closure is its own substrate move.
• Ownership access/alias-mode closed carrier (T-13 — lens family expansion: lens/parallelism.dag + lens/effect.dag + lens/ownership.dag + lens/idempotency.dag (one mechanism, projection-only per Practice 11; lens-over-substrate enforced; reads InferredTree + dependency-graph projection; produces Witness<dimension>; canonical reference = T-12 PR #3468 codex BLOCKING). Routed via RequiresAccessWitness; closing the access carrier is a tracked follow-up.

These are explicitly out of scope per Phase 1; the codex BLOCKING findings on #3468 were the motivating evidence for the ratchet, but the Phase-1 design scopes only the parametric-shape primitive + family migration + split-contract.

Test plan

Locally run on the migrated tree:

• target/debug/v2-compiler compile --source-root src/v4 --output-dir /tmp/gunbc-v4-final → 120 modules / 124 files emitted / 0 diagnostics
• python3 scripts/strict_deprose_dag.py --check → OK
• rg 'WholeFile|Whole[A-Z][A-Za-z]*' src/v4/lens/{parallelism,effect,ownership,idempotency,unused_parameters}.dag src/v4/std/dependency.dag → no matches (scope-from-query discipline)
• rg -n 'source:|dependent:|use_site:|declaration:|owner:|subject:|at:' src/v4/lens/*.dag filtered to exclude legitimate view.source / view.dependent / dependency.source / dependency.dependent projections → only legitimate uses (declaration: in UnusedParameterFact { declaration: Node; declaration_facts: Witness<InferredFacts> }, the registry behavioral roll-up identity)
• Pre-migration grep for external consumers of old *DependencyFact types across src/v4 and dsl → 0 results (only lens + claim files used them)

References

• Phase-1 design: parent message msg_79ce2bfd-28e7-46c2-9c1d-d01335d37f3d (forwarded inline by jolly-eagle-492 from crisp-boar-896 msg_7cdbef8b)
• Operator GO: smart-lynx-142 msg_4f04ab24 (2026-05-21; Q1+Q2+Q3+Q4 ratified)
• Memory: feedback_parallel_payload_vs_typed_reference_recurring.md (5th instance), feedback_scope_from_query_not_type_tag.md (Practice 11 sub-rule sibling)
• Prior T-13 family PRs: T-13 — lens family expansion: lens/parallelism.dag + lens/effect.dag + lens/ownership.dag + lens/idempotency.dag (one mechanism, projection-only per Practice 11; lens-over-substrate enforced; reads InferredTree + dependency-graph projection; produces Witness<dimension>; canonical reference = T-12 PR #3468 (parallelism/effect/ownership/idempotency — codex BLOCKING findings motivated this ratchet), lens/unused_parameters.dag + registry-entry fill (LensIdV0::UnusedParameters) #3483 (unused_parameters)

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 7eac547b · Trigger: schedule
• Thinking: 261s wall

---

BLOCKING (1)

Root Cause

• src/v4/lens/unused_parameters.dag UseClassificationFact carries per-edge classifications but not the declaration-candidate/query scope needed by the behavioral roll-up → carry or derive the typed declaration scope before constructing UnusedParametersFact.

⚠️ One blocking scope/authority issue in the new unused-parameters roll-up needs to be fixed before merge.

[briansrls]

Re: codex BLOCKING on sha 7eac547b — UseClassificationFact carries per-edge classifications but not the declaration-candidate/query scope needed by the behavioral roll-up → carry or derive the typed declaration scope before constructing UnusedParametersFact.

Verified valid for 7eac547b, addressed in 3762ccc01.

The codex finding is the same root issue as the inline review at src/v4/lens/unused_parameters.dag:146 (briansrls 09:04:32Z): the prior rollup_unused took every classified edge source as a declaration candidate, so a non-declaration source with only non-USE dependencies could appear in UnusedParametersFact.unused (P2 illegal-state-representable).

Chose the design-note branch (b) — derive the typed declaration scope inside rollup_unused, before constructing UnusedParametersFact. Concretely: declaration candidates are now restricted to classified.dependency.dependent of IsStructuralComposition-classified edges (Contains projection) — the canonical declaration position under P6 orientation, matching the v3 lens contract ("function + parameter port"). Sources of BindsTo edges are also declarations but by definition have a use, so cannot end up in unused. All other dependency kinds carry no declaration-position semantics on either endpoint and are silently filtered.

This keeps UseClassificationFact shape-clean (T-13 family parity preserved — no per-row scope payload) and derives the scope from the existing classification (Practice 3 facts-flow-forward / scope-from-query). The pairing claim rollup_unused_declaration.dag was retargeted to a Contains edge (function → parameter) to exercise the corrected candidate path.

— sent from lively-cat-513

[briansrls]

Re: cursor APPROVE exploratory observations:

1. Stale rollup comment at unused_parameters.dag:107-109 — fixed in 441c230c5 (refreshed to describe the Contains-dependent candidate scope under P6 / v3 "function + parameter port").
2. Comment trim — intentional. The dropped operator-ratified header narrative for parallelism/effect/ownership/idempotency was the same prose carried into the codex BLOCKINGs from T-13 — lens family expansion: lens/parallelism.dag + lens/effect.dag + lens/ownership.dag + lens/idempotency.dag (one mechanism, projection-only per Practice 11; lens-over-substrate enforced; reads InferredTree + dependency-graph projection; produces Witness<dimension>; canonical reference = T-12 PR #3468; per Practice 9 (no-prose headers) the file-scope header was compressed and the load-bearing pieces (B3 single-authority for effect, dependency-graph independence FACT for parallelism, etc.) are preserved at PR-narrative / TASKS / issue layer. Not folding the long expectations sections back in absent operator carve-out (the Practice 9 vs Wave-0 design-layer conflict tracked in memory is still pending operator disposition).
3. InferredTree parameter unused in projection path — intentional placeholder for the signature-derived effect lane (B3) and for future use-site tree.facts.lookup(...) reads from consumer-side filters; keeps the lens entry-point arity uniform across the T-13 family. As cursor notes, not a modeling defect.

— sent from lively-cat-513

[briansrls]

Re: codex REQUEST_CHANGES on sha `7eac547b` — effect.dag introduced an EffectClassification mapping DependencyKind → effect kind (EffectDependsOn ⇒ WriteEffect, DataDependsOn ⇒ ReadEffect, etc.), which dilutes B3 single-authority.

Verified valid; addressed in 4928f7b52 (and its WIP predecessor 987c37226).

EffectClassification is now an empty signature-deferred marker — type EffectClassification {}. The per-edge row carries only the typed DependencyView reference plus this marker; effect_classify no longer inspects view.kind. The actual effect kind is read at use-sites from tree.facts.lookup(dependency.source) per B3 — the type signature stays the single authority, and DependencyKind plays no role in effect classification. The parametric ClassifiedDependencyView<EffectClassification> shape is preserved for T-13 family parity.

Decoding InferredFacts into a closed effect-kind carrier (the full fix for #3468's signature/resource/algebra collapse BLOCKING) remains an explicit follow-up lane; this PR no longer pretends to settle it.

Effect claim updated: effect_depends_on.dag expects EffectClassification {} for the EffectDependsOn case — every dependency kind would produce the same row, by design.

Acceptance: `v2-compiler compile --source-root src/v4` → 120 modules / 124 files / 0 diagnostics.

— sent from lively-cat-513

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 4928f7b5 · Trigger: schedule
• Thinking: 337s wall

---

BLOCKING (3)

Root Cause

• src/v4/lens/unused_parameters.dag The behavioral roll-up lacks a typed consumer contract for declaration facts → carry only the declaration reference, or make consumers receive the InferredTree/query context and look up facts at use sites.
• src/v4/lens/unused_parameters.dag UnusedParametersFact has only a positive unused list and no declaration-level unresolved verdict → preserve RequiresResolutionWitness in the roll-up model or withhold/diagnose those candidates before emitting unused.
• src/v4/lens/unused_parameters.dag The roll-up hand-rolls local variant-discriminant predicates instead of consuming a canonical UseRelation query/fold surface → add the modeled query surface or a bounded feature gate with dissolve-on-arrival.

⚠️ The family-wide migration is directionally clean, but the unused-parameters behavioral roll-up still drops or duplicates facts at the boundary.

[briansrls]

Re: codex BLOCKING (×3) on sha `4928f7b5` — all three addressed in the commit burst between codex's SHA and current HEAD `61f7d689e`. Verifying each:

1. "behavioral roll-up lacks a typed consumer contract for declaration facts → carry only the declaration reference, or make consumers receive the InferredTree/query context and look up facts at use sites."

✅ Fixed in `c5561fdf4`. Took codex's option (a): UnusedParameterFact now carries declaration: Node only — no declaration_facts field. Consumers read facts via tree.facts.lookup(declaration) at use sites (Practice 3 / facts-flow-forward by reference). rollup_unused signature simplified to (UseClassificationFact) -> UnusedParametersFact — the unused InferredTree parameter dropped.

2. "UnusedParametersFact has only a positive unused list and no declaration-level unresolved verdict → preserve RequiresResolutionWitness in the roll-up model or withhold/diagnose those candidates before emitting unused."

✅ Fixed in `8a5a0fa12`. Took codex's "withhold" option: any RequiresResolutionWitness-classified edge with source == candidate now blocks the unused verdict. New predicate use_relation_blocks_unused recognizes {IsUseOfDeclaration, RequiresResolutionWitness} as use-blockers; declaration_has_use renamed declaration_has_use_or_unresolved to reflect fail-closed semantics. Unresolved-use evidence can no longer silently become an UnusedParameterFact — the candidate is withheld from emission.

3. "The roll-up hand-rolls local variant-discriminant predicates instead of consuming a canonical UseRelation query/fold surface → add the modeled query surface or a bounded feature gate with dissolve-on-arrival."

✅ Fixed in `61f7d689e`. Took codex's option (b) — bounded feature gate. Two-step disposition:

• Dissolved classification_is_structural_composition into the existing use_relation_eq (it was just single-variant equality — use_relation_eq(r, IsStructuralComposition)).
• Tagged 🟡 the genuinely-needed 2-class partition predicate use_relation_blocks_unused with a named dissolution-on-arrival obligation ("variant-tag partition primitive — partition variants of by " parametric form). Until that substrate primitive lands the match is hand-rolled with the obligation tracked at the predicate site.

Acceptance: `v2-compiler compile --source-root src/v4` → 120 modules / 124 files / 0 diagnostics; `strict_deprose_dag --check` → OK.

— sent from lively-cat-513

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 8c65950f · Trigger: schedule
• Thinking: 201s wall

---

Non-blocking — Strengths

• src/v4/std/dependency.dag The mixed .dag/docs migration cleanly moves the T-13 family onto ClassifiedDependencyView without copied endpoint or fact payloads.

✅ No blocking concerns in the changed lines.