v4 D1 — Diff/Path structural-delta vocabulary (operator ratification)

[briansrls]

What this is

Encodes the side-session-ratified B-1 decision: the structural-delta
vocabulary over Node (the Diff type that affected_set consumes,
apply_diff produces, and incremental eval / structural caching key on).
This is a substrate addition to the immutable-header T-1 file, so the PR
is the operator-ratification vehicle (DECISIONS.md Part-5 flow).

Ratified (operator-decided in session)

• Diff = a set of Edits; Edit replaces the subtree at a Path with
  a Node (term-rewriting t[s]p).
• Path = List<EdgeSelector> (ByName/ByPosition, mirroring
  EdgeLabel). Flat & finite — NOT a new recursive type (A1: Node
  stays the sole recursion). This eliminates the "structural edit-script
  ADT" option outright.
• Name is Path (the route), not Position (operator pick — a
  position is a coordinate; a path is how you get there). "position /
  occurrence" (JSON Pointer, RFC 6901) retained only as anchor citation.
• Well-formed Diff = pairwise-independent Paths (term-rewriting
  "parallel positions") ⇒ apply_diff is deterministic-total or
  fail-closed. apply_diff consumer = CLI / test harness / app code.

Encoded in (4 files)

File	Change
std/node.dag	EdgeSelector/Path/Edit/Diff decls + D1 header block (DATA ONLY)
lens/application.dag	subterm_at/apply_diff/predicate I/O contract in header (T-23 fill)
lens/affected_set.dag	cross-ref: Diff is the consumed node.dag D1 type
DECISIONS.md	Part-1 RATIFIED row D1

⚠️ One PROPOSED sub-point for your eye (confirm or redirect)

The session ratified "homed in std/node.dag". On encoding I hit a
forcing constraint and split it, which needs your confirmation:

• Data types (EdgeSelector/Path/Edit/Diff) → std/node.dag ✅ (as
  ratified; B1/Hash precedent — a structural delta over Node is
  substrate-tier).
• Operations (subterm_at/apply_diff → Result<Node,Diagnostic>,
  paths_independent/diff_well_formed) → lens/application.dag, not
  node.dag. Forced, not stylistic: std/diagnostic.dag already
  Consumes std/node.dag (Correction = Suggested(Node)), so a node.dag
  op returning Result<_,Diagnostic> is a substrate cycle. This is
  exactly node.dag's existing "the root declares the structural data +
  named invariant; CONSUMERS evaluate fail-closed" discipline (the
  node_well_formed precedent, node.dag ~L262).

Also corrected vs the initial briefing: the briefing said "owner = T-21"
and "Path is K-1-exempt like the diagnostics renderer." Both wrong —
single-authority puts the type in node.dag (not a lens), and Path
resolution needs only Symbol equality (K-1 grants that) so it is
K-1-clean, no exemption.

Status

Draft. Operator ratifies (confirm the data/op split) + merges per current
manual-merge policy. No code bodies added — node.dag gets inert data
decls; application.dag/affected_set.dag are scaffold (header contracts
only, bodies are T-23/T-21).

[briansrls]

Review metadata

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

---

BLOCKING (2)

Root Cause

• src/v4/std/node.dag D1 added structural-delta sum vocabulary without the required coproduct receipt → add the EdgeSelector classification with the attempted dissolution patterns or named scaffold trigger.
• src/v4/std/node.dag The root-status constraint is driving the index carrier instead of the positional ontology → use a nonnegative index carrier such as Nat/Fin/PositionIndex or explicitly stage that gap with a dissolution trigger.

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

• src/v4/DECISIONS.md The D1 row sits under RATIFIED while still asking for operator confirmation of the data/op split; either mark the split ratified or move that sub-point to a proposed/deferred T-23 note.

⚠️ Two substrate-shape issues should be fixed before this lands.

[briansrls]

Addressed in 7c91f73 — both findings valid, fixed structurally (not patched):

Finding 1 (ByPosition{index:Int} admits negatives). Deleted EdgeSelector/ByPosition entirely. Path = List<Symbol> — each step descends the Named edge keyed by that opaque Symbol. There is no ordinal, so the negative/out-of-range illegal state is structurally impossible, not deferred to path resolution. Positional-connective children (Arrow/Cardinality/Instantiation) are reached by replacing the nearest enclosing Named subtree (the safe over-fire #3157 point 3 explicitly blesses); surgical positional addressing is a future operator-ratified extension — omitted because the consumes-nothing root has no ordinal primitive (no kernel Nat; a recursive Peano = A1 STOP). This aligns the Path layer with node.dag's own no-stored-positional-index design (lines ~221-230) instead of fighting it.

Finding 2 (Diff validity via external diff_well_formed). Dropped the set / pairwise-independence / "parallel positions" framing and paths_independent/diff_well_formed. Diff is now an ORDERED List<Edit> applied as SEQUENTIAL rewrites. Any List<Edit> is a valid rewrite program — no representable illegal state, nothing for an external predicate to recover. A non-resolving Edit ⇒ a fail-closed Diagnostic at apply time (legitimate operational behavior, not a type-level illegal state); apply_diff is a fold, all-or-nothing.

Both changes refine the operator-ratified shape and are flagged in DECISIONS.md D1 (PROPOSED-for-operator-eye) for confirm/redirect. The data/op split and cycle rationale are unchanged.

— sent from valiant-boar-161

[briansrls]

BLOCKING addressed in 485f97e (verified against current HEAD, not stale-dismissed — findings were generated vs pre-fix sha a06a0666):

BLOCKING 1 — "D1 sum vocabulary without coproduct receipt." The EdgeSelector = ByName | ByPosition sum was already deleted in 7c91f738f (Path is now List<Symbol>, a record chain — no sum). But the decision not to have a positional selector is itself a Practice-4 dissolution, and the codebase requires the formal 4-pattern ledger for substrate-shape sum decisions (algebra.dag carries them for FreeMonoid/Ordering). Added that receipt to std/node.dag D1: 🟢 GREEN terminal — (1) fact-placement dissolves it (no D1 consumer needs positional-child addressing; everything factors through the Named step / enclosing-subtree replacement), (2) one-variant ⇒ payload ⇒ List<Symbol>, (3) N/A, (4) dimensional FAILS as a keep-reason. Not a deferred gap.

BLOCKING 2 — "root-status driving the index carrier." Resolved by the same dissolution: there is no index carrier. The receipt documents why none is needed (rather than the suggested Nat/Fin — positional addressing is structurally subsumed by enclosing-Named-subtree replacement, the safe over-fire #3157 point 3 ratifies) and why any future surgical positional form is an explicit operator-ratified substrate extension (the consumes-nothing root has no ordinal primitive; recursive Peano = A1 STOP), never a silent TODO.

Non-blocking — fixed in-PR: the DECISIONS.md D1 row no longer carries a "confirm or redirect" clause inside a RATIFIED row. The two refinements (data/op split; P2 shape change) are now stated as encoded via PR review (the normal channel), not an open fork.

— sent from valiant-boar-161

[briansrls]

Verified against current HEAD (485f97e94) — already resolved, not stale-dismissed:

This inline comment targets src/v4/std/node.dag:476 on pre-fix sha a06a0666, where EdgeSelector = ByName | ByPosition was a live coproduct. Two commits since:

• 7c91f738f deleted the EdgeSelector sum entirely — Path is now List<Symbol> (a record chain, no coproduct).
• 485f97e94 added the Practice-4 dissolution receipt for that decision at node.dag:471-500 — explicit classification: 🟢 GREEN (DISSOLVED-AWAY, terminal) with the four-pattern ledger, exactly the modeling-discipline §4 artifact this finding asks for.

Concrete check: grep -rn 'EdgeSelector|ByPosition' src/v4/ returns a single hit — node.dag:474, which is inside the receipt comment, quoting the dissolved shape to document it. There is no type EdgeSelector declaration anywhere in src/v4/. The line the finding points at (476) is now line 3 of the receipt prose, not a sum declaration.

No further change needed for this item.

— sent from valiant-boar-161

[briansrls]

Verified against current HEAD (485f97e94) — already resolved, not stale-dismissed:

This targets src/v4/std/node.dag:478 on pre-fix sha a06a0666, where ByPosition { index: Int } was a live selector variant (the negative-index-constructible concern — correct on that sha, and identical in substance to codex's earlier P2 Finding 1).

7c91f738f deleted that variant entirely. There is no Int ordinal selector anywhere in the substrate: Path = List<Symbol>, each step a Named-edge key resolved by opaque-Symbol equality. With no ordinal carrier, a negative/out-of-range selector is structurally unrepresentable — the illegal state is gone by construction, not deferred to a checker (the exact INVARIANTS P2 / M9 posture this finding asks for).

Concrete check — grep -rn 'index: *Int|ByPosition\{|type EdgeSelector' src/v4/ returns two hits, both comments:

• node.dag:278 — the pre-existing EdgeLabel doc that argues against a stored Positional { index: Int } (the anti-pattern this file always rejected; unrelated to D1).
• node.dag:474 — inside the D1 Practice-4 receipt, quoting the dissolved shape to document it.

No type EdgeSelector / ByPosition declaration exists. Line 478 on current HEAD is receipt prose, not a sum variant. The non-negativity is now enforced by the type not existing, which is strictly stronger than a Nat/Fin carrier. No further change needed.

— sent from valiant-boar-161

[briansrls]

Thanks for the APPROVE. Editorial nit fixed in the follow-up commit: the D1 header block's lines ~221-230 cross-ref was stale (adding the D1 header block shifted line numbers — that range is now Connective, as you spotted). Re-anchored by construct name plus corrected approximate lines (type EdgeLabel ~284 and its "deliberately NO stored index" rationale ~278) so it's robust to future drift. No substantive change.

— sent from valiant-boar-161

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: aa2bc7d9 · Trigger: schedule
• Thinking: 346s wall

---

BLOCKING (1)

Root Cause

• src/v4/compiler/04_infer.dag B-4 is trying to avoid a fifth InferredFacts field but routes the dependency edge through the type fact instead of naming the resolved Atom/name-reference carrier → state that exact declaration identity survives on the resolved name-reference itself, or add an explicit non-InferredFacts carrier that affected_set consumes.

⚠️ One cross-stage fact-flow contract needs correction before this design contract lands.

[briansrls]

Valid finding — fixed in the latest commit (not rebutted). You're right: resolved_type is the node's type (04_infer.dag:23); many declarations share a type, so it is lossy for binding identity — the use→def fact had no named forward carrier, a real Practice-3/P2 error in the B-4 wording.

Correction: the use→def carrier is the post-resolution opaque Symbol (K-1) on the name-reference Atom, not resolved_type. AUTHORITY is compiler/03_resolve.dag (it owns "identifier binding to declarations"): resolution canonicalizes a use-site Atom's Symbol to be identical to its binder declaration's Symbol, so binding = Symbol equality — the one K-1-granted operation, exactly node.dag's existing name_occurrences pattern, and the "resolved through the namespace" mechanism A1/K-1 already state. 04_infer is preserve-only (must not alter/drop the resolved Symbol; no 5th InferredFacts field — IR-1-safe). affected_set derives the graph by Symbol-equality traversal.

Fixed consistently in four places: 04_infer.dag B-4 block (rewritten), a new 03_resolve.dag B-4 authority note (binding is resolve's job, not infer's — which is exactly why resolved_type was the wrong carrier), affected_set.dag Consumes note, and the DECISIONS.md B-4 row. The fact now has a named, existing carrier with a single authority.

— sent from valiant-boar-161

[briansrls]

Already addressed in e236d8883 — codex reviewed aa2bc7d9 (a merge commit); the fix commit is 2 commits after it (aa2bc7d9c → 1ac902324 WIP → e236d8883). Verified against current HEAD, not stale-dismissed.

codex's requested remedy: "state that exact declaration identity survives on the resolved name-reference itself, or add an explicit non-InferredFacts carrier." The fix takes the first option exactly. Current 04_infer.dag B-4 block:

NAMED CARRIER, not resolved_type: The use→def fact's forward carrier is the post-resolution opaque Symbol (K-1) on the name-reference Atom — NOT resolved_type. AUTHORITY is compiler/03_resolve.dag (binding = Symbol equality; node.dag name_occurrences). 04_infer is preserve-only (no 5th InferredFacts field).

So the declaration identity survives on the resolved name-reference Atom itself (its canonical Symbol, K-1), authored by 03_resolve, preserved (not re-carried) by infer — a named, existing, single-authority carrier, no fifth InferredFacts field, the dependency edge no longer routed through the type fact. Fixed consistently in 04_infer.dag (B-4 block), a new 03_resolve.dag B-4 authority note, affected_set.dag Consumes, and the DECISIONS.md B-4 row. This is the same root cause as the briansrls inline BLOCKING at 04_infer.dag:54, fixed in the same commit.

— sent from valiant-boar-161

[briansrls]

Thanks. The exploratory point (Practice-4 receipts as a growing in-header prose anchor → maybe a sibling RECEIPTS.md / per-file .receipts.dag) is noted as a real watch-item, deliberately not actioned in this PR:

• It is explicitly non-blocking and v4 D1 — Diff/Path structural-delta vocabulary (operator ratification) #3162 is merge-ready — a receipts-relocation refactor here would be scope-creep and reset the approval cycle for zero correctness change.
• More substantively: where Practice-4 receipts live (in-header vs a new sibling file) is a substrate-organization decision under STRUCTURE.md's closed-file-tree invariant — adding RECEIPTS.md is an operator-ratified file addition, not a worker call. Pre-empting it unilaterally would itself violate invariant Add SVG viz, test helpers, and makegen scaffold #1.
• The tradeoff is real both ways: in-header keeps the dissolution argument adjacent to the type it justifies (the reviewer-validates-against-anchor discipline); a sibling file keeps headers contract-focused but splits the receipt from its subject. That's a genuine design fork for the operator, captured for the design ledger — not silently dropped.

Recorded as a design-consideration to route to the operator; no code change here.

— sent from valiant-boar-161

[briansrls]

Valid — fixed (not rebutted). docs/modeling-discipline.md:112 does require five dissolution patterns (Pattern 5 = Parameterized family, explicitly the one Patterns 1–4 won't catch). The D1 receipt recorded only four; added Pattern 5:

5. Parameterized family — FAILS: ByName/ByPosition are not one mechanical F<X> over a separately-declared set (different payload types Symbol/Int + different addressing semantics; they mirror node.dag's genuine 2-variant EdgeLabel discriminant, not an enumerated copy of a declared selector-kind set — contrast the Pattern-5 Homomorphism-per-algebra example). No source set X to project over ⇒ Practice-7 projection N/A. Post-(1), one constructor remains — a one-element family is not a family.

Classification stays 🟢 GREEN (dissolved by Pattern 1) but the ledger is now complete against the 5-pattern bar. This also aligns the D1 receipt with the #3160 operator-ratified node.dag receipts, which already use the 5-pattern form (node.dag:241 etc.) — the in-file precedent I should have matched.

Note (out of scope for this PR, flagging not fixing): std/algebra.dag's FreeMonoid/Ordering receipts appear to be 4-pattern (the older style I mistakenly copied) — a pre-existing inconsistency vs the rubric in already-merged code; surfacing for a separate pass rather than silently absorbing it here.

— sent from valiant-boar-161

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 5f509179 · Trigger: schedule
• Thinking: 340s wall

---

✅ No blocking concerns; the PR resolves the prior substrate issues and keeps the new D1/B-4 contracts aligned with the Node-centered v4 model.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 3763e4d5 · Trigger: schedule
• Thinking: 249s wall

---

Non-blocking — Strengths

• src/v4/std/node.dag The D1 Path/Edit/Diff shape is single-authority substrate data and keeps fail-closed operations out of node.dag to avoid the diagnostic cycle.
• src/v4/extdeps/languages/lean.dag The Lean scaffold is documented, bounded to the PROOF-1 termination target first, and defers Coq as a named future probe.

✅ No blocking concerns; the PR resolves the prior substrate issues and keeps the new v4 D1, B-4, B-5, C5, and PROOF-1 contracts aligned with the thesis.

[briansrls]

Valid (NON-BLOCKING) — fixed for self-consistency. The B-2 work added extdeps/languages/lean.dag + the L-4 row, but I left the PROOF-1 row ending "NO new file (closed-tree invariant)", which a worker reading the table literally sees as contradicting L-4. Reconciled into one story:

PROOF-1's framing (#3158) added NO new file — it was framing-only and explicitly DEFERRED the prover model ("realized when a lean/coq model lands"); that model subsequently lands as extdeps/languages/lean.dag per B-2/L-4 (operator-ratified closed-tree extension — see the L-4 row). No contradiction: framing = no file; the deferred model's later arrival is the L-4 extension.

The PROOF-1 row now cross-references L-4 and states the no-contradiction explicitly, so the decision table has a single coherent narrative. (Re: the exploratory note that the bundle is wider than the "D1" title — correct; #3162 became the v4 design-survey branch carrying D1 + B-4/B-5 + C5-1/2/3 + T-9 + B-2/L-4 as the operator directed continued encoding here; the commits + DECISIONS rows tell that single-branch story.)

— sent from valiant-boar-161

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 8404cddf · Trigger: manual
• Comparison: main @ eabfa71b ... session/valiant-boar-161 @ 8404cddf
• Conversation: View conversation

---

1. Story of the diff

This PR is primarily a v4 design-ratification pass that turns “structural delta over Node” into a named substrate vocabulary and then threads the consequences through the neighboring contracts. The load-bearing move is in src/v4/std/node.dag: Path, Edit, and Diff are declared as data over Node, with Path restricted to List<Symbol>, Edit replacing a subtree with a Node, and Diff as an ordered sequential List<Edit> rather than a set plus a validity predicate (src/v4/std/node.dag:740, src/v4/std/node.dag:749, src/v4/std/node.dag:767). The operation side is intentionally kept out of std/node.dag: subterm_at and apply_diff are specified in lens/application.dag because they return Diagnostic, and putting them in node.dag would create a node ↔ diagnostic dependency cycle (src/v4/lens/application.dag:52–65).

The rest of the diff ratifies the surrounding semantics that make that vocabulary usable: affected-set reads Diff but does not own it (src/v4/lens/affected_set.dag:14–19), resolve/infer establish the node-precise Symbol carrier for use→def identity (src/v4/compiler/03_resolve.dag:11–25, src/v4/compiler/04_infer.dag:49–80), effect granularity is pinned per Arrow/signature rather than ambiently (src/v4/lens/effect.dag:14–31), and emit/testgen get the C5 locality and node-level roundtrip contracts that D1 needs (src/v4/compiler/05_emit.dag:24–48, src/v4/lens/testgen.dag:54–80). Separately, the PR reconciles PROOF-1 by adding the first prover language model, extdeps/languages/lean.dag, as a scoped Lean 4 scaffold for termination proofs, and updates DECISIONS.md, STRUCTURE.md, and TASKS.md to make that extension explicit (src/v4/extdeps/languages/lean.dag:3–27, src/v4/TASKS.md:94–100).

2. Invariant categories

1. LAYER MODEL — Compliant. The diff does touch substrate: D1 data lands in std/node.dag, while diagnostic-returning operations are deliberately moved to lens/application.dag to avoid a substrate cycle (src/v4/std/node.dag:142–150, src/v4/lens/application.dag:52–60). That split preserves the substrate/consumer boundary instead of making node.dag depend back on diagnostics.
2. INVARIANTS.md + modeling-discipline.md — Compliant. The illegal-state surface from a positional selector is dissolved rather than retained: Path is only List<Symbol> (src/v4/std/node.dag:107–111, src/v4/std/node.dag:740–742), ordinal addressing is explicitly rejected because Int admits negative/out-of-range states (src/v4/std/node.dag:112–128), and the prior selector coproduct gets a five-pattern Practice-4 receipt (src/v4/std/node.dag:680–728). Fail-closed is also preserved: unresolved paths become diagnostics in subterm_at/apply_diff, never guesses (src/v4/lens/application.dag:16–24), and Diff is sequential data rather than a predicate-repaired set (src/v4/std/node.dag:129–141, src/v4/std/node.dag:755–769).
3. CODING.md — Compliant. There is no new Rust implementation surface; the .dag operations are specified as named functions over explicit inputs, not methods or hidden-state helpers: subterm_at(root: Node, p: Path) -> Result<Node, Diagnostic> and apply_diff(root: Node, d: Diff) -> Result<Node, Diagnostic> (src/v4/lens/application.dag:16–24). The new Lean target is also data/spec scaffold, not procedural emitter code (src/v4/extdeps/languages/lean.dag:29–44).
4. TESTING.md — N/A. This diff does not add executable Rust behavior or a runnable .dag implementation; it ratifies scaffold contracts. The future runnable surfaces are explicitly named as fill work rather than silently claimed as implemented: Lean is “Status: scaffold — fill per TASKS.md PROOF-1 (T-15)” (src/v4/extdeps/languages/lean.dag:52–57), and the D1 operations are “part of this file’s T-23 fill” (src/v4/lens/application.dag:61–65).
5. LOCKED DESIGN DECISIONS — Compliant. The diff does alter/clarify locked design posture, but does so explicitly in DECISIONS.md: PROOF-1’s prior “no new file” framing is reconciled with the later Lean model landing via L-4 (src/v4/DECISIONS.md:41, src/v4/DECISIONS.md:50), and TASKS is updated to say the prover model now lands as extdeps/languages/lean.dag while PROOF-1 completes when the lens framework composes with it (src/v4/TASKS.md:94–100). I do not see a silent divergence from a locked decision.
6. TRACKED vs UNTRACKED DEBT — Compliant. The new scaffolds are bounded and named. Lean is scoped to Lean 4, termination first, spec-not-Mathlib, with Coq explicitly deferred as a future operator-ratified second-prover probe (src/v4/extdeps/languages/lean.dag:8–13, src/v4/extdeps/languages/lean.dag:20–27, src/v4/extdeps/languages/lean.dag:52–57). Text-level fidelity is marked as an orthogonal future sidecar outside Node and content_hash, not a partial D1/C5 implementation (src/v4/lens/testgen.dag:71–79). I did not find a new TODO/bridge without documentation, bounds, and a dissolution or ratification path.

2.5. Top-down PM intent review

Compliant. From the PM/executive level, this PR preserves the v4 intent rather than diluting it: D1 becomes substrate data over Node, not a lens-private side type (src/v4/std/node.dag:151–155); operations stay in a consumer layer to avoid dependency cycles (src/v4/lens/application.dag:52–60); affected-set minimality is grounded in forward-carried Symbol identity rather than a lossy inferred type (src/v4/compiler/04_infer.dag:52–73); and Lean is added as a declarative language model, not as hand-written prover logic (src/v4/extdeps/languages/lean.dag:29–38). I do not see a must-have target becoming optional, a dissolution goal turning into permanent scaffolding, or hand-written implementation replacing the bootstrap/data-authored direction.

3. Verdict

APPROVE. The PR cleanly ratifies the D1 vocabulary, removes the two obvious illegal-state risks from the earlier shape, and keeps authority split across substrate data, application operations, resolve/infer carriers, and affected-set/effect consumers. No diff-cited blocking or non-blocking findings from me.

Exploratory observations

One seam to watch when T-21/T-23 becomes executable: affected_set says it consumes Diff but “never applies it” (src/v4/lens/affected_set.dag:14–19), while apply_diff is where path failure becomes diagnostic (src/v4/lens/application.dag:19–24). The current design is coherent if callers sequence “apply or validate first, then compute frontier”; when implementation lands, that precondition should be made explicit in the API shape or enforced by the runner so invalid diffs cannot produce authoritative frontier witnesses.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 06ab1967 · Trigger: schedule
• Thinking: 251s wall

---

✅ No blocking concerns in the current diff.