The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

lag concept

DefinitionHow far a replica trails the primary. The same lag gives two readers two staleness rates. Chapter 0 section 0.13 and chapter 13.
ExampleA replica 50 writes behind the primary is fresh for a reader that touches none of those 50 rows and stale for one that does.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id lag, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equationnone
Assumptions and scope
  • How far a replica trails the primary, in writes or in time. A read of the replica is stale for a consumer whose footprint the lag has touched and fresh for one it has not, so the same lag gives two readers two staleness rates, and a mixed workload’s rate lies between them.
  • Postgres read 0.50 to 0.06, MongoDB 0.47 to 0.03, and production Postgres 0.47 to 0.02 across readers on the same lag, with disjoint seeds.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/Replica.lean, lean/DataMiningAsObservation/Freshness.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
timestale for this readerprimary writereplica catches up
How far a replica trails the primary.

Equation

none

Conditions

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

Ledger

none

First stated

Chapter 0 section 0.13 of Data Mining as Observation, with the replica measurements in observation-theory-campaigns/experiments/DATABASE-FRESHNESS-TRACK.md.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/Replica.lean, theorems stale_mono, stale_zero, naive_certificate, witnessed_certificate, witnessed_coverage, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

lean/DataMiningAsObservation/Freshness.lean, theorems disagree, mixedRate_between, mixedRate_eq_left_iff, stale_for_all, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 13.

Related

replica; freshness; coherence time; false-clear rate; footprint.

See also

Book equations stated beside the entry’s terms, not defining it: 0.26, 13.2, 0.25.

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

Sources-table rows that share a record with the entry without naming it: chapter 13 section 13.2, chapter 13 section 13.3.

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.

← KV cacheLandauer's principle →