Provenance

Provenance is the ability to trace a conclusion back to its origins. In zetl, every fact, rule, and conclusion carries metadata recording the source file, line number, and page name where it was defined.

(given provenance-documented)

Why it matters

A reasoning system that says “X is true” is only useful if you can ask “why?” and get a concrete answer. Provenance connects the Reasoning Engine’s abstract logic back to the human-readable documents in your vault.

What is tracked

Element	Provenance
Fact	File path, line number, page name
Rule	File path, line number, page name, rule label
Conclusion	Full proof tree of contributing rules and facts
Grounding	Section hash or explicit source reference (see Drift Detection)

Commands

zetl reason explain <literal> — proof tree with source locations
zetl reason provenance <literal> — cross-referenced with the Link Graph
zetl reason export --format spl — reconstructed concepts/Spindle Lisp with provenance comments

Grounding freshness

Since SPEC-006 Merkle Tree, provenance includes grounding freshness. Each source in a provenance trace reports whether its grounding (section or explicit) is still fresh — i.e., whether the prose that justifies the fact has changed since the theory was built.

Example

Running zetl reason provenance "vault-ready-to-publish" on this vault traces the conclusion through rules in theories/vault-readiness.spl back to facts scattered across the architecture, reference, and concept pages.

Type	Syntax	Meaning
Fact	`(given X)`	X is unconditionally true
Strict	`(always label body head)`	If body, then head — no exceptions
Defeasible	`(normally label body head)`	If body, normally head — can be defeated
Defeater	`(except label body head)`	If body, block head — but don’t assert the opposite

Tag	Meaning
`+D`	Definitely provable — strict derivation, no defeating possible
`-D`	Definitely not provable
`+d`	Defeasibly provable — inferred, no active defeaters
`-d`	Defeasibly not provable — blocked or no derivation path

Tag	Meaning
`+D`	Definitely provable — strict derivation, no defeating possible
`-D`	Definitely not provable
`+d`	Defeasibly provable — inferred, no active defeaters
`-d`	Defeasibly not provable — blocked or no derivation path

ID	Requirement
REQ-037	Merkle tree construction during index
REQ-038	SPL block dual hashing (content + AST)
REQ-039	Two-tier cache invalidation (mtime + content hash)
REQ-040	SPL-specific theory cache invalidation
REQ-041	Implicit section grounding
REQ-042	Explicit grounding via `(meta ... (source ...))`
REQ-043	Drift detection in `zetl check --drift`
REQ-044	Durable provenance with content hashes
REQ-045	Content block discovery (`zetl blocks`)