v4 infer: remove v4.lens.cost / SymbolicCost (C1 cherry-pick from PR #3441)

[briansrls]

Summary

Salvaged C1 from the Wave-1 Worker C PR (#3441 / tidy-eagle-109). The P3 commitment 4 violation removal is clean, self-contained, and worth landing on its own; the rest of #3441 needs re-doing under the post-Pass-B / post-Practice-11 framing and lands as Wave-2 corrections.

What

src/v4/compiler/04_infer.dag was importing v4.lens.cost { SymbolicCost } and carrying cost: SymbolicCost as a field on InferredFacts. That makes cost-lens a compile-core fact rather than a lens-side dimensional projection over InferredTree. Per the v4 design doc's P3 commitment 4 (no specific lens imports in compiler-core) and Q14b rejection (cost-lens cannot drive compile-core target selection), this import is a hard violation.

Changes

src/v4/compiler/04_infer.dag only — 4 hunks:

• Header // Consumes: line — strip v4.lens.cost
• Import block — remove import v4.lens.cost { SymbolicCost }
• Type InferredFacts — remove cost: SymbolicCost field
• RULING-1 comment — cost/inhabitance coordinates remain T-9/T-12 bridged → inhabitance coordinates remain T-9 bridged (T-12 was the cost-lens task; no longer referenced from infer)

What was kept (and why)

• inhabits: AlgebraRef — algebra inhabitance is a real grounding fact required by T-9.
• descent: TerminationProof — termination is a semantic validity witness for grounding, NOT a cost/complexity projection. Out-of-scope follow-up could rename to descent_witness for clarity, but the current name is not a P3 violation.

Where cost-lens still lives

Cost / complexity / SymbolicCost remains a legitimate concept — it lives lens-side per the lens framework. validate_then_compile can gate on complexity via a required lens (e.g. [ComplexityLens(max = Linear)]); coercion_fold cannot consult it. Per Ratified Q14b in the v4 design doc, cost-lens-driven compile-core target selection is explicitly rejected.

Wave-1 disposition context

This PR is the C1 cherry-pick from the larger Wave-1 disposition. The other parts of #3441 are NOT pulled here:

• C2 (extdeps/file_system.dag with NodeFileBinding) — concept-home boundary violation (extdeps shouldn't know about Node); needs re-do under Practice 11 companion discipline.
• C3 (std/outcome.dag + NodeOutcomeFold) — uses legacy Produced/Rejected{diagnostic} Outcome shape + algebra signature gives policy authority to the algebra instead of the combinator; needs re-do against ratified Outcome shape + combinator-owns-policy discipline.

Both C2 and C3 will be dispatched as Wave-2 corrections under a corrected brief; PR #3441 will be closed after this one lands.

Test plan

• Manual review confirms only 04_infer.dag touched
• grep confirms no other file references cost: SymbolicCost or SymbolicCost from 04_infer.dag's context (cost-lens-side SymbolicCost is fine and stays)
• CI green

🤖 Generated with Claude Code

[briansrls]

@cursor exploratory observation upgraded to in-PR fix in commit a12d49559.

You were right that two claim scaffolds construct InferredFacts { cost: ... }, and on second look those files are NOT inert — they are scaffold-data files that v2-compile would fail on after the cost: field removal. Treated as a hidden BLOCKING rather than an out-of-PR follow-up since merging without them would break CI.

Cleanup (same PR, atomic):

src/v4/test/claim/manual/infer_emit_compile_anchor.dag:

• Header // Owns: drops anchor_stub_cost
• Header // Consumes: drops lens/cost.dag
• import v4.lens.cost { SymbolicCost, UnknownCost } removed (now unused)
• data anchor_stub_cost: SymbolicCost = UnknownCost { ... } declaration removed
• anchor_stub_inferred_facts: cost: anchor_stub_cost field removed

src/v4/test/claim/workflow/pipeline_rejections.dag:

• import v4.lens.cost { UnknownCost } removed (now unused)
• workflow_inferred_facts(): cost: UnknownCost { ... } field removed

Final sweep:

• grep -rn "import v4.lens.cost" src/v4/ → zero hits
• grep -rn "cost: SymbolicCost" src/v4/ → zero hits
• All InferredFacts {} construction sites match the new field shape

Other cost: matches in src/v4/ are unrelated lens-side / per-target-language declared costs (operation_cost, instruction_cost, etc. in extdeps/languages/*.dag; lens_registry_v0_cost in lens/registry.dag) — those are correctly lens-side, not compiler-core, and stay.

PR now atomic and CI-safe. Your APPROVE on the 04_infer.dag change stands.

[cursor]

I validated that PR comment end-to-end, and it is already fully applied in this branch (including commit a12d49559).

• Confirmed cleanup is present in all three files:
  • src/v4/compiler/04_infer.dag no longer imports v4.lens.cost, and InferredFacts no longer has cost.
  • src/v4/test/claim/manual/infer_emit_compile_anchor.dag no longer carries anchor_stub_cost/cost import, and anchor_stub_inferred_facts has no cost field.
  • src/v4/test/claim/workflow/pipeline_rejections.dag no longer imports UnknownCost, and workflow_inferred_facts() has no cost field.
• Final sweep checks:
  • import v4.lens.cost in src/v4 → no matches
  • cost: SymbolicCost in src/v4 → no matches
  • InferredFacts { ... } constructors found only in expected locations and all match new shape.

I also ran the v4 compile gate to ensure CI-safety posture is intact:

• target/debug/v2-compiler compile --output-dir /tmp/v4-compile-out --source-root src/v4
• Result: compiled: 85 files emitted, 0 diagnostics

No additional code changes were needed.

  

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: a12d4955 · Trigger: schedule
• Thinking: 96s wall

---

Non-blocking — Strengths

• src/v4/compiler/04_infer.dag Removing SymbolicCost from InferredFacts keeps cost authority in v4.lens.cost instead of carrying a parallel infer-stage fact.

ROADMAP — Verified

• T-12 cost lens authority: src/v4/TASKS.md makes cost/complexity a lens task depending on T-9, so this PR preserves the intended infer-to-lens direction.

✅ No blocking concerns.