19 Evidence ledgers and provenance
On this page · Permalink · Source line 1818
A claim ledger should answer five questions without reconstructing the entire research history.
What is the exact claim identifier?
What is its current status and scope?
Which justifications depend on it?
Which evidence records support or challenge it?
Which versions and compiled documents contain it?
Definition 19.1: Evidence ledger
An evidence ledger is an appendable collection of typed, scoped records linked to claim and justification identifiers. A record may certify, support, challenge, interpret, or refute an object. Its role is explicit rather than inferred from prose placement.
Definition 19.2: Provenance digest
A provenance digest is a cryptographic hash of a canonical serialization of the claim identifier, content, scope, evidence references, parent version, and relevant build inputs.
A digest does not prove a theorem. A changed digest establishes that the hashed byte sequence changed. An unchanged digest is an integrity check only subject to the possibility of collisions. Canonical serialization gives different representations a common byte-level reference.
Proposition 19.3: Digest stability
Fix a deterministic serialization \(s\) and a deterministic hash function \(h\). Identical serialized byte sequences have identical digests under \(h\). Distinct serialized byte sequences have distinct digests unless they form a collision under \(h\). Detecting a record change additionally requires that the change alter its serialized bytes.
Proof
If \(s(r)=s(r')\), applying the function \(h\) gives equal digests. If \(s(r)\ne s(r')\) but \(h(s(r))=h(s(r'))\), the two serialized strings form a hash collision by definition. Thus change detection at the record level requires both preservation of the audited distinction by \(s\) and exclusion of a collision for the resulting bytes. No injectivity of a fixed-length hash on arbitrary byte strings is asserted.
The serialization contract must state which fields, types, and distinctions it preserves and which differences it intentionally normalizes. Loss during serialization and a collision during hashing are separate mechanisms.
For example, joining string parts with a separator is ambiguous if the same separator may occur inside a part. The tuples \((\texttt{a|b},\texttt{c})\) and \((\texttt{a},\texttt{b|c})\) both become a|b|c. No hash function can recover the lost tuple boundary. The earlier provenance_digest helper had this defect with a control-character separator. Python release 1.4.0 replaces that encoding with a versioned, domain-separated JSON array of strings. Historical digests must retain their earlier format and version. The snapshot digest has its own unchanged serialization contract.
Proposition 19.4: Hashing cannot add recoverable tasks
Let \(s:\mathscr A\to B\) be serialization and \(h:B\to D\) be any deterministic map. Every task recoverable from \(h\circ s\) is recoverable from \(s\). If \(h\) is injective on the attained set \(s(\mathscr A)\), the two encodings support exactly the same tasks.
Proof
If \(s(a)=s(b)\), then \(h(s(a))=h(s(b))\). Any task constant on the digest fibers is therefore constant on the serialization fibers, and Theorem 10.12 supplies its decoder. If \(h\) is injective on attained serializations, equality of digests conversely implies equality of serializations, so the two fiber partitions coincide and the same criterion applies in both directions.
The module ProofPath.Recovery checks both implications. The injectivity condition is a conditional mathematical hypothesis, not a claim that a fixed-length cryptographic hash is injective on arbitrary inputs. A hash cannot repair an ambiguity introduced before hashing. It may introduce additional collisions, which must be kept separate from the serializer's preservation contract.