DAG

DAG — Persistent Axiom Registry + Formal Proof Builder

Every project gets a .dag/ directory. Axioms live there. Future proofs reference by ID — not re-stated. Nothing drifts. Everything traces.

Caveman Rules (all prose output from this skill)

Drop: "I would like to", "please note", "it's worth mentioning", "in order to" Use fragments. "No session store. JWT only." not "You should not use a session store." Keep exact: code, IDs, field names, inference rules, statements — never compressed. Target: 50-65% fewer tokens on prose. Technical accuracy: unchanged.

Registry Structure

{project-root}/
  .dag/
    registry/
      axioms/           # A-type: structural ground truths (non-derivable)
        A1.md  A2.md  ...
      definitions/      # D-type: what terms mean
        D1.md  D2.md  ...
      hypotheses/       # H-type: scope/existence claims (empirical, falsifiable)
        H1.md  H2.md  ...
      theorems/         # T-type: derived conclusions with proof chains
        T1.md  T2.md  ...
      deprecated/       # Tombstones: superseded entries, never deleted
        A2.md  ...
    meta/
      registry.json     # Machine index + consistency state + file paths
      provenance.json   # Full derivation graph
    sessions/
      YYYY-MM-DD-N.md   # Per-session typed scratchpads

One file per entry. Each file = one atom. registry.json is the index: ID → file path + one-liner + status + deps. Agent loads only the files it needs — never more.

Why Directories, Not Files

The three Aristotelian types fail differently:

• D-type: term meaning shifts (drift) → audited separately
• H-type: world changes, scope assumptions go stale → each needs falsification criterion
• A-type: can contradict each other → write-time contradiction check on every add
• T-type: derived conclusions — stay theorems permanently; if content needs to become foundational, human writes a new A-type from scratch

Each type lives in its own directory. Each entry lives in its own file. Retrieval cost = one file read per entry, not one file read per type. This is the atomic access guarantee.

ID Scheme

| Prefix | Type | Example | |--------|------|---------| | D | Definition | D1, D2 | | H | Hypothesis | H1, H2 | | A | Axiom | A1, A2 | | T | Theorem | T1, T2 |

IDs are permanent. Never reused after deprecation. Deprecated entries get tombstones written to registry/deprecated/{original-ID}.md.

Entry Format

Every entry has universal mandatory fields:

---
id: A3
type: axiom
label: "short-human-name"
statement: "The full formal statement. One sentence. No ambiguity."
created: YYYY-MM-DD
created_by: human        # human | derived
status: active           # active | deprecated | under-review
---

Type-specific additional fields — see references/registry-spec.md.

Mandatory rules:

• A-type: rationale field required. Cannot be empty. Axiom without rationale = hypothesis in disguise.
• T-type: derived_from field required. Theorem without provenance = orphaned claim.
• H-type: falsification field required. Hypothesis without falsification = belief, not science.

Commands

| Command | What it does | |---------|-------------| | /dag init | Bootstrapping — co-build registry with user (see Bootstrapping section) | | /dag prove [claim] | Build formal proof chain against registry | | /dag derive [claim] from [IDs] | Add new theorem after 5-check validation | | /dag add axiom | Add A-type after contradiction check + derivability probe | | /dag add definition | Add D-type; flags dependent axioms as under-review | | /dag add hypothesis | Add H-type with mandatory falsification criterion | | /dag review [H-ID] | Review an H-type entry — log verdict (valid / amended / deprecated), reset staleness clock | | /dag deprecate [ID] | Deprecate entry; creates tombstone; checks downstream theorems first | | /dag status | Consistency report from registry.json | | /dag audit | Full consistency re-check, all entries | | /dag session | Print current session scratchpad |

Workflow 1: First Run — /dag init

Check .dag/registry/axioms/ directory first. If .md files exist → load registry.json for summary, ask: continue / review / start fresh. Never silently overwrite.

Then run bootstrapping in strict order (definitions → hypotheses → axioms). See references/bootstrapping.md for full dialogue.

Phase order is mandatory. You cannot write a well-formed axiom before fixing the meaning of the terms it uses.

Key rule during bootstrapping: For every proposed axiom, run the derivability probe: > "Could this be derived from the definitions and hypotheses you've already stated, plus common knowledge?"

If yes → it's a theorem candidate, not an axiom. Derive it, add as T-type. If no → write it as A-type with a mandatory rationale.

Completeness checks (qualitative — no fixed counts):

• Definitions: have you named every project-specific term that could mean different things to different people? If any axiom uses a term someone could reasonably misread, it needs a definition.
• Hypotheses: have you made explicit every assumption about the world that, if false, would change your conclusions?
• Axioms: is every entry genuinely non-derivable from existing entries plus common knowledge? The minimum sufficient set is the goal — neither too few (gaps in reasoning) nor inflated (n² contradiction surface).

After bootstrapping, write all entry files atomically — one file per entry in its type directory (registry/definitions/D1.md, registry/axioms/A1.md, etc.). Update registry.json last, after every entry file exists. Print summary:

Registry initialized for [project]:
  N definitions (D1-DN)
  N hypotheses (H1-HN)
  N axioms (A1-AN)
  0 theorems
Consistency: CLEAN

Workflow 2: Proof Chain — /dag prove [claim]

The LLM is the translator. The registry is the verifier.

The LLM does not generate truths. It translates the claim into derivation steps that cite registry IDs. Steps that cannot cite a registry ID must be flagged — not resolved silently.

Session system prompt for every proof chain: > "You are constructing a derivation, not generating a position. Every step must cite a specific registry ID. Steps that cannot cite a registry ID must be flagged as HIDDEN ASSUMPTION. Do not resolve hidden assumptions — surface them."

Proof output format (always):

AXIOM LAYER (active entries used)
───────────────────────────────────────────────────────
A1: [statement]    [active]
D2: [statement]    [active]

THEOREM LAYER
───────────────────────────────────────────────────────
T_new: [conclusion]
    because: A1, D2
    rule: modus ponens
    confidence: CERTAIN | PROBABLE | UNCERTAIN
    therefore: [concrete decision]

HIDDEN ASSUMPTIONS SURFACED
───────────────────────────────────────────────────────
[HIDDEN ASSUMPTION] [text] → Candidate H-type entry

VERIFICATION
───────────────────────────────────────────────────────
[check] [decision]    traces to [ID]
[X] [decision]        NO PARENT → MISSING AXIOM: [what would justify this]

PROOF CONFIDENCE SUMMARY
───────────────────────────────────────────────────────
[CERTAIN N] [PROBABLE N] [UNCERTAIN N]
Weakest link: [step with lowest confidence + reason]

Confidence band definitions (mandatory per proof step):

| Band | Meaning | When to assign | |------|---------|----------------| | CERTAIN | Direct logical consequence; no assumptions beyond stated premises; formal rule applies cleanly | Modus ponens / transitivity where premise-to-conclusion match is unambiguous | | PROBABLE | Follows with standard domain reasoning; requires one unstated assumption that is common knowledge or industry standard | Step needs a bridging premise not in registry — flag it as [HIDDEN ASSUMPTION] candidate | | UNCERTAIN | Logical gap present; cannot close without adding an H-type or A-type entry; the step may be wrong | Premises do not entail conclusion without additional claims that are NOT common knowledge |

Confidence rules:

• A proof chain where ALL steps are CERTAIN → can be written as T-type without qualification
• A proof chain with PROBABLE steps → can be written as T-type IF all PROBABLE steps have their hidden assumption flagged and user confirms
• A proof chain with ANY UNCERTAIN step → BLOCK write. Must add missing H-type or A-type entry first, then re-derive
• The proof confidence summary is mandatory at the end of every /dag prove or /dag derive output

After proof: ask "Should any hidden assumptions be added as H-type entries?"

Workflow 3: Add Theorem — /dag derive [claim] from [IDs]

Five checks before writing a new theorem entry file:

1. Premise existence: all cited IDs exist and are status: active
2. Term consistency: all terms in statement have D-type definitions or are general language
3. Inference validity: LLM evaluates whether claim follows from premises. Hidden assumptions surfaced as H-type candidates, not silently absorbed.
4. Contradiction check: new theorem checked against all active entries (see references/failure-modes.md for check prompt)
5. Loop check: no circular dependencies in derived_from chain

If check 3 surfaces hidden assumptions → pause. Ask: "Add as H-type entry or revise derivation?" Do not write theorem until resolved.

Workflow 4: Session Scratchpad

Every session creates .dag/sessions/YYYY-MM-DD-N.md. All working claims are typed:

[AXIOM-REF A3] statement cited from registry
[HYPOTHESIS-REF H1] statement cited from registry
[ASSUMPTION] unstated assumption — candidate H-type
[DERIVED] conclusion with cited IDs
[CONTRADICTION FLAG] conflict with [IDs] — requires resolution
[THEOREM CANDIDATE] T_n: candidate for /dag derive
[QUESTION] open question

No untagged entries in the formal scratchpad section.

Token Load Modes

Mode 1 — Summary Index (default): Read registry.json entry_index — one-liner + status + file path per entry. Use at session start, for scoping. Never load individual entry files in this mode.

Mode 2 — Targeted Full Load (during active proof): Read the individual entry file for each cited ID using the file path from registry.json. Load only what the current proof step actually cites — nothing more. Example: Read .dag/registry/axioms/A3.md to get A3's full text — nothing else loads.

Mode 3 — Full Registry Load: Only for: /dag init, /dag audit, /dag deprecate. Read all individual entry files across all type directories. Never for routine proof chains.

Load decision:

• Session start → Mode 1 (registry.json only)
• /dag prove or /dag derive → Mode 1 + Read individual entry files on demand (Mode 2)
• /dag status → Read registry.json only (no entry file loads)
• /dag init / audit / deprecate → Mode 3 (all entry files)

Why this works: An agent reading A3 does Read .dag/registry/axioms/A3.md. It loads only A3. Under the old format, getting A3 required reading axioms.md — loading every other axiom with it. Individual files = atomic access = zero context pollution.

What This Skill Must NOT Do

• Auto-generate axioms without human confirmation of each
• Silently absorb hidden assumptions surfaced during proof chains
• Delete any entry without creating a tombstone
• Add theorem without derived_from field
• Add axiom without rationale field
• Promote theorems to axioms mechanically — if a theorem's content needs to be foundational, the human writes a NEW A-type entry from scratch with their own words; do not copy-promote
• Load Mode 3 for routine proof chains
• Re-use deprecated IDs

References

• Entry format specs + example registry: references/registry-spec.md
• Bootstrapping dialogue in full: references/bootstrapping.md
• Failure mode guards + contradiction check prompt: references/failure-modes.md

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: ndpvt-web
• Source: ndpvt-web/claude-dag-skill
• License: MIT

Install and usage instructions live in the source repository linked above.