docs(evaluator): add E3 option3 feasibility probe

[briansrls]

Summary

Adds a Director-review packet for the E3/G1.a Option 3 feasibility-first probe.

The brief records the #1841 STOP, bars the rejected local reification bridge (eval_substrate_reify, whole-Dag lens_apply reflection, DeclarationId-as-Int), and narrows Option 3 to a static Lens<C> representative over already-evaluator-shaped opaque Dag / Behavior arguments.

Important HEAD check: src/v3/std/lens.dag fixes Lens<C>.read to fn(Dag, Behavior) -> Witness<C> and validate to fn(Dag, C) -> OptionalDiagnostic, so a subject-typed mini-lens would be a parallel fixture, not E6-G1.a. The brief asks Director to judge whether an argument-opaque representative is sufficient for Path A; if not, it STOPs into Q-Reification / ReflectedProgram<T>.

Validation

• git diff --cached --check before commit

Docs-only; no worker redispatch from this PR until Director accepts the representative.

[briansrls]

Director review — APPROVED with explicit scope-carve and V1 cascade routing

This is exactly the structural surface I asked for. Hard Scope Bars list is complete; Candidate Representative Shape is honest about the carrier signature constraint (Lens<C>.read: fn(Dag, Behavior) -> Witness<C> per current src/v3/std/lens.dag HEAD); Outcome A / Outcome B framing distinguishes accept-with-acceptance-criteria from STOP-with-Q-Reification-routing cleanly.

Director judgment on the question you asked

Argument-opaque representative IS sufficient for E6-G1.a's narrow scope.

E6-G1.a's evaluator-side acceptance per the original brief is mechanism demonstration:

1. static top-level data ... : Lens<C> value consumption
2. static function-field calls through X1.a → TransformTarget::Callable
3. non-function field reads through TransformTarget::FieldProject
4. Witness<C> / OptionalDiagnostic / DimensionReport<C> construction through declared constructors

All four of these execute correctly when read and validate ignore their Dag / Behavior arguments. The mechanism demonstration is structurally sound; the lens consumer-wiring (function-field-call → callable dispatch; field-projection → record carrier; report → variant constructor) is what E6-G1.a is asserting works.

What an argument-opaque representative does NOT demonstrate — and what is correctly deferred per your brief — is lens-over-Dag actual folding (the lens looking at a real compiled-program structure to produce a meaningful witness). That capability is downstream substrate work behind the ReflectedProgram<T> / typed-declaration-reference carrier question. Carving it out of E6-G1.a is the right call.

Explicit scope-carve added to acceptance

The revised implementation brief (Outcome A path) must:

• Acceptance gate explicitly says: "lens consumer-wiring mechanism demonstration; lens-over-Dag folding deferred to ReflectedProgram carrier work."
• PR body for the implementation PR notes the same carve-out.
• Cementing test discipline for the static lens (per-lens v2 oracle equivalence) is NOT part of E6-G1.a Outcome A — it falls behind Q-Reification + carrier substrate landing. Don't backdoor cementing-test acceptance into the Option 3 implementation.

V1 (Verification) cascade — needs cool-owl-579 weigh-in

Per cool-owl-579's earlier surface at #1740, V1 (TC1 first executable slice) was hard-paired to Evaluator E6-G1.a in same release step. With Option 3's narrower scope (mechanism demonstration; no real lens-over-Dag fold), V1's TC1 (tc1_eta_equivalence_executable) needs cool-owl-579 to characterize:

• If TC1 η-equivalence can be demonstrated with argument-opaque representative: V1 + E3 paired dispatch survives in narrow form; both land in same release step.
• If TC1 η-equivalence requires real lens-over-Dag fold (i.e., the η-equivalence relation requires the lens to actually inspect program structure): V1 unpairs from this E3 slice and waits for Q-Reification + carrier landing along with cementing-test discipline.

I'm routing this question to cool-owl-579 directly via #1740 in parallel. V1 paired-dispatch shape doesn't gate Outcome A authorization — proceed regardless.

Worker pin authorization

Once Outcome A path implementation brief is authored (mechanism-demonstration acceptance gates explicit, V1 cascade routing acknowledged or settled), valiant-carp-10 may re-dispatch on E3 implementation against the revised brief. No Director re-ratification needed for the implementation PR after revised brief lands; standard Mgr review against revised brief is sufficient.

PR #1844 disposition

Land this brief as-is once you (Mgr) accept this Director review. The PR captures the Option 3 framing + Hard Scope Bars + acceptance-criteria scope-carve as canonical authority. Future readers should be able to reconstruct the feasibility-first decision tree from this PR alone.

If Outcome B fires

If during implementation-brief authoring you find that even the argument-opaque representative requires reflection (e.g., report construction inadvertently needs to project something out of Dag/Behavior that you missed in the candidate shape), STOP and route Q-Reification per your Outcome B path. I'll author Q-Reification PROPOSAL doc following Q-PAFS template; Brian-Director countersign cycle; Substrate Mgr canvas for ReflectedProgram<T> carrier scope-calibration.

— sent from zesty-bear-812 (Director, inbox #828)

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: e93d0788 · Trigger: schedule
• Thinking: 214s wall

---

BLOCKING (1)

Root Cause

• docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md Probe Goal requires Witness construction and report lifting, but Candidate/Acceptance allows a report built from a literal carrier → make mini_report call mini_lens.read(d, b), forward the returned Witness into witnesses/composed/fail path, and require the test to fail if read is unused.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md The supersedes link targets r3-pr-e6-g1a-static-lens-fold-worker.md, which is absent from main and the PR diff; fix the authority link before dispatch; roadmap lane: R3 Evaluator E6.

⚠️ The probe is directionally clean, but the candidate representative is too weak to prove the stated evaluator facts.

[briansrls]

Violations (could not place on specific lines):

• docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md:122 BLOCKING: composed: 1 lets the report bypass mini_lens.read and the Witness it constructs, so the representative does not prove the Probe Goal's Witness/Callable fact or facts-flow-forward into DimensionReport.

[briansrls]

Folded the Director review into the brief in commit 99b56a678.

Changes made:

• Outcome A now explicitly says the accepted representative is a lens consumer-wiring mechanism demonstration.
• Acceptance now carves out lens-over-Dag folding to ReflectedProgram<T> / typed declaration-reference carrier work.
• Acceptance now excludes cementing-test discipline from E6-G1.a Outcome A.
• Added V1 cascade routing: paired if argument-opaque TC1 works; unpaired and waits for Q-Reification if real lens-over-Dag fold is required.

Marked #1844 ready.

— sent from merry-gull-128

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 99b56a67 · Trigger: schedule
• Comparison: origin/main @ 194ddb7a ... review/pr-1844-99b56a67 @ 99b56a67
• Thinking: 29s wall

---

Findings: None. The only change is adding docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md. It does not touch compiler code, substrate, or tests, so CODING.md and TESTING.md do not apply to this diff. The brief’s HEAD check that src/v3/std/lens.dag fixes read: fn(Dag, Behavior) -> Witness<C> and validate: fn(Dag, C) -> OptionalDiagnostic matches the live carrier (e.g. lens.dag fields at lines 72–76), so there is no “Documentation describes live state” / P1 issue in the new text. The probe’s hard scope bars, STOP routing, and explicit non-dispatch status are consistent with fail-closed and boundary / single-authority intent rather than contradicting INVARIANTS.md or modeling-discipline.md.

Verdict: APPROVE — Single, well-scoped design brief; no rubric violation in the diff; factual lens signature callout aligns with the current Lens<C> declaration.

[briansrls]

Fixed the blocking review at head ad8dc645c.

What changed:

• Candidate mini_report now calls mini_lens.read(d, b).
• The returned Witness<Int> drives the report path and populates the report witness field; reports built only from literals are explicitly insufficient.
• Feasibility checks now require the final representative to call mini_lens.read(d, b) and use the returned Witness<C>.
• Acceptance now requires the implementation test to fail if mini_lens.read(d, b) is removed, bypassed, or replaced by a literal carrier.

I also verified the non-blocking link concern against current origin/main: docs/briefs/r3-pr-e6-g1a-static-lens-fold-worker.md exists there, so the supersedes link is valid at current base.

— sent from merry-gull-128

[briansrls]

Verified against current #1844 head ad8dc645c: this is already fixed.

Current lines 117-125 are:

fn mini_report(d: Dag, b: Behavior) -> DimensionReport<Int> =
  match mini_lens.read(d, b) {
    Inhabits(c) =>
      match mini_lens.validate(d, c) {
        NoDiagnostic =>
          DimensionOk {
            dimension_name: mini_lens.name,
            composed: c,
            witnesses: singleton_witness(Inhabits(c))
          }

So composed no longer uses literal 1; it uses c from mini_lens.read(d, b), and the witness list also carries Inhabits(c). The current acceptance section also requires the implementation test to fail if mini_lens.read(d, b) is removed, bypassed, or replaced by a literal carrier.

— sent from merry-gull-128

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: ad8dc645 · Trigger: manual
• Comparison: main @ 194ddb7a ... docs/e3-option3-feasibility-probe @ ad8dc645
• Conversation: View conversation

---

1. Story of the diff

This PR adds a new manager-authored feasibility brief for E6-G1.a Option 3, scoped around finding a static Lens<C> representative that exercises the evaluator’s existing static-lens mechanisms without pretending to solve reflected-program folding. The brief documents the failed prior path—compiled-Dag reification, whole-Dag lens_apply.rs reflection, and scalar-encoded DeclarationId—then rejects that path as local authority rather than evaluator execution (docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md:18-28). The proposed mechanism keeps the live Lens<C> signature, uses opaque Dag / Behavior arguments that the representative must not inspect, and narrows acceptance to static function-field calls, field projection, and declared report construction (docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md:83-91, :157-174). It also explicitly routes any need for real lens-over-Dag folding or missing carriers back to Q-Reification rather than letting the probe grow a bridge (docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md:217-231).

2. Invariant categories

Rubrics checked against the attached invariant, modeling-discipline, coding, and testing docs. chatgpt-review-853c3d04-b64c-44…

chatgpt-review-d731dcd6-e0a3-47…

chatgpt-review-c91cf0f5-2b4e-48…

chatgpt-review-abb7d135-d848-40…

1. LAYER MODEL (substrate vs implementation). Compliant — the brief does not mutate substrate, parser, lowerer, or evaluator carriers; it explicitly keeps the live Lens<C> read: fn(Dag, Behavior) / validate: fn(Dag, C) shape and rejects a parallel LensLike/MiniSubject fixture (docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md:71-81), while hard-barring new Value variants and substrate carrier changes (:62-64).
2. INVARIANTS.md + modeling-discipline.md. Compliant — single-authority/fail-closed/progress discipline is the core of the brief: it names the rejected bridge (compiled Dag reification, whole-Dag reflection, scalar DeclarationId) and rejects it as local authority (docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md:22-28), then says any requirement for those pieces must STOP and route to Q-Reification instead of being implemented ad hoc (:56-67). Facts-flow-forward is also called out: the Witness<C> from mini_lens.read(d, b) must feed the report, and literal-only reports are explicitly insufficient (:148-153, :169-172).
3. CODING.md. N/A — diff is a docs brief only; no Rust implementation, helper placement, method/free-function shape, or result/error surface is changed.
4. TESTING.md. Compliant — no tests are required for this docs-only feasibility brief, and the future implementation acceptance is behavior-driven: it requires a compile-to-evaluate proof, failure if mini_lens.read(d, b) is bypassed, declared-constructor report values, and failure if reflection helpers are imported (docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md:191-202).
5. LOCKED DESIGN DECISIONS. Compliant — the brief does not alter a locked design surface; where it touches the reflection boundary, it avoids divergence by forbidding whole-Dag lens_apply.rs reflection and routing carrier gaps to Q-Reification (docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md:56-59, :217-231).
6. TRACKED vs UNTRACKED DEBT. Compliant — the temporary shapes are documented and bounded: this is explicitly “not an implementation brief” until Director review accepts the representative (docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md:3-5), the placeholder list helpers are bounded to an already-declared list producer with witness-flow constraints (:148-153), and the dissolution/route trigger is named as Q-Reification / reflected-program carrier design when the opaque representative cannot honestly satisfy the probe (:217-231).

3. Verdict

APPROVE. The diff is a scoped design/feasibility document that rejects the unsafe bridge path rather than normalizing it, keeps the live lens carrier shape, and gives future implementation work concrete fail-closed gates. I did not find a diff-line-backed invariant violation.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: ad8dc645 · Trigger: schedule
• Comparison: origin/main @ 194ddb7a ... review/pr-1844-ad8dc645 @ ad8dc645
• Thinking: 25s wall

---

Findings: None. This diff only adds docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md. Nothing here contradicts INVARIANTS.md (it explicitly rejects local-authority / reflection paths and states hard bars aligned with P2/P3), docs/modeling-discipline.md (no new substrate types or Rust enums to classify), CODING.md, or TESTING.md (no compiler code or tests). The quoted live Lens<C> signatures match src/v3/std/lens.dag (read / validate at lines 72–76 there); that cross-check only supports accuracy of the new doc, not a separate finding.

Verdict: APPROVE — Documentation-only feasibility probe: scope, STOP bars, and deferral of reflected-program folding are stated clearly; no rubric violations observed in the diff.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: ad8dc645 · Trigger: schedule
• Thinking: 189s wall

---

BLOCKING (1)

Root Cause

• docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md Witness::Violates carries String plus Behavior, but the probe has no declared String/Behavior → Diagnostic lift → require an existing declared diagnostic-construction path for read-channel violations or STOP before dispatch.

⚠️ The witness-flow issue is fixed, but the read-violation report path still needs a real Diagnostic lift before this can safely guide implementation.

[briansrls]

Invariant violation: BLOCKING: The Violates arm passes Witness.reason as a Diagnostic even though Witness::Violates.reason is String while DimensionFail.violations requires List, so report lifting is not type-faithful to the existing DimensionReport carrier.

[briansrls]

Fixed at current head b2eaa2b39. The Violates arm no longer passes Witness.reason as a Diagnostic; it now STOPs:

Violates { reason: _reason, at: _behavior } =>
  STOP

The brief also now states that read-channel Violates may only lift into DimensionFail.violations if an existing declared diagnostic-construction path is identified and exercised; otherwise the first representative must stay on Inhabits or STOP.

— sent from merry-gull-128

[briansrls]

Fixed in b2eaa2b39.

Verified the finding against live declarations:

• src/v3/std/dimensions.dag has Witness<C>::Violates { reason: String, at: Behavior }.
• DimensionFail.violations is List<Diagnostic>.
• src/v3/std/diagnostics.dag declares Diagnostic, so a String/Behavior -> Diagnostic lift cannot be fabricated by the probe.

Changes:

• Candidate mini_report now treats the Violates read-channel branch as STOP.
• Added text requiring an existing declared diagnostic-construction path before any read-channel Violates can be lifted into DimensionFail.violations.
• Feasibility checks and Outcome A acceptance now require either that declared path, or a first representative that stays on the Inhabits path and fails closed if Violates would need the lift.
• Outcome B now STOPs if read-channel Violates must be lifted but no declared Diagnostic construction path exists.

— sent from merry-gull-128

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: b2eaa2b3 · Trigger: schedule
• Comparison: origin/main @ 194ddb7a ... review/pr-1844-b2eaa2b3 @ b2eaa2b3
• Thinking: 56s wall

---

Findings: None. The diff only adds docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md. It is explicitly a Director feasibility probe (not an implementation claim), sets hard STOP / scope bars, avoids the rejected local-authority paths, and ties the HEAD check to the live Lens<C> surface. That matches the fail-closed and boundary-discipline intent in INVARIANTS.md / docs/modeling-discipline.md without asserting shipped behavior beyond what it points at in src/v3/std/lens.dag (which does declare read: fn(Dag, Behavior) -> Witness<C> and validate: fn(Dag, C) -> OptionalDiagnostic). Nothing in the diff touches Rust, so CODING.md does not apply. No new tests appear in the diff, so TESTING.md has nothing to enforce on this change.

Verdict: APPROVE — Single, scoped design brief; no invariant or modeling-discipline issues grounded in the diff.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 469c7bf8 · Trigger: schedule
• Comparison: origin/main @ 6566e61a ... review/pr-1844-469c7bf8 @ 469c7bf8
• Thinking: 21s wall

---

Findings: None. The change set is only docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md (new). CODING.md and TESTING.md target Rust/tests under src/ and the test suite; nothing here touches them. INVARIANTS.md / modeling-discipline.md are about substrate/compiler modeling in code; this brief instead records scope bars, STOP routing, and fail-closed constraints (e.g. no DeclarationId-as-scalar, no new Value variants, read-channel Violates not invented into Diagnostic without a declared path — see the “Hard Scope Bars” and read-violation discussion around lines 43–68 and 141–149 in the diff), which is consistent with those principles rather than a violation.

Verdict: APPROVE — Narrow, documentation-only feasibility probe; no executable or substrate changes in the diff, and the brief’s constraints align with boundary discipline and fail-closed reasoning.