docs(lens-framework): correct Lens.read purity invariant per #1319 BLOCKING

[briansrls]

Summary

Fix follow-on for #1319 BLOCKING review (briansrls 2026-04-30T23:00:42Z). My Director-ratified Lens.read purity invariant amendment said "depends only on (Node, Behavior)" — stripping the Dag substrate authority that L-7 / P2 require.

Verification

Live Lens<C> primitive signature:

• Line 25: read: (Dag, Behavior) → Witness<C>
• Line 343: canonical read: (Dag, Behavior) → Witness<C> (matches AnalysisDimension.witness_of at dimensions.dag:74 verbatim)
• Lines 155, 196, 237: all worked instances (Complexity, Tenant-Flow, IFC) DO Dag-based substrate-fact lookup
• Line 310: explicitly cites the per-Behavior input space distinction (re L6 not being a Lens instance)

Reviewer correct: my amendment removed the substrate authority.

Fix

Reframe the invariant correctly:

• Lens.read MUST be a pure function of (Dag, Behavior) inputs
• Function may freely consume substrate facts via Dag (per-op cost from std/algebra.dag, capability sets, security labels)
• MUST NOT depend on external mutable state (no globals, no time, no I/O, no consumer-side caches)
• The Dag IS the substrate authority L-7/P2 require; purity invariant is about external state, not the substrate-fact channel

Memoization key becomes (Dag-identity, Behavior-identity) since both inputs are immutable; runtime memoization is the auto-memoization free consequence in T-Free-Consequences-Demonstration.

Test plan

• Verified Lens.read signature in lens-framework.md vs invariant amendment
• Verified worked-instance Dag-based lookups
• Updated invariant text references the correct (Dag, Behavior) input space

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: d448b9d2 · Trigger: schedule
• Comparison: origin/main @ 5e6b48b4 ... review/pr-1340-d448b9d2 @ d448b9d2
• Thinking: 50s wall

---

Verdict: APPROVE

The diff is a single documentation correction at docs/design-lens-framework.md:417. It narrows the purity invariant correctly: Lens.read may read declared facts through its explicit Dag input, while external mutable state remains forbidden. That aligns with P2/L-7 single-authority boundary discipline and does not introduce a modeling, coding, or testing violation.

[briansrls]

Verification + approval (PM perspective). This fix corrects my original invariant text in PR #1319 — I introduced two errors that the BLOCKING reviewer caught:

1. Wrong input space — I wrote "(Node, Behavior)" but the actual Lens<C>.read signature at design-lens-framework.md:25 is (Dag, Behavior) → Witness<C>. The worked instances at lines 155 / 196 / 237 all do read(dag, behavior) substrate-fact lookups through the Dag context.
2. Ambiguous purity scope — "not external state" could be read as forbidding the substrate-fact channel itself, which would gut the L-7 / P2 substrate authority that the worked instances depend on.

This PR's correction handles both:

• Names (Dag, Behavior) as the declared input pair (matches signature verbatim)
• Explicitly allows substrate-fact reading through Dag (preserves L-7 / P2)
• Explicitly forbids external mutable state with concrete enumeration (globals, time, I/O, consumer-side caches)
• Updates memoization key to (Dag-identity, Behavior-identity) consistent with both inputs being immutable

The auto-memoization-as-free-consequence framing the user requested is preserved — runtime memoization remains an instance of T-Free-Consequences-Demonstration, just keyed correctly.

LGTM from PM side; thanks for the catch + correction.

— sent from deep-wolf-155

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: d448b9d2 · Trigger: schedule
• Thinking: 205s wall

---

Non-blocking — Strengths

• docs/design-lens-framework.md The design/doc change is consistent with L-7 and P2: Dag remains the single substrate authority while external mutable state is excluded from Lens.read.

✅ No blocking concerns; this corrects the prior purity wording without introducing a competing authority.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: d448b9d2 · Trigger: manual
• Conversation: View conversation

---

1. Story of the diff

This PR corrects the lens-framework documentation so the Lens.read purity invariant no longer treats substrate lookups as impurity. The old wording required Lens.read to depend only on a (Node, Behavior) pair; the new wording at docs/design-lens-framework.md:417 says it is a pure function of declared (Dag, Behavior) inputs, which means it may read facts already authored in the DAG but must not depend on external mutable state, I/O, time, globals, registries, or consumer-side caches. That is the load-bearing change: it preserves memoizability while restoring Dag as the single substrate authority for cost, capability, label, and similar facts.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — docs/design-lens-framework.md:417 does not introduce a new substrate type, DAG field, variant, or Rust implementation path; it documents that Dag is the substrate authority for Lens.read and that external mutable state is outside the layer boundary.

1. INVARIANTS.md + modeling-discipline.md.

Compliant — P2 / L-7 single-authority and facts-flow-forward are honored by the line: Lens.read “may freely consume substrate facts reachable through the Dag” but “MUST NOT depend on any external mutable state” at docs/design-lens-framework.md:417. This distinguishes shared reads of the canonical DAG from parallel representations or consumer-owned authority.

1. CODING.md.

N/A — documentation-only diff; no Rust functions, methods, result shapes, helper placement, naming, or mutability surfaces are changed.

1. TESTING.md.

N/A — documentation-only invariant correction; no executable behavior changed, and there is no new implementation surface requiring unit, integration, boundary, or regression tests in this PR.

1. LOCKED DESIGN DECISIONS.

Compliant — the change edits a ratified lens purity statement, but it is explicit rather than silent: docs/design-lens-framework.md:417 says the invariant is “corrected per #1319 BLOCKING review” and narrows the lock to external-state purity while preserving the memoizable-shape commitment.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the deferred work is bounded and named: docs/design-lens-framework.md:417 says memoization implementation is deferred and identifies the R3 T-Free-Consequences-Demonstration lane as the consequence demonstration, rather than leaving a generic TODO or unbounded scaffold.

3. Verdict

APPROVE — The PR fixes the over-restrictive purity wording without creating a second authority for lens facts. The new invariant keeps Lens.read pure relative to declared inputs, allows legitimate DAG-backed substrate reads, and explicitly tracks the deferred memoization implementation.