Wave-4-A — find_witness enumeration and coercion_fold identity-MVP body fill

[briansrls]

Summary

Fills the mechanical find_witness enumeration and multiplicity-resolution control flow, plus the coercion_fold success lift, while keeping unresolved predicate semantics fail-closed. The current preservation predicate is explicitly scaffolded as an exact-structural identity MVP: it accepts only preservation_rule_exact_structural_equality_zip_fold when the predicate algebra and selected candidate both equal the source facts; other preservation rules, including constraint satisfaction, remain fail-closed until their caller-owned predicate algebra lands.

This PR also fixes selected-target zero diagnostics to return no-candidate, carries an auditable coercion homomorphism evidence Node binding source/candidate/find_witness evidence, and cleans stale T-10 comments that previously named std/find_witness as the remaining blocker.

Scope notes

This is a substrate body-fill step, not the final T-9/T-10 Accepted-outcome unlock. solve_constraints still delegates through preservation_rule_constraint_satisfaction, which intentionally remains fail-closed under the current predicate scaffold. General structural zip-fold coercions between distinct source and target Nodes also remain deferred to the modeled structural predicate algebra.

Test plan

• python3 scripts/test_strict_deprose_dag.py: PASS
• python3 scripts/strict_deprose_dag.py --check: PASS
• git diff --check: PASS
• rg -n "import v4\.lens" src/v4/compiler src/v4/std: no matches
• cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely
• cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet: PASS remotely

[briansrls]

Wave-4-A body fill pushed at 88fe2d2.\n\nImplemented in-scope substrate bodies only:\n- std/find_witness.dag: deterministic closed-candidate enumeration, predicate checks across the full set, UniqueOnly/TargetSelection multiplicity resolution, FindWitnessResult and verify_witness Accepted paths.\n- std/constraints.dag: canonical root candidate set, hard-bound UniqueOnly, FindWitnessResult -> CanonicalGrounding lift.\n- std/coercion.dag: TargetSelection find_witness call, FindWitnessResult -> CoercionResult/HomomorphismWitness lift.\n\nVerification run:\n- cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely.\n- python3 scripts/test_strict_deprose_dag.py: PASS.\n- python3 scripts/strict_deprose_dag.py --check: PASS.\n- git diff --check: PASS.\n- rg -n "import v4.lens" src/v4/compiler src/v4/std: no matches.\n\nKnown blocker before ready: AC#4 MVP add Accepted trace cannot be authored honestly against current origin/main because src/v4/compiler/04_infer.dag and 05_emit.dag are still fail-closed scaffolds, and this brief forbids touching compiler/*.dag. Full v4 bootstrap compile also resolved 99 modules then exited 137 in the remote runner; current resolve-posture bridge accepts 124/143 only, so it did not apply to this 137 run.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 9c112387 · Trigger: schedule
• Thinking: 300s wall

---

BLOCKING (3)

Root Cause

• src/v4/std/find_witness.dag PreservationPredicate is only a Symbol selector, so the primitive body becomes a predicate switchboard → make the predicate an evaluable caller-owned carrier or move the checks to the concept homes before generic enumeration/resolution.
• src/v4/std/constraints.dag ConstraintGraph still carries only root and the new body turns that scaffold into accepted canonical evidence → keep rejection until real graph carriers exist or derive the candidate set from actual constraint facts and closedness evidence.
• src/v4/std/find_witness.dag The trusted verification path validates the candidate/predicate pair but not the witness payload it returns → require witness.evidence == candidate or strengthen StructuralPropertyWitness so the candidate is the evidence by construction.

⚠️ The accepted paths are close, but these bodies currently make the generic primitive a semantic switchboard and allow unsound canonical/witness acceptance.

[briansrls]

Merged origin/main into the branch and reconciled the T-9/T-10 shapes. The PR delta is now limited to std/find_witness.dag and std/coercion.dag; std/constraints.dag matches main's closedness-bridge shape and remains fail-closed for root-only ConstraintGraph candidate generation per the blocking review fix.\n\nPost-merge verification:\n- python3 scripts/test_strict_deprose_dag.py: PASS\n- python3 scripts/strict_deprose_dag.py --check: PASS\n- git diff --check: PASS\n- cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely\n- cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet: PASS remotely\n\nReconciliation note: the merged T-9/T-10 TestClaim files are fail-closed receipts: infer still rejects at infer_descent_not_derived before solve_constraints, translate still rejects canonical_grounding_for_node, and emit still rejects target_serialize_source_from_model. Producing an end-to-end Accepted add trace would require changing those merged compiler-stage scaffolds or reintroducing the root-only canonical candidate fabrication rejected in review. This body-fill branch keeps the reviewed fail-closed substrate behavior.\n\n— sent from swift-lark-412

[briansrls]

Verified the dashboard-only cursor review against current head 35784a839. The observations are accurate: preservation_predicate_holds is intentionally the minimal identity/well-formed predicate, accepted_witness_result tags the witness with predicate.preservation_rule, and Exact is currently unreachable for distinct source/target Nodes.

I am not changing code for this review because the artifact itself marks these as non-blocking for Wave-4-A, and the stronger fix would require an evaluable caller-owned predicate carrier or moving predicate algebra semantics into std/constraints.dag / std/coercion.dag. That is a signature/model change outside this body-fill PR, and the earlier blocking review explicitly rejected hard-coding caller-specific predicate semantics inside generic find_witness. This PR therefore keeps the fail-closed, scaffold-bounded identity predicate and avoids fabricating canonical/coercion evidence.

Current verification remains green: CI passed, v4 smoke passed, translate smoke passed, strict-deprose passed, and the PR is mergeable.

— sent from swift-lark-412

[briansrls]

Operator review fixes pushed at a6abe147.

Disposition:

• find_witness preservation predicate now consumes both sides of the exact-structural MVP check: predicate.algebra == source_facts and candidate == source_facts, with all three Nodes still required well-formed.
• resolve_selected_candidate now distinguishes selected-zero from selected-many: zero returns the no-candidate diagnostic; multiple remains ambiguous.
• coercion_fold now preserves an audit path in the HomomorphismWitness.evidence Node by binding source, selected candidate, and the original FindWitnessResult.witness.evidence under named edges.
• Stale T-10 receipt comments no longer describe std/find_witness as the pending blocker; they point to the remaining compiler-stage canonical grounding / target serialization scaffolds.

Verification:

• python3 scripts/test_strict_deprose_dag.py: PASS
• python3 scripts/strict_deprose_dag.py --check: PASS
• git diff --check: PASS
• rg -n "import v4\.lens" src/v4/compiler src/v4/std: no matches
• cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely
• cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet: PASS remotely

— sent from swift-lark-412

[briansrls]

Codex REQUEST_CHANGES verified and fixed at 20db35ff.

The exact-structural equality MVP is now gated by predicate.preservation_rule == preservation_rule_exact_structural_equality_zip_fold before it can accept predicate.algebra == source_facts && candidate == source_facts. That keeps preservation_rule_constraint_satisfaction and any other rule fail-closed until their caller-owned predicate algebra exists, instead of fabricating every rule into plain Node equality.

Verification repeated after the patch:

• python3 scripts/test_strict_deprose_dag.py: PASS
• python3 scripts/strict_deprose_dag.py --check: PASS
• git diff --check: PASS
• rg -n "import v4\.lens" src/v4/compiler src/v4/std: no matches
• cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely
• cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet: PASS remotely

— sent from swift-lark-412

[briansrls]

Verified the cursor REQUEST_CHANGES against current head. The scope mismatch is valid: the current body is an exact-structural identity MVP, not a general structural zip-fold implementation, and preservation_rule_constraint_satisfaction remains intentionally fail-closed.

Addressed at a9570c3fb by:

• adding an explicit yellow dissolution marker on preservation_predicate_holds naming the narrowed identity-MVP scaffold and its structural zip-fold predicate-algebra dissolution point;
• narrowing the PR title to Wave-4-A — find_witness enumeration and coercion_fold identity-MVP body fill;
• replacing the autogenerated PR body with a scope note that says this is not the final T-9/T-10 Accepted-outcome unlock, that constraint satisfaction remains fail-closed, and that distinct-node structural zip-fold coercions remain deferred.

Validation for the code change:

• python3 scripts/test_strict_deprose_dag.py: PASS
• python3 scripts/strict_deprose_dag.py --check: PASS
• git diff --check: PASS

— sent from swift-lark-412

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 35784a83 · Trigger: schedule
• Thinking: 326s wall

---

BLOCKING (1)

Root Cause

• src/v4/compiler/06_translate.dag Target candidate-set root is collapsed into a one-element CandidateSet before find_witness → either materialize the closed inhabitants list before the call or make CandidateSet carry the root plus the canonical enumerator/fold that find_witness consumes.

⚠️ One target-candidate enumeration gap remains in the new body path.

[briansrls]

Verified against current PR head 96c8e922: this is already addressed by the later Option-A + concept-home fix.

find_witness intentionally folds candidates.candidates, but translate no longer supplies the declared-inhabitants root as that flat list. coercion_candidates_from_target_model obtains inhabitants_root and delegates to std/coercion.coercion_candidate_set_from_declared_inhabitants(...). That helper constructs CandidateSet { candidates: declared_inhabitant_candidates(inhabitants_root), ... }, where declared_inhabitant_candidates maps inhabitants_root.children to e.target. So the root’s children are flattened before find_witness consumes the set.

Relevant current-head locations:

• src/v4/std/coercion.dag: declared_inhabitant_candidates maps inhabitants_root.children to candidate targets.
• src/v4/std/coercion.dag: coercion_candidate_set_from_declared_inhabitants stores that flattened list in CandidateSet.candidates.
• src/v4/compiler/06_translate.dag: coercion_candidates_from_target_model calls the coercion concept-home helper rather than passing the root directly.

No code change needed for this stale finding.

— sent from swift-lark-412

[briansrls]

Round-2 candidate-root enumeration blocker verified and fixed at 1273d23b using operator option A.

coercion_candidates_from_target_model now flattens the declared_inhabitants root into the actual closed candidate list before constructing CandidateSet:

• added declared_inhabitant_candidates(inhabitants_root) -> List<Node> using map(inhabitants_root.children, fn(e) { e.target })
• CandidateSet.candidates now receives that flattened list instead of [inhabitants_root]
• updated the translate comment to state that translate performs the flattening before find_witness consumes the candidate list

Also verified the relayed canonical_grounding_candidates inline comment is stale on current head: src/v4/std/constraints.dag still returns outcome_rejected(constraints_not_realized_diagnostic(...)), so it does not accept a root-only candidate set.

Verification:

• python3 scripts/test_strict_deprose_dag.py: PASS
• python3 scripts/strict_deprose_dag.py --check: PASS
• git diff --check: PASS
• rg -n "import v4\.lens" src/v4/compiler src/v4/std: no matches
• cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely
• cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet: PASS remotely

— sent from swift-lark-412

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 1273d23b · Trigger: manual
• Comparison: main @ 2f384004 ... session/swift-lark-412 @ 1273d23b
• Conversation: View conversation

---

1. Story of the diff

This PR fills the Wave-4-A identity-MVP path that was previously mostly scaffolded: find_witness now enumerates candidate nodes, applies a narrowed exact-structural-equality preservation predicate, resolves multiplicity/selection policy, and returns a typed FindWitnessResult rather than leaving the path unrealized (src/v4/std/find_witness.dag:75-234). coercion_fold now consumes that result and can produce an accepted CoercionResult with Identity or Exact quality plus structural evidence derived from the selected witness (src/v4/std/coercion.dag:106-148). translate wires this into the MVP path by flattening declared inhabitant children into the CandidateSet passed to find_witness, while the manual MVP claim is updated to keep the remaining blockers explicit: canonical grounding and target serialization are still fail-closed scaffolds (src/v4/compiler/06_translate.dag:178-193, src/v4/test/claim/manual/mvp1_rust_add_translate.dag:5).

2. Invariant categories

1. LAYER MODEL — Finding

src/v4/compiler/06_translate.dag:178-193 introduces declared_inhabitant_candidates as a compiler-stage helper that reaches into inhabitants_root.children and maps each edge to e.target. That makes the translate stage depend on the storage shape of the target model’s declared-inhabitant root, rather than consuming a declared candidate-set/accessor surface. The PR is directly responsible because it changes the candidate construction from passing the root node as a single candidate to flattening its children in translate.

This violates the layer/boundary rule: a consumer should not reverse-engineer lower-layer Node.children layout to recover a semantic fact. The fix should be to expose this as a canonical target/coercion query or candidate-set construction surface, then have translate consume that surface without knowing that declared inhabitants are currently encoded as child edges.

2. INVARIANTS.md + modeling-discipline.md — Finding

Same concrete issue: src/v4/compiler/06_translate.dag:178-193 violates Boundary Discipline / facts flow through typed query surfaces. The semantic fact “these are the declared inhabitant candidates” now has a local derivation in translate, and future consumers could derive the same fact differently. That creates a parallel authority for candidate enumeration.

The fail-closed parts of the PR are otherwise handled well: preservation_predicate_holds narrows acceptance to well-formed source/predicate/candidate facts and exact structural equality (src/v4/std/find_witness.dag:82-87), while find_witness rejects zero passing candidates, ambiguous candidates, and invalid selected candidates rather than fabricating a witness (src/v4/std/find_witness.dag:196-215). The identity-MVP scaffold is also bounded in-line at src/v4/std/find_witness.dag:75.

3. CODING.md — Compliant

The new implementation is decomposed into small free functions with typed outcomes: passing_candidate_count, only_passing_candidate, selected_candidate_count, resolve_selected_candidate, find_witness, and verify_witness each expose a clear input-to-output contract rather than hiding state in methods (src/v4/std/find_witness.dag:89-234). The new coercion_homomorphism_evidence helper is likewise a narrow data-construction function (src/v4/std/coercion.dag:106-124). The scaffold comment at src/v4/std/find_witness.dag:75 is dense, but it is load-bearing because it names the MVP bound and dissolution trigger.

4. TESTING.md — Finding

This PR changes core behavior from “body scaffold / reject” to “identity witness can be accepted,” but the diff does not add behavior coverage for that new contract. The changed acceptance paths are find_witness at src/v4/std/find_witness.dag:184-220 and coercion_fold at src/v4/std/coercion.dag:133-148.

This should have same-PR .dag TestClaim or generated-harness coverage for the identity MVP contract: exact identity candidate accepts, non-identity candidate rejects, ambiguous passing candidates reject under UniqueOnly, selected-priority/user-selected candidates accept only when the selected candidate also preserves, and verify_witness rejects mismatched property/evidence. This is not a broad “more tests” request; it is a regression surface for the PR’s new fail-closed/accepted behavior.

5. LOCKED DESIGN DECISIONS — N/A

No locked design decision appears to be directly altered by this diff. The PR stays within the existing v4 .dag source surface, does not introduce a seventh type connective or sixth behavior, and keeps remaining translate/emit blockers explicitly fail-closed rather than silently claiming full MVP emission.

6. TRACKED vs UNTRACKED DEBT — Compliant, except for the boundary finding above

The identity-MVP predicate scaffold is tracked: src/v4/std/find_witness.dag:75 states the narrow scope, the exact identity-only behavior, the fail-closed treatment of other preservation rules, and the W-T-10 structural zip-fold dissolution trigger. The manual MVP claim also keeps its remaining blockers named instead of pretending the full compile-to-emit path is complete (src/v4/test/claim/manual/mvp1_rust_add_translate.dag:5).

The untracked piece is the new local candidate-flattening helper in translate; it is not marked as a scaffold and does not name a dissolution path to a canonical candidate query (src/v4/compiler/06_translate.dag:178-193).

2.5. Top-down PM intent review

Compliant with one implementation caveat captured above. The PR’s PM-level intent is consistent with the v4 direction: move find_witness from body scaffold toward the parameterized witness primitive and let coercion_fold consume witness evidence rather than owning a separate coercion decision path. It also preserves honesty about what is still not done by keeping canonical grounding and target serialization blocked in the manual MVP claim (src/v4/test/claim/manual/mvp1_rust_add_translate.dag:5). The PM-level concern is not semantic dilution of the plan; it is the implementation-layer boundary issue where candidate enumeration moved into translate rather than a canonical query surface.

3. Verdict

REQUEST_CHANGES

The PR makes real progress on the identity-MVP witness/coercion path and keeps the narrowed predicate fail-closed, but it also introduces a storage-shape traversal in translate for declared-inhabitant enumeration and adds no behavior coverage for the new accepted witness/coercion paths. Both are directly tied to changed lines and should be corrected before merge.

[briansrls]

Openai-pro REQUEST_CHANGES verified and addressed across d5e292ac and 684ee620.

Boundary fix:

• Moved declared-inhabitant root flattening out of compiler/06_translate.dag and into std/coercion.dag as coercion_candidate_set_from_declared_inhabitants(...).
• translate now consumes that coercion substrate construction surface instead of mapping inhabitants_root.children locally.
• Kept the existing T-10 structural receipt imports visible while routing the actual target-priority wrapping through coercion_fold_with_declared_priority(...).

Coverage fix:

• Added src/v4/test/claim/manual/find_witness_identity_mvp.dag with behavior anchors for identity accept, non-identity reject, other-rule fail-closed, UniqueOnly ambiguity, invalid selected-priority/user-selected rejection, verify_witness property/evidence mismatch rejection, and coercion identity lift.

Verification:

• python3 scripts/test_strict_deprose_dag.py: PASS
• python3 scripts/strict_deprose_dag.py --check: PASS
• git diff --check: PASS
• rg -n "import v4\.lens" src/v4/compiler src/v4/std: no matches
• cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely
• cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet: PASS remotely after restoring the expected structural imports

— sent from swift-lark-412

[briansrls]

CI failure on 684ee620 verified and fixed on current head 625f2e67.

Root cause: full v4 bootstrap compile hit a parse error in the new manual claim file because two data ...: Bool = declarations split before the expression. The syntax fix keeps those expressions on the declaration line.

Post-fix state:

• GitHub fmt: PASS
• GitHub affected: PASS
• GitHub ci: PASS
• GitHub v4: PASS
• PR remains MERGEABLE

I also ran the local-equivalent bootstrap command remotely after the syntax fix; it passed the previous parse point (resolved 107 sources) and then hit the known v4 compile OOM/SIGKILL 137 pattern, not the prior parse error.

— sent from swift-lark-412

[briansrls]

Addressed codex REQUEST_CHANGES from review 15747 in head bd676d4.

Fixes:

• Closedness evidence now stays target-side: std/coercion constructs the candidate-set witness with evidence: inhabitants_root, and 06_translate no longer threads source grounding.node into the target declared-inhabitants closedness receipt.
• Behavior coverage is now asserted: find_witness_identity_mvp imports Equals and adds explicit TestClaim assertions for identity accept, non-identity reject, other-rule fail-closed, UniqueOnly ambiguity, invalid selected/user-selected priority, verify_witness accept/reject cases, and coercion identity lift.

Verification:

• python3 scripts/test_strict_deprose_dag.py: PASS
• python3 scripts/strict_deprose_dag.py --check: PASS
• git diff --check: PASS
• rg -n "import v4.lens" src/v4/compiler src/v4/std: no matches
• cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely
• cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet: PASS remotely

— sent from swift-lark-412

[briansrls]

Verified the claude exploratory observations on bd676d4.

• only_passing_candidate is currently sound only under the existing passing_count == 1 call precondition. I’m leaving it unchanged in this ready head because the observation is non-blocking and tightening it would be follow-up cleanup rather than a requested merge fix.
• The Exact arm in coercion_fold is unreachable under the identity-MVP predicate (candidate == source.node) until W-T-10 widens the structural predicate algebra. That is already bounded by the identity-MVP scaffold/dissolution marker, so I’m not adding a new comment on this ready head.

Current dashboard review summary shows ready=true: 2 distinct approvals, no request-change providers, no active reviews, mergeable=MERGEABLE, checks passing.

— sent from swift-lark-412

[briansrls]

Verified the latest claude approval observations against current PR head 96c8e92.

• coercion_fold still has the forward Exact arm, and it is unreachable under the current identity-MVP predicate because preservation_predicate_holds requires candidate == source_facts. This is non-blocking and already bounded by the W-T-10 dissolution marker; I am not changing the ready head for a comment-only follow-up.
• predicate.algebra == source_facts is likewise identity-MVP-specific. The function-level scaffold explicitly states exact structural equality currently accepts only source-identical Node evidence and other preservation rules fail closed, so the eventual zip-fold lift is the right follow-up rather than another in-PR tweak.

No code change made for these exploratory notes.

— sent from swift-lark-412

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 1273d23b · Trigger: schedule
• Thinking: 338s wall

---

BLOCKING (2)

Root Cause

• src/v4/std/find_witness.dag candidate enumeration is split into count plus sentinel-backed selection → carry zero/one/many in a typed accumulator or return Outcome from the selection fold.
• src/v4/std/coercion.dag declared_inhabitants is still represented as raw Node storage read by the consumer → make the constructor fail-closed on the canonical declared-inhabitants shape or introduce a typed closed-list accessor before producing CandidateSet.

⚠️ Two substrate-level fail-closed/API enforcement gaps remain in the new candidate enumeration path.

[briansrls]

Verified against current PR head 46f65997: this is already addressed. only_passing_candidate now returns Outcome<Node> and folds through the typed PassingCandidateFold coproduct (NoPassingCandidate | OnePassingCandidate | ManyPassingCandidates) rather than seeding with source_facts.

Current behavior:

• zero passing candidates -> Rejected { find_witness_no_candidate_diagnostic(...) }
• one passing candidate -> Accepted { value: only, ... }
• multiple passing candidates -> Rejected { find_witness_ambiguous_candidate_diagnostic(...) }

So the helper no longer has a fabricated source-node fallback and cannot return a node that was not selected from the closed candidate set.

— sent from swift-lark-412

[briansrls]

BLOCKING: coercion_candidate_set_from_declared_inhabitants mints CandidateSet.closedness from an arbitrary inhabitants_root without checking it is a well-formed closed-set carrier, so malformed target models can become trusted candidate sets instead of diagnostics under P2/P3.

[briansrls]

Verified valid and fixed on current PR head 46f65997.

coercion_candidate_set_from_declared_inhabitants now returns Outcome<CoercionCandidateSet> and checks well_formed(n: inhabitants_root) before minting the CandidateSet.closedness witness. Malformed roots now return outcome_rejected(coercion_candidate_set_not_closed_diagnostic(...)) instead of becoming trusted candidate sets. 06_translate.dag was updated to consume that Outcome directly rather than wrapping the constructor result in Accepted.

Verification run for this fix:

• python3 scripts/test_strict_deprose_dag.py: PASS
• python3 scripts/strict_deprose_dag.py --check: PASS
• git diff --check: PASS
• rg -n "import v4\\.lens" src/v4/compiler src/v4/std: no matches
• cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely
• cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet: PASS remotely

— sent from swift-lark-412

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 46f65997 · Trigger: manual
• Comparison: main @ d5d61d2f ... session/swift-lark-412 @ 46f65997
• Conversation: View conversation

---

1. Story of the diff

This PR turns the Wave-4-A identity MVP from “body still rejects” into a real, narrow witness path. translate now reads target selection priority and declared inhabitants from the target model, then delegates candidate construction and coercion to the shared std/coercion surface instead of assembling a candidate set locally (src/v4/compiler/06_translate.dag:186, src/v4/compiler/06_translate.dag:214). std/coercion flattens declared inhabitant edges into a CandidateSet, calls find_witness, and lifts an accepted witness into a CoercionResult with Identity quality only when the chosen candidate is exactly the grounded source node (src/v4/std/coercion.dag:123, src/v4/std/coercion.dag:173, src/v4/std/coercion.dag:177). std/find_witness now enumerates candidates, accepts only the intentionally narrow exact-structural-identity predicate scaffold, enforces multiplicity/selection policy, and adds verify_witness; the new manual TestClaim file anchors identity acceptance, fail-closed non-identity/ambiguity/invalid-selection behavior, witness verification mismatch rejection, and coercion identity lifting (src/v4/std/find_witness.dag:80, src/v4/std/find_witness.dag:194, src/v4/test/claim/manual/find_witness_identity_mvp.dag:258).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — this touches std/ witness/coercion substrate-adjacent surfaces, and the layering direction is right: translate consumes the target model and delegates declared-inhabitant flattening to std/coercion (src/v4/compiler/06_translate.dag:186) and coercion selection to the shared coercion helper (src/v4/compiler/06_translate.dag:214) instead of keeping a parallel compiler-local witness path.

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

Finding — P3 fail-closed / API-level enforcement: src/v4/std/find_witness.dag:217 introduces Rejected { diagnostics: r } => Rejected { diagnostics: r }, but this module’s diagnostic import list includes Accepted, Outcome, and outcome_rejected while omitting Rejected (src/v4/std/find_witness.dag:15–src/v4/std/find_witness.dag:24). That makes the new primary find_witness body depend on an unbound rejected-outcome constructor instead of compiling to a typed fail-closed path. This is especially blocking because std/coercion now delegates through this function, so the identity-MVP coercion path can be made unresolvable by the body fill itself. Add Rejected to the diagnostic import or rewrite the branch through an in-scope rejection constructor.

1. CODING.md.

Compliant — the body fill is decomposed into named helpers (passing_candidate_count, only_passing_candidate, resolve_selected_candidate, accepted_witness_result) rather than one opaque body, and it returns structured Outcome<...> carriers rather than primitive sentinels (src/v4/std/find_witness.dag:93, src/v4/std/find_witness.dag:110, src/v4/std/find_witness.dag:156, src/v4/std/find_witness.dag:173). The scaffold comment at src/v4/std/find_witness.dag:80 is load-bearing because it states the identity-MVP boundary and dissolution target.

1. TESTING.md.

Compliant — the PR adds .dag TestClaim anchors rather than a new Rust harness, and the claims are behavior-shaped: identity accepts, non-identity and other-rule reject, ambiguity rejects, invalid declared/user selections reject, witness property/evidence mismatches reject, and coercion identity accepts (src/v4/test/claim/manual/find_witness_identity_mvp.dag:266, src/v4/test/claim/manual/find_witness_identity_mvp.dag:274, src/v4/test/claim/manual/find_witness_identity_mvp.dag:290, src/v4/test/claim/manual/find_witness_identity_mvp.dag:298, src/v4/test/claim/manual/find_witness_identity_mvp.dag:322, src/v4/test/claim/manual/find_witness_identity_mvp.dag:338).

1. LOCKED DESIGN DECISIONS.

Compliant — the diff preserves the locked derived-homomorphism direction rather than diluting it: translation delegates to coercion/witness surfaces (src/v4/compiler/06_translate.dag:214), and the MVP-1 manual claim honestly says full accepted emit remains blocked on canonical grounding and target serialization scaffolds rather than pretending this PR closes those later facts (src/v4/test/claim/manual/mvp1_rust_add_translate.dag:5).

1. TRACKED vs UNTRACKED DEBT.

Compliant — the intentional narrowed predicate is marked as a scaffold with a concrete dissolution trigger, W-T-10 structural zip-fold predicate algebra, at src/v4/std/find_witness.dag:80. The remaining MVP-1 blockage is also bounded in the status line as canonical grounding plus target serialization scaffolds, not left as an untracked TODO (src/v4/test/claim/manual/mvp1_rust_add_translate.dag:5).

2.5. Top-down PM intent review

Compliant — the highest-level intent is preserved: this PR collapses the previously separate “solve/coercion/witness” work into the parameterized find_witness(facts, candidates, predicate, multiplicity_policy) shape and routes translation through that canonical coercion surface. It does not postpone the must-have identity MVP; it implements the narrow identity behavior while explicitly leaving broader canonical grounding and serialization facts fail-closed (src/v4/std/find_witness.dag:80, src/v4/compiler/06_translate.dag:214, src/v4/test/claim/manual/mvp1_rust_add_translate.dag:5).

3. Verdict

REQUEST_CHANGES. The design direction and test shape are solid, but the new find_witness body uses Rejected without importing it, which is a blocking substrate/std compile-resolution issue on the newly load-bearing path. Fixing that binding should make the PR reviewably clean.

[briansrls]

Addressed the openai-pro REQUEST_CHANGES on head 10f0ca254.

Fix:

• Added Rejected to the v4.std.diagnostic import list in src/v4/std/find_witness.dag, so the Rejected { diagnostics: r } => Rejected { diagnostics: r } branch in find_witness is bound through the same diagnostic Outcome constructor surface as the rest of the module.

Verification:

• python3 scripts/test_strict_deprose_dag.py: PASS
• python3 scripts/strict_deprose_dag.py --check: PASS
• git diff --check: PASS
• rg -n "import v4\.lens" src/v4/compiler src/v4/std: no matches
• cargo test -p v3-compiler --test integration v4_bin_main_dag_smoke_test::v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor -- --exact --quiet: PASS remotely
• cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet: PASS remotely

— sent from swift-lark-412

[briansrls]

Verified the latest claude approval observations against current head 10f0ca254.

• The identity-MVP predicate is still explicitly bounded by the exact-structural-preservation-identity-mvp scaffold and W-T-10 dissolution marker.
• The Exact arm in coercion_fold remains unreachable under the current identity-only predicate and is a non-blocking extension point for the zip-fold predicate lift.
• The two-pass passing_candidate_count / only_passing_candidate structure is intentionally left unchanged on this ready head; the helper now uses PassingCandidateFold + Outcome<Node>, so the prior sentinel correctness issue is gone.
• The manual TestClaim behavior anchors remain aligned with the identity-MVP surface.

No code change made for these non-blocking observations.

— sent from swift-lark-412

[briansrls]

Verified the cursor approval observations on current head f09175773.

• The file-level find_witness-enum scaffold wording is stale-ish now that identity-MVP bodies are present, but the function-level identity-MVP marker is the authoritative scoped debt for this PR. I’m leaving header cleanup for the W-T-10 predicate continuation rather than touching the ready head.
• coercion_candidate_set_from_declared_inhabitants currently gates closedness with well_formed(inhabitants_root) and the older T-9 closedness bridge remains as tracked scaffold debt. That convergence belongs with the named bridge follow-up.
• The two-pass passing_candidate_count / only_passing_candidate structure is redundant but fail-closed; only_passing_candidate now uses PassingCandidateFold + Outcome<Node>.

No code change made for these optional notes. Dashboard currently reports ready=true on f09175773: approvals met, no request-change providers, no active reviews, mergeable clean, checks passing.

— sent from swift-lark-412

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 46f65997 · Trigger: schedule
• Thinking: 426s wall

---

⚠️ No new blocking findings, but the prior declared_inhabitants closed-carrier/API-enforcement concern remains open.

[briansrls]

Verified against current PR head f09175773: the prior declared_inhabitants closed-carrier/API-enforcement concern is already addressed.

Current shape:

• coercion_candidate_set_from_declared_inhabitants(...) -> Outcome<CoercionCandidateSet>
• It checks well_formed(n: inhabitants_root) before constructing CandidateSet.closedness.
• Malformed roots reject via coercion_candidate_set_not_closed_diagnostic(...).
• 06_translate.dag consumes that Outcome directly through the bind_outcome chain; it no longer wraps an unchecked candidate-set constructor result in Accepted.

Dashboard currently reports ready=true on f09175773: approvals met, no request-change providers, no active reviews, mergeable clean, checks passing.

— sent from swift-lark-412