The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

commit hash instrument

DefinitionThe fingerprint git assigns to a snapshot of a repository and its history, which identifies the content exactly and does not by itself prove when it existed. Chronology comes from a public push, a signed tag, or an archival deposit. Chapter 0 section 0.12. Also commit.
ExampleCommit 3172e00 identifies one snapshot of the book’s repository and every file in it, and says nothing about the clock.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id commit-hash, kind instrument.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equationnone
Assumptions and scope
  • The fingerprint git assigns to a snapshot of a repository together with its history. It identifies exact content, so a changed hash proves a changed file and an equal hash is strong evidence of an unchanged one, but it does not by itself prove when that content existed, since git’s author and committer dates are supplied fields.
  • Chronology comes from a public repository receipt, a signed tag, a transparency log, or an archival deposit such as a Zenodo DOI, and a sealed prediction names one of those beside its hash.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/Seal.lean
Reviewedsemantic review 2026-09-06; generated 2026-09-10 from records at the commits on the provenance page.
predictionsealed3f2a…measurementrun9c1e…verdictreportedb7d0…each file's digest is recorded before the next step, and a changed digest proves a changed file
A fingerprint of a snapshot and its history, proving content and not time.

Equation

none

Conditions

Conditions are curated in entries.toml rather than read from a record.

Ledger

none

First stated

Chapter 0 section 0.12 of Data Mining as Observation, with the program’s seal ledger, observation-theory-campaigns/experiments/SEALS.md:1-10, where every seal is a registration id, a sealing commit, and a hash.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/Seal.lean, theorems changed_of_hash_ne, hash_eq_of_eq, exists_collision, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation primers L and S, chapters 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14.

Related

hash; sealed; sources table; preregistration.

See also

Book equations stated beside the entry’s terms, not defining it: 8.3.

Ledger rows that cite the entry’s records without naming it: OT-7.

Status

Generated 2026-09-10 by encyclopedia/generate.py; book at observation-data-mining f3914f0; the commit of every record is listed in the encyclopedia’s provenance.

← column spacecommute time →