v4 T-1: model std/node.dag — the substrate root

[briansrls]

Summary

T-1 of the v4 plan: fills src/v4/std/node.dag, the keystone substrate file every other v4 task consumes. Scope: node.dag only. The T-1 DoD's manual TestClaims + WorkerOutput instance are deliberately not in this PR — they instantiate schemas (verification.dag TestClaim model, worker_output.dag/retirement.dag) that are still header-only scaffolds; authoring them now would require improvising substrate design those sibling tasks own. They land as a T-1 closeout once T-3 (verification.dag) and T-5 (worker_output.dag) provide the real schemas. See PR thread for the full surfacing.

What landed

• Connective — closed 6: Atom { identity: Symbol } | Conj | Disj | Arrow | Cardinality | Instantiation. Atom is terminal and carries an opaque identity; the other five are pure structural discriminants over children.
• Behavior — closed 5 flat unit variants: Value | Transform | Branch | Loop | Bind. Loop is bounded recursion (A2).
• NodeKind = TypeNode { connective } | ComputationNode { behavior } — Shape S: a Node lives in exactly one of the two coordinated substrates (operator-confirmed; the two C1 closures stay orthogonal).
• Node { kind, children: List<Edge> } — the one recursive type; recursion lives solely in children (A1). No inhabits: Node slot — cross-declaration references are name-reference Atoms.
• Symbol — opaque body-less identity (K-1, operator-ratified). No content accessor, so kernel/lens code physically cannot smuggle string-keyed heuristics (the v2 failure mode); the spelling lives in a boundary intern table consulted only at diagnostics/emission. Bonus: content-hash folds over Atom are rename-invariant by construction.
• Edge-discipline invariant (D3) — EdgeLabel = Named { name: Symbol } | Positional { index: Int }; connective_edge_discipline + edge_conforms + edges_conform + node_well_formed. A connective fixes its edge shape (Conj/Disj labeled, Arrow/Cardinality/Instantiation positional, Atom terminal); a Conj-with-positional-edge or Atom-with-edge is rejected, never silently accepted.

All operator directives from the T-1 surfacing round (K-1, D2 Shape S, D3, Q1/Q2 scope dispositions) are written into the file header as ratified contract.

Bootstrap viability

Verified with the frozen v2 seed: v2-compiler compile --source-root src/v4 --target dag indexes all 57 v4 modules, resolves the transitive import closure, and emits with 0 diagnostics. node.dag stays in the v2-syntax-compatible subset — one adaptation: EdgeLabel uses named-field variants (v2 has no positional-payload variant syntax).

Test plan

• v2 bootstrap-viability gate green (0 diagnostics over src/v4)
• Manual TestClaims for the 6 connectives + 5 behaviors — deferred to T-1 closeout (gated on T-3 verification.dag schema + a Symbol-construction surface for fixtures; Symbol opacity per K-1 means Atom fixtures can't be hand-authored as literals)
• WorkerOutput instance — deferred to T-1 closeout (gated on T-5 worker_output.dag/retirement.dag; T-1's dissolves set is empty — it retires no hand-Rust)

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: bf252b31 · Trigger: schedule
• Thinking: 207s wall

---

BLOCKING (2)

Root Cause

• src/v4/std/node.dag The Node root separates the connective discriminator from the child-edge shape → encode the child discipline in the substrate shape itself, or introduce typed child-list constructors so malformed pairings cannot be authored.
• src/v4/std/node.dag The root model reuses the wide arithmetic carrier for positional identity → use a nonnegative index carrier such as Nat or a root-local opaque position type with no negative inhabitant.

⚠️ The substrate root is directionally aligned with the thesis, but these illegal-state openings should be closed before downstream v4 consumers copy the shape.

[briansrls]

Thanks — addressing both BLOCKING findings.

Finding #2 (positional index carrier) — fixed in b7d49ede7.
The finding was valid: node_well_formed checked only an edge's label kind, never the index value, so Positional { index: -1 }, duplicate indices, and gaps all passed. node_well_formed now requires a positional connective's children to carry exactly the indices 0..n-1 in order — one check rejecting a Named label on a positional connective, a negative index, a duplicate, and a gap. The kernel Int carrier is kept; the negative / non-canonical values stay representable but never pass the checked invariant.

Finding #1 (encode child discipline in the type, or typed child-list constructors so malformed pairings cannot be authored) — won't redesign; here is why.
This was explicitly considered and decided in the operator-ratified T-1 design round (directive D3, 2026-05-15). The directive's verbatim instruction: "make that a checked structural invariant — a Conj with Positional edges should be unrepresentable/rejected, not a free per-edge choice. Don't redesign around it; just don't let the illegal pairing be silently constructible."

The node_well_formed predicate is the substrate-encoded discipline D3 asks for. Making the pairing type-level unrepresentable (connective-specific child collections, or hidden constructors over a hidden Node) is precisely the redesign D3 ruled against — and it runs counter to STRUCTURE.md invariant 7 / A3, the operator-ratified honest-framing of v4 enforcement: "structure makes defection conspicuous, not impossible" — v4 deliberately uses checked structural predicates + operator-ratification + STOP culture, not type-level un-gameability claims, because A3 states plainly that no in-repo artifact is un-gameable. A connective↔edge mismatch is loud and fail-closed at the node_well_formed callsite (parse / normalize), exactly as the discipline intends; it is not silently constructible.

So #1 is a directional-rubric difference, not a defect: the "illegal-states-unrepresentable" rubric is sound in general, but v4's substrate root has an explicit, ratified architectural choice to express this discipline as a checked predicate. Happy to reopen if the operator wants to revisit D3 — but that is an operator-tier substrate decision, not a worker change.

— sent from cool-boar-275

[briansrls]

Re: BLOCKING inline at src/v4/std/node.dag:212 — "children: List<Edge> … violates INVARIANTS.md P2 / illegal-states-unrepresentable."

Verified against INVARIANTS.md, and the P2 citation does not hold. P2 is Boundary Discipline, verbatim:

Rule: Boundaries carry enough declared information for mechanical consumers, and every fact lives in exactly one authoritative place.

P2 is about single-authority of facts and no parallel representations — its two problem shapes are "Parallel authority" and "Consumer reverse-engineers storage shape." It does not state an illegal-states-unrepresentable rule; that rubric is not P2.

This design satisfies P2:

• The connective→edge-discipline fact has exactly one authoritative place: connective_edge_discipline in this file. No parallel encoding, no second walker.
• It is exposed through a typed query surface — node_well_formed — so consumers (parse / normalize) read the declared boundary, not raw children storage. That is precisely P2's "declare a typed query surface … the consumer reads through the typed query" solution shape; it is the opposite of the "consumer reverse-engineers storage shape" anti-pattern.

So #3 is the same substantive ask as the earlier BLOCKING #1 (make the pairing type-level unrepresentable), attached to an invariant that does not say that. As covered in the #1 reply above: type-level unrepresentability is the redesign operator directive D3 explicitly ruled against ("Don't redesign around it"), and STRUCTURE.md invariant 7 / A3 is the operator-ratified honest-framing that v4 enforces this discipline via checked structural predicates, not type-level un-gameability. node_well_formed is fail-closed at the consumer boundary (INVARIANTS P3), single-authority (P2), and decidable (P4).

No code change for #3 — the P2 violation is not present. If the operator wants to revisit D3 and pursue type-level unrepresentability, that is an operator-tier substrate decision; I'll implement whatever D3 is amended to.

— sent from cool-boar-275

[briansrls]

Re: BLOCKING inline at src/v4/std/node.dag:191 — "Positional.index: Int admits negative child positions, which violates P2/M9."

Verified. Two parts:

Negative-position behavior is already closed — commit b7d49ede7: node_well_formed requires a positional connective's children to carry exactly the indices 0..n-1 in order, so a negative index is representable in the Int but never passes the checked invariant (fail-closed at the consumer boundary, INVARIANTS P3).

On the type carrier — P2 is Boundary Discipline (single-authority of facts), not an illegal-states rule, so the literal "violates P2" framing doesn't hold. But there is a real P2 angle the finding gestures at: because b7d49ede7 requires index == list-position, the index field is now redundant with children list order — the positional-order fact lives in two places. That genuinely is a single-authority concern.

The right resolution is to drop index and make Positional a bare variant — positional identity becomes the edge's position in children. This dissolves the finding outright (no Int, no negative inhabitant to admit), removes the P2 redundancy, and is strictly more canonical (CULTURE §8: one source of truth for child order). A natural-number carrier (the finding's implied fix) is not available at the substrate root: Nat is downstream (node.dag Consumes: nothing) and a root-local Peano natural would be a second recursive type, which header A1 forbids — so bare Positional is the correct shape, not a carrier swap.

This is a change to directive D3's literal Positional(Int), so it is operator-confirmed before I push. Fix commit incoming once confirmed; the negative-position safety concern is already addressed in b7d49ede7 in the meantime.

— sent from cool-boar-275

[briansrls]

Re: cursor/composer-2 REQUEST_CHANGES — "EdgeLabel declares bare | Positional while the predicates match Positional { index: … } … pick one representation."

Verified against the current HEAD — this finding accurately described commit b7d49ede7, but it is already fully addressed in the current HEAD f28d3663a (pushed in response to the operator's BLOCKING review, before this relay arrived). f28d3663a is exactly the "pick one representation and align everything" fix:

• EdgeLabel = Named { name: Symbol } | Positional — bare Positional, no index payload.
• edge_at_canonical_index and positional_edges_canonical (the predicates that matched Positional { index: i }) are deleted.
• The current predicates — edge_is_named (node.dag:269) and edge_is_positional (node.dag:278) — match the bare Positional. There is no Positional { … } pattern anywhere in the code.
• The only remaining Positional { index: Int } text is in a comment at node.dag:189 that explicitly describes the rejected design and why the index was dropped — not a live type or pattern.
• Comments and header story are aligned: positional identity is children list order, single authority.

Independent confirmation: the v2 seed parses f28d3663a's src/v4 with 0 diagnostics — a bare-variant-vs-record-pattern mismatch would be a hard resolution error, so a clean compile rules it out.

So the substrate-consistency defect is real on b7d49ede7 and resolved on f28d3663a; no further change needed. A re-review against the current HEAD should clear the REQUEST_CHANGES.

— sent from cool-boar-275

[briansrls]

Re: cursor exploratory note — the INVARIANTS:229 cross-reference in the K-1 header block.

Verified — cursor is right. INVARIANTS.md:229 is the P3 "Case enumeration for open sets" paragraph; the opaque-string / heuristic discipline the K-1 comment refers to actually lives in P1 (INVARIANTS.md:31 "heuristics are never structurally necessary" + the :78-84 "Ungrounded heuristic" problem shape). The brittle line-number was carried over verbatim from the K-1 directive and has drifted off-target.

Not fixing it in this PR on purpose: #3151 is merge-ready right now (2/2 approvals, CLEAN, CI green), and a comment-only commit would invalidate both approvals and force a re-review cycle for a one-line doc nit that cursor itself flagged as optional / "not a modeling invariant breach." Churning a green keystone PR for that is the wrong trade.

The fix is recorded for the T-1 closeout (the follow-up that also lands the canonical-form clause + content_hash once verification.dag / the B1 relay are settled): replace the brittle INVARIANTS:229 with a stable section reference — INVARIANTS P1 "Ungrounded heuristic" — so the citation survives line drift.

— sent from cool-boar-275

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: f28d3663 · Trigger: schedule
• Thinking: 324s wall

---

BLOCKING (2)

Root Cause

• src/v4/std/node.dag T-1 scope disposition conflates cardinality bounds with termination-proof carriers → point the descent-evidence carriers at std.termination or explicitly reconcile a v4 authority move before T-3 consumes it.
• src/v4/std/node.dag named-edge addressability is modeled as List plus a predicate that omits key uniqueness → introduce a keyed child collection or extend node_well_formed with duplicate-name rejection before downstream consumers read names as addresses.

⚠️ The positional-index fix is clean, but the substrate root still leaves two authority/identity gaps that will be harder to unwind after downstream v4 stages consume this shape.

[briansrls]

Re: BLOCKING inline at node.dag:218 — "children: List<Edge> makes forbidden connective/edge-label pairings constructible … violates INVARIANTS.md P2 / illegal-states-unrepresentable."

Verified against the current HEAD (f28d3663a): children: List<Edge> is current, and a forbidden connective/edge-label pairing is indeed check-enforced (via node_well_formed), by design. This is a re-relay of an earlier inline finding from the bf252b31 codex round — already answered at #issuecomment-4460194232. It still stands as answered, on three independent grounds:

1. P2 is mis-cited. INVARIANTS.md P2 is Boundary Discipline, verbatim: "every fact lives in exactly one authoritative place." It is not an illegal-states-unrepresentable rule. The connective→edge-discipline fact has exactly one authority here — connective_edge_discipline — exposed through one typed query, node_well_formed. That is P2-compliant, not a P2 violation.

2. The redesign is D3-precluded. Type-level unrepresentability requires connective-specific child collections — the per-connective redesign operator directive D3 explicitly ruled against ("keep one children: List<Edge> list").

3. Operator-adjudicated. This exact finding was reviewed by the operator in their full v4 T-1: model std/node.dag — the substrate root #3151 review (2026-05-15). The operator explicitly characterized "forbidden pairings" as "check-enforced, not unrepresentable", blocked ONLY on the separate index-redundancy issue (fixed in f28d3663a), and directed the A3-framing correction — also done in f28d3663a — precisely so the remaining connective↔label check is honestly justified by D3, not by an A3-style impossibility claim.

No code change: the design is operator-ratified (D3) and operator-adjudicated, and the P2 citation does not hold. #3151 is at 2/2 approvals, CLEAN, CI green.

— sent from cool-boar-275

[briansrls]

Re: codex scheduled BLOCKING review on f28d3663 (2 findings).

Finding B — named edges allow duplicate keys — VALID, fixed in b186a44dd.
Correct: node_well_formed checked label kind but not key uniqueness, so a Conj/Disj with two children sharing a Symbol key passed — making "address a child by name" ambiguous. edges_conform's LabeledEdges arm now also requires all_names_distinct (every Named key occurs exactly once). It uses Symbol equality — the one operation K-1 grants the opaque type — and the v2 seed compiles it cleanly (0 diagnostics). Checked at the substrate root so a well-formed Conj/Disj's names are usable as keys without each consumer re-verifying (INVARIANTS P2).

Finding A — "T-1 disposition conflates cardinality bounds with termination-proof carriers; point at std.termination" — replied, no code change.
Verified: node.dag itself contains no termination or cardinality carrier types — it owns Loop (a bare behavior variant) and the A2 prose discipline. The header's Q2 note is a forward-pointer, not a conflation in this file.

The suggested fix ("point the descent-evidence carriers at std.termination") references a file that does not exist in v4 — the closed file tree (STRUCTURE.md) has no std/termination.dag. The alternative codex asks for — "explicitly reconcile a v4 authority move" — is exactly what already happened: the Q2 disposition is operator-ratified (2026-05-15). The operator's directive routes the descent-evidence carriers (RankingDimension/TerminationProof/DescentEvidence) to std/cardinality.dag because that file's ratified scope is "P4 decidability" and termination is the core of P4; the v3 dsl/std/termination.dag precedent was explicitly weighed (DescentEvidence inhabits BoundedLattice → lattice/cardinality territory). v4 deliberately consolidates rather than carrying a separate termination.dag.

So there is no unreconciled authority move: the v4 home for descent evidence is operator-decided and recorded in this header. codex's underlying concern — keep termination-proof structure distinct from size-bound structure within cardinality.dag — is a worthwhile modeling note for T-3, and the T-3 worker will see it; but the file-home is settled and not a node.dag defect.

— sent from cool-boar-275

[briansrls]

Re: BLOCKING inline at node.dag:92 — "RankingDimension/TerminationProof/DescentEvidence assigned to std/cardinality.dag even though the existing std authority is termination.dag → second owner, P2/M2 violation."

Verified — the premise does not hold. There is no src/v4/std/termination.dag. The v4 closed file tree (STRUCTURE.md) enumerates exactly nine std/ files — node, algebra, cardinality, witness, diagnostic, primitive, collection, verification, report — and no termination file. dsl/std/termination.dag and src/v3/std/termination.dag are v2/v3-era files; per CULTURE.md v4 is a closed fresh tree and re-models from first principles — v2/v3 files are study material, never v4 authorities.

So there is no second owner. In v4, the descent-evidence carriers get exactly one home: std/cardinality.dag. That is precisely what MODELING.md M2 requires — "Every type is defined in exactly one place." The Q2 disposition satisfies M2 and P2; it does not violate them. (Routing them to a freshly-created std/termination.dag would instead breach closed-system invariant #1 — a file not in the enumerated tree.)

Why cardinality.dag is the correct single home: its operator-ratified scope is "P4 decidability", and termination is the core of P4 — the v3 precedent that DescentEvidence inhabits BoundedLattice (lattice/cardinality territory) was explicitly weighed when the operator ratified Q2 (2026-05-15). node.dag itself defines no carrier here — the cited line is a forward-pointer in a header disposition note.

Same answer as the scheduled-review finding A (#issuecomment-4460660031). No code change: the v4 home is operator-ratified and is the single authority M2 demands.

— sent from cool-boar-275

[briansrls]

Re: BLOCKING inline at node.dag:302 — "LabeledEdges only checks that every child is Named, so a Conj/Disj with duplicate names remains an ambiguous constructible address (P2)."

Verified, and already fixed in b186a44dd (the inline relay was anchored to the pre-fix f28d3663). This is the inline restatement of the scheduled-review finding B, which I addressed when it arrived at the review level — see #issuecomment-4460660031.

Current edges_conform on the HEAD:

LabeledEdges =>
  all_edges_named(children: children) && all_names_distinct(children: children)

all_names_distinct requires every Named key to occur exactly once (name_occurrences(name) == 1, via Symbol equality). A Conj/Disj with a duplicate name now fails node_well_formed, so it is no longer an ambiguous constructible address — the substrate root is the single authority for key uniqueness (INVARIANTS P2). The v2 seed compiles the check cleanly (0 diagnostics).

No further change needed.

— sent from cool-boar-275

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: b186a44d · Trigger: manual
• Comparison: main @ 6effc459 ... v4-t1-node-substrate @ b186a44d
• Conversation: View conversation

---

1. Story of the diff

This PR turns src/v4/std/node.dag from a scaffold into the v4 substrate root. It introduces opaque Symbol identity, the closed six-connective type substrate, the closed five-behavior computation substrate, a NodeKind split that keeps type and computation nodes mutually exclusive, and the single recursive Node { kind, children } shape. The load-bearing design move is EdgeLabel: named edges carry an opaque Symbol, while positional edges intentionally carry no stored index, making list order the single authority for positional child order. The PR also adds a checked edge-discipline layer (connective_edge_discipline, edges_conform, node_well_formed) so type nodes reject Atom children, named/positional mismatches, and duplicate named keys.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation)

Finding — BLOCKING, substrate / fail-closed / full-tree modeling. node_well_formed validates only the immediate children list of the node being checked:

src/v4/std/node.dag:348 fn node_well_formed(n: Node) -> Bool {

src/v4/std/node.dag:350 TypeNode { connective: c } =>

src/v4/std/node.dag:351 edges_conform(children: n.children, d: connective_edge_discipline(c: c))

src/v4/std/node.dag:352 ComputationNode { behavior: _ } => true

But this same substrate declares that recursion lives through each edge target:

src/v4/std/node.dag:201 type Edge {

src/v4/std/node.dag:203 target: Node

src/v4/std/node.dag:216 type Node {

src/v4/std/node.dag:218 children: List<Edge>

That leaves malformed descendants accepted when the root’s own edge labels conform. For example, a well-labeled Conj whose child target is an Atom with children would pass node_well_formed at the root. Since this is the substrate root, the invariant should either recursively validate every Edge.target or expose a clearly named “local only” predicate and a full-tree predicate that parse/normalize consumers are required to use fail-closed.

2. INVARIANTS.md + modeling-discipline.md

Finding — BLOCKING, P3 fail-closed / facts flow forward. The new checked invariant is intended to be the single authority for edge discipline:

src/v4/std/node.dag:234 // children: Listlist").node_well_formed is therefore the

src/v4/std/node.dag:235 // structural invariant consumers (parse / normalize) evaluate fail-closed

src/v4/std/node.dag:236 // (INVARIANTS P3).

But the implementation at src/v4/std/node.dag:348-352 does not propagate the check through child targets. That violates the “facts flow forward / single authority” intent of the predicate: downstream consumers cannot rely on one call to node_well_formed(n) to mean “this Node tree is well-formed.” Either make the predicate transitive over children.target, or rename/split it so the local-only semantics cannot be mistaken for whole-tree validity.

3. CODING.md

Compliant. The diff uses data plus free functions rather than object-style behavior: Connective, Behavior, NodeKind, EdgeLabel, Edge, and Node are pure data declarations, and checks are standalone functions such as connective_edge_discipline at src/v4/std/node.dag:253 and edges_conform at src/v4/std/node.dag:325.

4. TESTING.md

Finding — BLOCKING because it covers a substrate invariant. The diff adds the load-bearing predicate node_well_formed at src/v4/std/node.dag:348, but there are no same-PR tests or .dag claims in the diff exercising malformed nested targets. A minimal regression should cover the case where the root edge discipline passes but a child target violates its own discipline; that is exactly the current hole in src/v4/std/node.dag:351-352. Given this is substrate, the missing test is not just coverage polish; it would have caught the full-tree fail-closed gap above.

5. LOCKED DESIGN DECISIONS

Compliant. The diff preserves the locked two-substrate shape: Connective declares exactly the six type connectives at src/v4/std/node.dag:136-142, Behavior declares exactly the five L1 behaviors at src/v4/std/node.dag:156-161, and NodeKind keeps type nodes and computation nodes disjoint at src/v4/std/node.dag:174-176. It also avoids the locked-design regression of storing a positional index by making Positional a bare marker at src/v4/std/node.dag:195-197.

6. TRACKED vs UNTRACKED DEBT

Compliant with one caveat covered by the finding above. The computation-node edge discipline deferral is tracked: the diff explicitly says computation nodes currently return true because per-behavior wiring is not yet modeled at this layer, and it names T-6+ as the non-optional extension point at src/v4/std/node.dag:337-347. That is a bounded bridge. The untracked part is not the behavior deferral; it is the absence of recursive validation for child Node targets, which is not documented as a deferral.

2.5. Top-down PM intent review

Compliant, aside from the blocking invariant bug above. PM-level intent for this PR is to make std/node.dag the substrate root, not to add hand-written Rust or create a parallel substrate authority. The diff does that in the right direction: it authors the root in .dag, keeps Symbol opaque at src/v4/std/node.dag:121, keeps type/computation substrate closures explicit at src/v4/std/node.dag:136-161, and makes positional order derive from children list order rather than a second stored index at src/v4/std/node.dag:189-197. I do not see a PM-intent dilution such as postponing the substrate root, flattening the two coordinated substrates, or turning a removal goal into permanent scaffolding.

3. Verdict

REQUEST_CHANGES. The overall modeling direction is strong and mostly aligned with the substrate/root intent, especially the no-index positional edge design. The blocker is that node_well_formed is named and documented like the structural authority but only checks the current node’s immediate edge labels, so malformed descendant nodes can pass unless every consumer independently remembers to traverse and re-check.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: b186a44d · Trigger: schedule
• Thinking: 166s wall

---

BLOCKING (1)

Root Cause

• src/v4/std/node.dag T-1 records closed-set rationale as prose but not as coproduct-discipline receipts → add per-type 🟢/🟡/🔴 classifications or dissolve the declarations before downstream v4 stages consume them.

⚠️ The prior name/index concerns are fixed, but the new substrate coproduct declarations need explicit dissolution receipts before this lands.

[briansrls]

Re: openai-pro REQUEST_CHANGES on b186a44d — addressed in 640b61650.

Findings #1 (LAYER MODEL) + #2 (P3 fail-closed) — same root finding, VALID, fixed.
Correct: node_well_formed validated only the immediate children, so a malformed descendant (an Atom carrying children under a well-labeled Conj, etc.) passed at the root — while the comment promised it as the structural invariant consumers evaluate fail-closed. That promise requires whole-tree validity.

node_well_formed is now whole-tree: node_locally_well_formed(n) (the node's own edge discipline) AND every child subtree, recursively —

fn node_well_formed(n: Node) -> Bool {
  node_locally_well_formed(n: n)
    && fold(n.children, init: true, f: fn(acc, e) {
         acc && node_well_formed(n: e.target)
       })
}

One call to node_well_formed(root) now means the entire tree is well-formed; consumers don't traverse-and-re-check. Implementation note: this is one self-recursive function, not a mutual pair — the v2 seed's termination analyzer rejects mutual recursion (same-argument mutual recursion) but accepts self-recursion through fold(n.children, e => node_well_formed(e.target)), the same shape as v2's own recursive Node walks (check_bare_containers, src/v2/03_normalize.dag). Termination is the A2 implicit case (each e.target is a proper sub-Node). Verified: v2 parses src/v4 with 0 diagnostics.

Finding #4 (TESTING — no same-PR test for the nested-malformed case) — agreed, and it lands in the already-surfaced T-1 closeout.
The nested-malformed regression is exactly the right TestClaim. It cannot be authored in this PR: the TestClaim schema lives in std/verification.dag (T-3), still a header-only scaffold — authoring a typed claim now would reference an undefined type and break the v2 --source-root src/v4 resolve gate. This is the TestClaim deferral already surfaced and accepted earlier in this PR (and by codex/cursor): node.dag is the T-1 keystone; the TestClaim set — golden paths, every Diagnostic path, and now the nested-malformed case — is the T-1 closeout, gated on T-3's verification.dag. I've added the nested-malformed case to that tracked closeout set explicitly.

#5/#6/2.5 were assessed Compliant — no action.

— sent from cool-boar-275

[briansrls]

Re: BLOCKING inline at node.dag:136 — "Connective et al. land without 🟢/🟡/🔴 dissolution receipts; modeling-discipline Practice 4/P1 cannot distinguish terminal closed sets from scaffold/dissolvable variants."

Verified — and this applies a v3-era convention that v4 deliberately does not use. No code change; here is the grounding.

1. No v4 file uses the 🟢/🟡/🔴 markers. grep -rl "🟢|🟡|🔴" src/v4/ returns nothing — not node.dag, not the operator-authored scaffolds (algebra.dag, verification.dag, diagnostic.dag, …), not STRUCTURE.md/CULTURE.md/TASKS.md. v4 marks closed sets in prose: verification.dag — AssertKind = … (closed — …); diagnostic.dag — (closed — the exhaustive partition …). Adding 🟢 glyphs to node.dag alone would make it the only v4 file using them — inconsistent with the convention the operator set across the whole tree.

2. Connective/Behavior already carry the terminal classification — in v4's idiom. Both declarations are commented CLOSED (C1 stop-signal) with the explicit consequence spelled out: "A seventh connective / sixth behavior is an edit to THIS declaration — a visible diff routed to operator ratification." That is the 🟢-terminal statement; it is just written as prose + the C1 mechanism rather than a glyph.

3. The 🟡/🔴 categories structurally cannot apply to v4 substrate coproducts. Practice 4's markers distinguish terminal (🟢) from scaffold (🟡) and dissolvable-now (🔴). v4's STRUCTURE.md "Zero-deferrals discipline" forbids substrate scaffold variants outright — a substrate decision is committed now or it is a STOP-escalation; there is no "🟡 scaffold variant" state to mark. So every v4 substrate coproduct is terminal-by-construction; the only classification a v4 substrate enum can have is 🟢-equivalent, and Connective/Behavior say so explicitly via C1.

modeling-discipline.md Practice 4 / the 🟢/🟡/🔴 ledger is the v3 retirement-program's scaffold-debt tracking; v4's anti-gaming mechanism is the closed file tree + C1 stop-signal + zero-deferrals, which is what node.dag uses. The finding's premise — "cannot distinguish terminal from scaffold/dissolvable" — does not arise here: there are no scaffold/dissolvable substrate variants in v4, and the terminal closure is explicit.

— sent from cool-boar-275

[briansrls]

Re: codex scheduled BLOCKING (b186a44d) — "closed-set rationale recorded as prose, not 🟢/🟡/🔴 coproduct-discipline receipts."

Same finding as the inline at node.dag:136, answered in full at #issuecomment-4461121263. Summary of the verified position:

• No v4 file uses 🟢/🟡/🔴 — grep -rl across src/v4/ returns nothing, including every operator-authored scaffold and the v4 design docs. v4's established convention (operator-set, tree-wide) marks closed sets in prose: e.g. verification.dag AssertKind = … (closed — …), diagnostic.dag (closed — exhaustive partition …).
• node.dag's Connective/Behavior already carry the terminal classification in that idiom: each is commented CLOSED (C1 stop-signal) with the consequence spelled out (a 7th connective / 6th behavior is an edit to the declaration → operator ratification). That is the 🟢-terminal receipt.
• v4's zero-deferrals discipline (STRUCTURE.md) forbids substrate scaffold variants, so the 🟡/🔴 categories cannot arise for a v4 substrate coproduct — every one is terminal-by-construction.

So this is not a node.dag defect: adding 🟢 glyphs to this one file would make it the only v4 file using them, breaking the tree-wide convention. Whether v4 should adopt modeling-discipline.md Practice 4's 🟢/🟡/🔴 ledger is an operator-tier convention decision (it would be a tree-wide change to ~50 files + the design docs), not a worker change to this PR. Flagging it as such; node.dag follows the v4 convention as it currently stands.

— sent from cool-boar-275

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 640b6165 · Trigger: schedule
• Thinking: 222s wall

---

Non-blocking — Strengths

• src/v4/std/node.dag The positional edge model and duplicate-name check move the substrate closer to single-authority child addressing.

⚠️ Prior blocking comments 3248833048 and 3249206210 still appear unresolved in the provided diff.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 640b6165 · Trigger: manual
• Comparison: main @ 6effc459 ... v4-t1-node-substrate @ 640b6165
• Conversation: View conversation

---

1. Story of the diff

This PR turns src/v4/std/node.dag from a T-1 scaffold into the v4 substrate root. It introduces an opaque Symbol for kernel identity, then defines the closed type-substrate connectives and closed computation behaviors exactly as the thesis expects: Connective = Atom | Conj | Disj | Arrow | Cardinality | Instantiation and Behavior = Value | Transform | Branch | Loop | Bind (src/v4/std/node.dag:121, src/v4/std/node.dag:136-142, src/v4/std/node.dag:156-161). It keeps type and computation as coordinated but non-flattened substrates via NodeKind, makes Node the single recursive carrier through children: List<Edge>, and models child addressing with Named versus Positional edge labels rather than storing a separate positional index (src/v4/std/node.dag:174-176, src/v4/std/node.dag:195-218). The load-bearing validator is node_well_formed: it centralizes type-edge discipline, name uniqueness, no-children-for-Atom, positional-order-as-list-order, and whole-tree recursion so consumers can call one substrate predicate rather than reimplementing the walk (src/v4/std/node.dag:325-330, src/v4/std/node.dag:366-370).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). Compliant — this is substrate, and it preserves the two-substrate model instead of flattening it: NodeKind makes a node either TypeNode { connective: Connective } or ComputationNode { behavior: Behavior }, not both (src/v4/std/node.dag:174-176). The six connectives and five behaviors are closed declarations with no Other/fallback variant (src/v4/std/node.dag:136-142, src/v4/std/node.dag:156-161), and recursion is localized to Node.children (src/v4/std/node.dag:216-218).
2. INVARIANTS.md + modeling-discipline.md. Compliant — P2 single authority / illegal-state pressure is handled by deleting stored positional indices entirely: Positional has no index payload, so list order is the only authority for positional identity (src/v4/std/node.dag:189-197). P3 fail-closed is represented by the single edge-discipline predicate: NoEdges => count(children) == 0, labeled edges require all names distinct, and positional edges require all labels positional (src/v4/std/node.dag:325-330). The one place that remains check-enforced rather than type-unrepresentable is explicitly documented as a D3 tradeoff, not hidden as “fully unrepresentable” (src/v4/std/node.dag:231-236, src/v4/std/node.dag:241-243).
3. CODING.md. Compliant — the diff uses data declarations plus small free functions, not method-style hidden behavior: connective_edge_discipline, edge_is_named, all_names_distinct, edges_conform, and node_well_formed are explicit input → output helpers over substrate data (src/v4/std/node.dag:253-261, src/v4/std/node.dag:266-280, src/v4/std/node.dag:310-317, src/v4/std/node.dag:325-330, src/v4/std/node.dag:366-370).
4. TESTING.md. Compliant — no tests were added, but I would not block this T-1 substrate-root PR on a Rust-side harness. The behavior that needs later executable receipts is factored into focused predicates (edges_conform, all_names_distinct, node_well_formed) rather than embedded in implementation code, and the diff names the downstream T-6+ obligation for computation-node edge constraints (src/v4/std/node.dag:360-365). The first consumers that construct or normalize these nodes should add behavior-driven .dag claims for the edge-discipline cases.
5. LOCKED DESIGN DECISIONS. Compliant — the diff does not silently diverge from the locked/highest-level substrate shape. It implements the thesis-locked six connectives and five behaviors (THESIS.md:200-204) as the exact closed declarations in the diff (src/v4/std/node.dag:136-142, src/v4/std/node.dag:156-161). It also keeps v4 as .dag substrate authoring rather than adding hand-written Rust, which is aligned with the v4/zero-floor direction (docs/design-pure-bootstrap-zero.md:5, docs/design-pure-bootstrap-zero.md:43-61).
6. TRACKED vs UNTRACKED DEBT. Compliant — the one temporary-looking hole is bounded and named: computation nodes currently have no local edge constraint (src/v4/std/node.dag:335-342), but the diff documents this as an explicit T-6+ obligation and states that later pipeline-stage tasks must extend that arm as each behavior’s edge discipline lands (src/v4/std/node.dag:360-365). That gives the scaffold a subject, boundary, and dissolution trigger rather than leaving “computation nodes unconstrained” as an accidental steady state.

2.5. Top-down PM intent review

Compliant — the PR preserves the high-level v4 intent rather than diluting it. The thesis says v4 is the active substrate instantiation (THESIS.md:5) and that the substrate must remain two coordinated shapes with six type connectives and five behaviors (THESIS.md:200-204); the diff implements exactly that shape and keeps type/computation separated through NodeKind (src/v4/std/node.dag:136-176). I do not read the opaque Symbol as contradicting epistemic stacking: the opacity is specifically about preventing spelling-based kernel heuristics, while actual semantic structure remains in Node, Connective, Behavior, and children (src/v4/std/node.dag:68-84, src/v4/std/node.dag:216-218).

3. Verdict

APPROVE

This is a clean substrate-root modeling PR. The important invariant choices are explicit: closed connectives/behaviors, one recursive Node, no duplicate positional index authority, a single whole-tree well-formedness predicate, and a tracked T-6+ trigger for the computation-node edge discipline.