Skip to content

v4: cut work-direction meta-layer + node.dag Practice-4 ledgers (operator-ratified) - #3160

Merged
briansrls merged 6 commits into
mainfrom
session/still-heron-594-cleanup
May 15, 2026
Merged

briansrls merged 6 commits into
mainfrom
session/still-heron-594-cleanup

Conversation

@briansrls

@briansrls briansrls commented May 15, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Two operator-ratified (2026-05-15) v4 substrate-hygiene changes, one PR, two commits. Operator-directed cleanup — please review/merge personally; not auto-merging.

Commit 1 — cut the work-direction meta-layer

The v3-derived "model our own work-direction as .dag data" substrate is not used by the project, and the compiler model self-justifies (rationale emergent from composition), so no meta-layer narrates it. Deleted (never filled — scaffolds only; nothing in the substrate imported them, verified — pure scope reduction):

src/v4/workflow/{worker_output,brief,cycle,retirement,doc_anchor}.dag

Kept: workflow/{bootstrap,ci}.dag — compiler build infrastructure, explicitly NOT the meta-layer. bootstrap.dag is load-bearing for the anti-regression guarantee (STRUCTURE.md invariant 7); cutting it would reintroduce the v3 regression door — so it stays.

Authority docs narrowed surgically (not gutted), dated + honest per the thesis's own no-fabrication discipline:

  • STRUCTURE.md — workflow/ tree → {bootstrap,ci}; checksum 68→63 .dag; invariant 6 "Workflow substrate first" → "Meta-process as data" (work-direction-substrate claim retracted; lens-self-application to build/CI survives).
  • THESIS.md — facet 4 narrowed: keeps lens self-application to the build/CI pipeline (bootstrap/ci), retracts the T-Workflow-As-Data process-self-modeling sub-claim. Meta-process bullet narrowed.
  • TASKS.md — T-5 → tombstone (decision on record, not silently dropped); bootstrap=T-20, ci=T-24 stand alone.
  • BRIEF_TEMPLATE.md — DEFINITION-OF-DONE "WorkerOutput instance" line removed; why-shape bullet replaced.

Commit 2 — node.dag Practice-4 ledgers (T-1 closeout)

Gate (b) ratified: modeling-discipline.md §4 (coproduct dissolution) is a binding v4 rule, full ledger form. node.dag was the lone non-compliant outlier. Added the full 4-pattern 🟢 GREEN/terminal ledger to its 5 enums (Connective, Behavior, NodeKind, EdgeLabel, EdgeDiscipline) — comment-only; variants byte-unchanged (the closed kernel is terminal by C1 ratification; ledgers make that reviewable per the now-binding discipline).

Verification

  • v2 bootstrap gate green at each commit: Part-A → 63 modules resolved (−5), 0 diagnostics; node.dag ledgers → 63 modules, 0 diagnostics.
  • Diff vs main: 10 files, 136 ins / 143 del — exactly the intended change. No .dag substrate logic changed; node.dag variants byte-identical.

Test plan

  • v2 gate 0-diag after deletions (nothing imported the cut files)
  • v2 gate 0-diag after node.dag ledgers (comment-only)
  • workflow/ = {bootstrap.dag, ci.dag}; bootstrap preserved (invariant-7 load-bearing)
  • Authority-doc narrowing dated + honest (T-5 tombstoned, no silent retraction)
  • Operator personal review of the THESIS facet-4 narrowing (parent-doc edit — flagged for your eyes specifically)

🤖 Generated with Claude Code

briansrls and others added 3 commits May 15, 2026 18:40
Delete the v3-derived "model our own work-direction" substrate — it is
not used by the project and the compiler model self-justifies (rationale
emergent from composition), so no meta-layer narrates it. Removed (never
filled; nothing imported them — pure scope reduction):
  workflow/{worker_output,brief,cycle,retirement,doc_anchor}.dag

Kept: workflow/{bootstrap,ci}.dag — compiler build infrastructure, NOT
the meta-layer. bootstrap.dag is load-bearing for the anti-regression
guarantee (STRUCTURE.md invariant 7).

Authority docs narrowed surgically (not gutted):
- STRUCTURE.md: workflow/ tree → {bootstrap,ci}; count 68→63 .dag;
  invariant 6 "Workflow substrate first" → "Meta-process as data"
  (work-direction-substrate claim retracted; lens-self-application to
  build/CI pipeline survives).
- THESIS.md: facet 4 narrowed — keeps lens self-application to the
  build/CI pipeline, retracts the T-Workflow-As-Data process-self-
  modeling sub-claim (dated, honest, per the thesis's own
  no-fabrication discipline). Meta-process bullet narrowed.
- TASKS.md: T-5 → tombstone (decision on record); bootstrap=T-20,
  ci=T-24 stand alone.
- BRIEF_TEMPLATE.md: DEFINITION-OF-DONE WorkerOutput line removed;
  why-shape bullet replaced (paper-shrink now contained by immutable
  contract + no-new-files + closed substrate + bootstrap reproduction).

v2 bootstrap gate green: 63 modules resolved (−5), 0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…atified)

Gate (b) ratified 2026-05-15: modeling-discipline.md §4 (coproduct
dissolution) is a binding v4 rule, full ledger form. node.dag was the
lone outlier — its 5 enums (Connective, Behavior, NodeKind, EdgeLabel,
EdgeDiscipline) carried no 🟢/🟡/🔴 classification. Added the full
4-pattern GREEN/terminal ledger to each (comment-only; variants
unchanged — the closed kernel is terminal by C1 ratification, the
ledgers just make that reviewable per the now-binding discipline).

v2 bootstrap gate green: 63 modules resolved, 0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls briansrls changed the title T-2 v4: cut work-direction meta-layer + node.dag Practice-4 ledgers (operator-ratified) May 15, 2026
@briansrls
briansrls marked this pull request as ready for review May 15, 2026 22:51
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 0a0f1fec · Trigger: manual
  • Comparison: main @ a549f88c ... session/still-heron-594-cleanup @ 0a0f1fec
  • Conversation: View conversation

1. Story of the diff

This PR narrows v4’s recursive-flex/meta-process claim from “model gunbc’s work-direction as .dag data” to “model only the build/bootstrap and CI pipeline as .dag data.” The thesis line is rewritten so meta-process modeling now names only workflow/bootstrap.dag and workflow/ci.dag, with the work-direction claim explicitly retracted as operator-ratified (THESIS.md:226, THESIS.md:260-280). The same semantic cut is propagated through worker authoring and structure docs: BRIEF_TEMPLATE.md removes the WorkerOutput DoD requirement and explains that the worker-output substrate was cut (src/v4/BRIEF_TEMPLATE.md:52-53, src/v4/BRIEF_TEMPLATE.md:104-110), STRUCTURE.md shrinks workflow/ to two files and updates the checksum from 78 to 73 files (src/v4/STRUCTURE.md:86-114), and TASKS.md tombstones T-5 while preserving bootstrap and CI as T-20/T-24 (src/v4/TASKS.md:181-198).

The code-modeling side of the PR is in src/v4/std/node.dag: it adds 🟢 terminal Practice-4 ledgers to the five closed substrate sum types: Connective, Behavior, NodeKind, EdgeLabel, and EdgeDiscipline (src/v4/std/node.dag:164, src/v4/std/node.dag:201, src/v4/std/node.dag:234, src/v4/std/node.dag:270, src/v4/std/node.dag:337). The five deleted workflow files were empty scaffolds for the now-retracted work-direction substrate, not implemented consumers (src/v4/workflow/brief.dag:14, src/v4/workflow/worker_output.dag:14).

2. Invariant categories

  1. LAYER MODEL — Finding, BLOCKING.

The diff touches substrate declarations in src/v4/std/node.dag, so the terminal modeling evidence has to be complete. The newly added ledger for Connective says // 🟢 GREEN (terminal). Ledger — four patterns attempted: at src/v4/std/node.dag:164, and the same “four patterns” wording recurs for Behavior, NodeKind, EdgeLabel, and EdgeDiscipline at src/v4/std/node.dag:201, src/v4/std/node.dag:234, src/v4/std/node.dag:270, and src/v4/std/node.dag:337. Practice 4 requires trying five dissolution patterns before a terminal classification, including the parameterized-family/projection check; omitting that check makes the substrate GREEN classification under-evidenced. chatgpt-review-8ef26a4a-8175-4a…

  1. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKING.

Specific principle: P1 Modeling Faithfulness / Practice 4 Coproduct dissolution, with Practice 7’s projection-over-enumeration check as the missing fifth pattern. The diff’s ledgers enumerate only fact placement, variant-is-data, algebraic form, and dimensional checks; for example src/v4/std/node.dag:164-175 ends after “4. Dimensional” and immediately declares terminality at src/v4/std/node.dag:176-178. That skips the required “Parameterized family” attempt, which modeling-discipline calls out precisely because patterns 1–4 do not catch mechanically repeated F<X> families. chatgpt-review-8ef26a4a-8175-4a…

The fix is small but substrate-level: add a fifth bullet to each of the five ledgers, even if each says it fails trivially.

  1. CODING.md — N/A.

N/A — this diff does not add or refactor Rust implementation code, helper placement, error/result shapes, methods, or hidden state; it changes docs, .dag comments/types, and deletes empty .dag scaffolds.

  1. TESTING.md — N/A.

N/A — no executable behavior or test runner behavior changes here. The only .dag changes are ledger comments on existing substrate enums plus deletion of unfilled scaffold files, so there is no new behavior-driven test surface to add in this PR.

  1. LOCKED DESIGN DECISIONS — Compliant.

The PR does alter a high-level thesis/design claim, but it does so explicitly rather than silently: the new thesis text says the facet was “narrowed 2026-05-15, operator-ratified” and then names the retracted work-direction sub-claim (THESIS.md:260-280). STRUCTURE.md likewise rewrites invariant 6 to say workflow/ is exactly bootstrap.dag and ci.dag, and explicitly retracts briefs / worker-outputs / cycles / retirement / doc-anchors as modeled process data (src/v4/STRUCTURE.md:293). That is the right shape for a locked-decision divergence: the meaning changes, but the change is surfaced at the authority layer.

  1. TRACKED vs UNTRACKED DEBT — Compliant.

The PR removes scaffolds rather than adding new ones. The deleted files were explicitly marked Status: scaffold — fill per TASKS.md T-5 (src/v4/workflow/brief.dag:14, src/v4/workflow/cycle.dag:14, src/v4/workflow/doc_anchor.dag:13, src/v4/workflow/retirement.dag:14, src/v4/workflow/worker_output.dag:14), and TASKS.md now preserves the removal as a tombstone instead of silently dropping it (src/v4/TASKS.md:181-198). I do not see a new TODO, bridge, temporary carrier, or dissolution-trigger-less scaffold introduced by this diff.

2.5. Top-down PM intent review

Compliant, aside from the ledger completeness finding above. From the PM/executive-owner lens, the scope cut is not hidden semantic dilution: the PR explicitly says the project no longer models its own work-direction, preserves only bootstrap/CI pipeline self-application, and reconciles that same meaning across THESIS.md, STRUCTURE.md, TASKS.md, and BRIEF_TEMPLATE.md (THESIS.md:270-280, src/v4/STRUCTURE.md:86-91, src/v4/TASKS.md:181-198, src/v4/BRIEF_TEMPLATE.md:104-110). I do not see a diff-cited mismatch where a worker would faithfully execute the remaining plan and accidentally rebuild the retracted meta-layer; the plan now says not to.

The one PM-relevant risk is narrower: the PR title promises Practice-4 ledgers, but the added ledgers omit Practice 4’s fifth dissolution pattern. That is not a scope-cut disagreement; it is an incomplete modeling receipt on the remaining substrate work.

3. Verdict

REQUEST_CHANGES

The work-direction meta-layer cut is coherent, explicit, and consistently propagated. The blocker is that the new substrate GREEN ledgers claim only “four patterns attempted” even though the uploaded modeling discipline requires five; complete that fifth parameterized-family/projection check on all five node.dag ledgers before merging.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 0a0f1fec · Trigger: schedule
  • Thinking: 239s wall

Non-blocking — Strengths

  • src/v4/std/node.dag The Practice-4 ledgers classify the five substrate coproducts with concrete dissolution attempts and add no parallel authority.
  • src/v4/TASKS.md The T-5 tombstone preserves the operator-ratified work-direction cut instead of silently dropping the deleted scaffolds.

✅ No blocking concerns; the narrowed build/CI workflow claim stays aligned with the thesis and v4 structure.

briansrls and others added 2 commits May 15, 2026 19:13
modeling-discipline.md §4 was updated to require FIVE dissolution
patterns (added "5. Parameterized family" + Practice 7
projection-over-enumeration — the codified lesson from the Homomorphism
15→1 dissolution). The 5 node.dag ledgers (written against the prior
4-pattern §4) were under-evidenced. Added the 5th-pattern bullet to all
five (Connective/Behavior/NodeKind/EdgeLabel/EdgeDiscipline): each
FAILS trivially with structural reasoning (the variants are
heterogeneous, NOT one generic F<X>/projection over a source set), so
the 🟢 terminal classification stands — now fully evidenced per the
updated rule. Comment-only; variants byte-unchanged.

v2 bootstrap gate green: 63 modules resolved, 0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Re: openai-pro/gpt-5.5-pro REQUEST_CHANGES (12713) — valid finding, fixed in e7f3baf31.

Verified against the current modeling-discipline.md on main: §4 was updated to require FIVE dissolution patterns (it added 5. Parameterized family + Practice 7 "projection over enumeration" — ~+4K chars; the codified lesson from the Homomorphism 15→1 dissolution). My 5 node.dag ledgers were written against the prior 4-pattern §4 and were under-evidenced. openai-pro is correct.

Added the 5th-pattern bullet to all five ledgers (Connective, Behavior, NodeKind, EdgeLabel, EdgeDiscipline). Each FAILS trivially with structural reasoning — the variants are heterogeneous (distinct payloads/arities/semantics), NOT one generic F<X> / projection over a source set (Practice 7) — so the 🟢 GREEN terminal classification stands, now fully evidenced per the updated rule. Comment-only; variants byte-unchanged. v2 bootstrap gate green: 63 modules resolved, 0 diagnostics.

Pre-existing follow-up flagged (NOT this PR's scope): the merged std/algebra.dag ledgers from #3154 (FreeMonoid, Ordering) also predate the 5-pattern §4 — they carry only 4 patterns and are now likewise under-evidenced against the updated rule. Since gate (b) is ratified binding-fully, that is a real consistency debt; it should be a small follow-up PR (add the 5th-pattern bullet to those two, same trivial-FAILS form). Out of scope here (this PR is the workflow-cut + node.dag), surfacing so it is tracked, not dropped.

— sent from still-heron-594

… 12713)

The prior commit added the 5th dissolution-pattern bullet but left each
ledger's lead-in saying "Ledger — four patterns attempted:" — internally
inconsistent (announced four, listed five). Updated all 5 lead-ins to
"five patterns attempted:" so each ledger is self-consistent and fully
compliant with the updated modeling-discipline.md §4 (five patterns).
Comment-only; gate green (63 modules, 0 diagnostics).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

openai-pro 12713 — now FULLY addressed (correcting my prior reply).

Re-verifying against current code (not assuming my earlier fix was complete) caught that e7f3baf31 added the 5th-pattern bullet to all 5 node.dag ledgers but left each lead-in saying Ledger — four patterns attempted: — internally inconsistent (announced four, listed five). That's exactly the under-evidenced shape openai-pro flagged, only half-fixed. Completed in c5b55018c: all 5 lead-ins → five patterns attempted:. So every node.dag ledger now: (a) lists patterns 1–5 incl. 5. Parameterized family (Practice 7 projection-over-enumeration, FAILS trivially with structural reasoning — variants are heterogeneous, not one generic F<X>), and (b) self-describes as five, fully compliant with the updated modeling-discipline.md §4. 🟢 terminal stands; comment-only; v2 gate green (63 modules, 0 diagnostics) at c5b55018c.

Verification receipt: grep -c "five patterns attempted" = 5, "four patterns attempted" = 0.

Pre-existing follow-up still tracked (NOT this PR): merged std/algebra.dag FreeMonoid/Ordering ledgers (from #3154) also predate the 5-pattern §4 — same trivial 5th-bullet + lead-in fix, separate PR.

— sent from still-heron-594

@briansrls
briansrls merged commit 362221e into main May 15, 2026
7 checks passed
briansrls added a commit that referenced this pull request May 15, 2026
B-5 (affected_set R1 usefulness): effect is a per-Arrow-Node fact from
the signature (B3), never aggregated coarse — a granularity invariant
(coarse ⇒ R1 correct-but-useless). effect.dag B-5 block + affected_set
Consumes/Ex.R1 cross-ref + DECISIONS B-5 row.

Subsume #3153 (v4-affected-set-design, no worker — operator-directed):
its 4 worked-examples + adversarial R1/R2/R3 + dogfood-reality folded
into affected_set.dag as the T-21 design contract, reconciled to the
now-ENCODED reciprocal contracts — Ex.R1→B-5 (effect.dag), Ex.R2→B-4
(04_infer.dag), Ex.R3→B-3 (drafted #3157 point-3 correction). #3153
superseded; recommend close. DECISIONS #3153-subsumed row.

B-2 (PROOF-1 prover model lands): extdeps/languages/lean.dag (new) —
Lean first, termination theorem class; Coq deferred second-prover
probe. B2-OMNI requires the LanguageModel file PROOF-1 #3158 deferred.
STRUCTURE enumeration+count 63→64; DECISIONS L-4; TASKS PROOF-1 note.

Includes the already-committed origin/main merge (204b855: #3158
PROOF-1 + #3160 meta-cut; DECISIONS.md conflict resolved keeping
D1/B-4/PROOF-1).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 16, 2026
… (binding §4 compliance) (#3164)

* v4: add Practice-4 5th pattern to algebra.dag FreeMonoid/Ordering ledgers

modeling-discipline.md §4 is binding-full at FIVE patterns (gate (b)).
The merged std/algebra.dag (#3154) FreeMonoid + Ordering coproduct-
dissolution ledgers predate that and carried only four patterns — the
lone remaining non-compliant spot on main after #3160 fixed node.dag.
Added the 5th pattern (Parameterized family / Practice 7 projection-
over-enumeration) to both, each FAILS trivially with structural
reasoning (inductive base/step constructors / fixed trichotomy
codomain — not one generic F<X> over a source set), and corrected the
lead-in count four→five. 🟢 terminal stands; comment-only; variants
byte-unchanged.

v2 bootstrap gate green: 63 modules resolved, 0 diagnostics.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: T-2

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 16, 2026
…EQUEST_CHANGES)

Valid finding. docs/modeling-discipline.md:112 requires FIVE dissolution
patterns; the node.dag #3160 operator-ratified receipts already use 5.
The D1 receipt did only 4 (I wrongly followed algebra.dag's older
4-pattern style). Added Pattern 5 (Parameterized family) — FAILS:
ByName/ByPosition are not one mechanical F<X> over a declared set
(different payload types + addressing semantics; mirror EdgeLabel's
genuine 2-variant discriminant, not an enumerated copy à la
Homomorphism-per-algebra); no source set to project over (Practice-7
N/A); post-dissolution one constructor = not a family. "four" → "five".

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 16, 2026
…#3162)

* WIP: v4 design

* v4 D1: Diff/Path structural-delta vocabulary over Node

Side-session-ratified B-1. EdgeSelector/Path/Edit/Diff data types in
std/node.dag (DATA ONLY; A1-clean — Node stays the sole recursive type;
B1/Hash precedent for substrate-tier placement). Operations
(subterm_at/apply_diff -> Result<Node,Diagnostic>, paths_independent/
diff_well_formed) contracted into lens/application.dag header — forced
off node.dag by the diagnostic.dag->node.dag cycle (Correction=
Suggested(Node)); the node.dag "consumers fail-close" discipline.
affected_set.dag consumes the type. DECISIONS.md Part-1 row D1 carries
the data/op-split PROPOSED sub-point for operator confirmation.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: v4 design

* v4 D1: dissolve two P2 illegal-state surfaces (codex #3162 REQUEST_CHANGES)

Both findings valid; fixed structurally rather than patched.

Finding 1 (node.dag:~478 ByPosition{index:Int} admits negatives): drop
EdgeSelector/ByPosition entirely. Path = List<Symbol> — each step
descends the Named edge keyed by that opaque Symbol. No ordinal exists,
so the negative/out-of-range illegal state is structurally impossible
(dissolved, not deferred to path resolution). Positional-connective
children are reached by replacing the enclosing Named subtree (the safe
over-fire #3157 blesses); surgical positional addressing is a future
operator-ratified extension (consumes-nothing root has no Nat; recursive
Peano = A1 STOP).

Finding 2 (node.dag:~514 Diff=List<Edit> validity via external
predicate): drop the set / pairwise-independence / parallel-positions
framing and paths_independent/diff_well_formed. Diff = ORDERED List<Edit>
applied SEQUENTIALLY; any List<Edit> is a valid rewrite program (no
representable illegal state). A non-resolving Edit => fail-closed
Diagnostic at apply time (operational, not a type-level illegal state);
apply_diff is a fold, all-or-nothing.

Both refine the operator-ratified shape — flagged in DECISIONS.md D1
PROPOSED-for-operator-eye for confirm/redirect.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 D1: add Practice-4 dissolution receipt; fix RATIFIED/PROPOSED contradiction (#3162 BLOCKING)

BLOCKING (codex via briansrls relay, vs pre-fix sha a06a066 — verified
against current HEAD):
- "D1 sum vocabulary without coproduct receipt": the EdgeSelector sum
  was already deleted in 7c91f73, but the DECISION not to have a
  positional selector is itself a Practice-4 dissolution requiring the
  formal 4-pattern ledger (algebra.dag precedent). Added the receipt to
  std/node.dag D1 (🟢 GREEN terminal: positional addressing subsumed by
  enclosing-Named-subtree replacement; not a deferred gap).
- "root-status driving the index carrier": resolved by the same
  dissolution — there is no index carrier; the receipt documents why
  none is needed (vs the reviewer's Nat/Fin suggestion) and why a
  future surgical form is an explicit operator-ratified extension.

Non-blocking: DECISIONS.md D1 row no longer carries a "confirm or
redirect" clause inside a RATIFIED row — refinements are stated as
encoded-via-PR-review (the normal channel), not an open fork.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 D1: fix stale EdgeLabel cross-reference in node.dag header (cursor #3162 editorial)

The D1 header block cited "lines ~221-230" for the no-stored-index
discipline, but adding the D1 header block shifted line numbers — that
range is now `Connective`. Re-anchored by construct name + corrected
approx lines: `type EdgeLabel` ~284 and its "deliberately NO stored
index" rationale ~278. Editorial only; cursor APPROVE on this PR.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 B-4: affected_set R2 node-precise-resolution contract

Encodes the B-4 cross-cutting decision (operator-greenlit): affected_set
minimality requires 04_infer resolution to bind each use-site name-ref
to the EXACT declaration Node (not module/scope). The use->def graph is
derived by traversal over already-resolved name-references, NOT a 5th
InferredFacts field (IR-1-safe; same derive-don't-store discipline as
content_hash/D1). Coarse resolution = correct but maximally over-fires.

Reciprocal header contracts: 04_infer.dag B-4 block + affected_set.dag
Consumes note. DECISIONS.md Part-1 row B-4. Scaffold headers only; no
bodies. Continues the v4 design-survey on the session branch alongside
D1 (operator sequences/carves at manual merge).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 B-5 + subsume #3153 + B-2 (lean.dag PROOF-1 model)

B-5 (affected_set R1 usefulness): effect is a per-Arrow-Node fact from
the signature (B3), never aggregated coarse — a granularity invariant
(coarse ⇒ R1 correct-but-useless). effect.dag B-5 block + affected_set
Consumes/Ex.R1 cross-ref + DECISIONS B-5 row.

Subsume #3153 (v4-affected-set-design, no worker — operator-directed):
its 4 worked-examples + adversarial R1/R2/R3 + dogfood-reality folded
into affected_set.dag as the T-21 design contract, reconciled to the
now-ENCODED reciprocal contracts — Ex.R1→B-5 (effect.dag), Ex.R2→B-4
(04_infer.dag), Ex.R3→B-3 (drafted #3157 point-3 correction). #3153
superseded; recommend close. DECISIONS #3153-subsumed row.

B-2 (PROOF-1 prover model lands): extdeps/languages/lean.dag (new) —
Lean first, termination theorem class; Coq deferred second-prover
probe. B2-OMNI requires the LanguageModel file PROOF-1 #3158 deferred.
STRUCTURE enumeration+count 63→64; DECISIONS L-4; TASKS PROOF-1 note.

Includes the already-committed origin/main merge (204b855: #3158
PROOF-1 + #3160 meta-cut; DECISIONS.md conflict resolved keeping
D1/B-4/PROOF-1).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: v4 design

* v4 B-4: correct the use→def carrier (Symbol/K-1, not resolved_type) — #3162 BLOCKING

Valid P2/Practice-3 finding (briansrls inline @ 04_infer.dag:54):
resolved_type is the node's TYPE; many declarations share a type, so it
is lossy for binding identity — the use→def fact had no named forward
carrier. Corrected: the carrier is the post-resolution opaque Symbol
(K-1) on the name-ref Atom, AUTHORED by 03_resolve.dag (binding =
Symbol equality, node.dag name_occurrences pattern). 04_infer is
preserve-only (no 5th InferredFacts field, IR-1-safe); affected_set
derives by Symbol-equality traversal. Fixed consistently across
04_infer.dag B-4 block, new 03_resolve.dag B-4 authority note,
affected_set.dag Consumes note, DECISIONS.md B-4 row.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: v4 design

* WIP: v4 design

* v4 C5-2 emit-locality + T-9 infer keystone contracts (operator-ratified)

C5-2 (emit-locality): emit is structurally local — a D1 apply_diff at
Path p re-emits ONLY p's subtree. Per operator code-as-data steer:
locality is Node-relative, NOT file-relative; a file is a convenience
projection, the substrate anchors no semantic on the file concept;
non-local emit = declared normalization at the enclosing NODE scope,
never "file scope". The C5↔D1 hinge (AGENT-1 faithful re-emit).
05_emit.dag header + Owns + DECISIONS C5-2 row.

T-9 A+B: A — Find decidable by construction (closed declared-inhabitance
candidate set, not a synthesized search; structural descent ⇒ the
inferencer terminates; empty = decidable fail-closed Diagnostic).
B — single-file discipline is the 03_resolve scope boundary (env/scope/
lookup/binding belongs to 03_resolve per B-4; infer owns only Find +
cardinality + diagnostic precision). 04_infer.dag header + DECISIONS
T-9 row.

Receipts: in-header (operator decision; status quo, no change).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 D1: complete the Practice-4 receipt — add Pattern 5 (#3162 codex REQUEST_CHANGES)

Valid finding. docs/modeling-discipline.md:112 requires FIVE dissolution
patterns; the node.dag #3160 operator-ratified receipts already use 5.
The D1 receipt did only 4 (I wrongly followed algebra.dag's older
4-pattern style). Added Pattern 5 (Parameterized family) — FAILS:
ByName/ByPosition are not one mechanical F<X> over a declared set
(different payload types + addressing semantics; mirror EdgeLabel's
genuine 2-variant discriminant, not an enumerated copy à la
Homomorphism-per-algebra); no source set to project over (Practice-7
N/A); post-dissolution one constructor = not a family. "four" → "five".

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4 C5-1 + C5-3 (operator-ratified) — node-level round-trip law + spec-provable F

C5-1: the bidirectional_roundtrip TestClaim asserts ingest∘emit=id_Node
via B1 content_hash (meaning round-trips), NOT text-byte identity.
Text-level fidelity recorded as a DEFERRED orthogonal future layer (a
trivia sidecar outside Node/content_hash, partial; the C5-fidelity
Declared-normalized dispositions are its forward hook — node-level
adoption preserves it zero-rework). Non-orthogonal route (lexical in
the Node) explicitly rejected.

C5-3: F = the spec-provable meaning core; spec silence ⇒ out of F
(Declared-normalized or Fail-closed). Conservative/fail-safe — the
spec decides, modeler has no discretion; per-language non-F shrinkage
declared up front, not discovered at test time.

Encoded: lens/testgen.dag C5-1/C5-3 header block + DECISIONS C5-1/C5-3
rows.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* v4: reconcile PROOF-1 row with L-4 — DECISIONS.md self-consistency (cursor #3162 APPROVE_WITH_COMMENTS)

Valid NON-BLOCKING finding: B-2 added lean.dag + the L-4 row but the
PROOF-1 row still ended "**NO new file** (closed-tree invariant)",
contradicting L-4 (which lands extdeps/languages/lean.dag). Reconciled:
PROOF-1's framing (#3158) added no file (framing-only, deferred the
model "lands later"); that deferred model subsequently lands as
lean.dag per B-2/L-4. One coherent story; PROOF-1 row now cross-refs
L-4 and states "No contradiction" explicitly.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant