docs: design interprocedural cost (complexity-gate S3) — binding_id-keyed callee summaries, fail-closed recursion, substrate-gated activation

[briansrls]

Worker attestation

• Title describes the change (not the session id or branch).
• PR body summarises what and why.
• Tests run: docs-only change (one new markdown file); no tests changed — relied on CI.
• No work item issue to close (design doc under the complexity-gate planning lane).
• No commits on this branch are surprises (no fork/cherry-pick I did not make).
• No secrets / credentials / large binaries staged.

Summary

Design-only doc for complexity-gate S3: closing the soundness gap where a call site costs unit_cost() regardless of the callee's body (src/v4/lens/cost.dag:206), so a superlinear helper hides behind every caller as O(1). Follows the merged S1 (#4668/#4669, design-lens-subject-supply.md) and S2 (#4673) rungs; no code lands here.

Key decisions pinned by the doc:

• One fold, one algebra: S3 is an additive lens module composing existing pieces — per-declaration cost_lens summaries keyed by binding_id (Implement brand-identity side-channel phase plan for A3/PD-3: equivalence-first ident channel + honest ident_span gates #4581 callee channel, never name strings), call edges via the canonical Transform-callee accessor, substitution via the existing symbolic_sequential/symbolic_product algebra. The single consult hook in cost.dag's fold is explicitly flagged as an operator-STOP escalation, preferred over a shadow fold.
• Recursion is not an S3 problem (reworked per operator feedback): recursive surface forms lower via CallPattern classification onto the closed iteration primitives (INVARIANTS "Recursive Syntax Is Sugar", DB-9), so a well-formed lowered call graph is acyclic by construction and recursion is priced by the existing Loop treatment. SCC/self-edge fail-closure survives only as an integrity backstop against lowering defects (ClassUnknown → red, never silently green). The earlier draft's "P2" (witness-refined SCC summaries at the lens level) is now an explicitly rejected alternative — it would re-derive at analysis time what the lowering establishes structurally (second-path ban). §3.1 additionally pins the operator's no-steady-state-unknowns rule: the CallPattern taxonomy is closed and exhaustive (same-argument "forever" loops lower to repeat(Forever), a named finite bound — not unknown; mutual recursion via DB-9 cluster facts), so every ClassUnknown over lowered code is a defect or modeling-gap work item, never a tolerated category.
• Substrate-gated activation: nothing implements until the COMPREP callee-dispatch wave admits a call-containing subject; S3 must land no later than the first call-containing roster row, with consult/cycle-backstop/missing-summary perturb reds specified up front.

Test plan

• Docs-only; no tests changed — relied on CI.
• Spot-checked the doc's code anchors: base_cost_for_behavior Transform→unit_cost() at src/v4/lens/cost.dag:206, interim eval_transform_callee_edge at src/v4/compiler/05_eval.dag:1371, CallPattern lowering table at dsl/std/computation.dag:192, iteration-primitive closure at dsl/std/iteration.dag:1.