witness concept
| Definition | An independent measurement of whether a certificate's claim was true. Chapter 13. |
|---|---|
| Example | The witness read the replica’s actual position where the certificate had said fresh, and that disagreement is one false clear. |
| Book | Data Mining as Observation, draft 0.2, commit f3914f0; entry id witness, kind concept. |
| Status | no ledger row names this entry. Corrections: none recorded. |
| Defining equation | Book equation 0.26. |
| Assumptions and scope |
|
| Prior art | none recorded |
| Evidence | lean/DataMiningAsObservation/Certificate.lean |
| Reviewed | not yet reviewed; generated 2026-09-10 from records at the commits on the provenance page. |
Equation
Book equation 0.26.
\[\mathrm{FC}=\Pr\big[W\ \text{refutes}\ \big|\ \mathcal C_t\ \text{clears}\big],\qquad \text{coverage}=\Pr\big[\mathcal C_t\ \text{clears}\big].\]
Book equation 13.1.
\[\mathrm{FC}=\Pr\big[W\ \text{refutes}\ \big|\ \mathcal C_t\ \text{clears}\big],\qquad d_O(\Delta)=\operatorname{tr}\big(P_C\,M_{\mathrm{drift}}(\Delta)\big),\qquad M_{\mathrm{drift}}(\Delta)=\mathbb E\big[\delta_\Delta\delta_\Delta^{\top}\big].\]
Conditions
- A witness is independent of the certificate it grades. A certificate that grades itself has no witness.
- The witness is the consumer’s own outcome or a measurement of it, so the same certificate has a different witness for each consumer, as the hot and cold readers of one replica show.
Conditions are curated in entries.toml rather than read
from a record.
Ledger
none
First stated
Volume 14, chapter 19,
geometric-observation/chapters/ch19_the_certificate_that_ages.md:61-76,
and the freshness program’s umbrella document
observation-theory-campaigns/experiments/FRESHNESS-PROGRAM.md.
Measurements
From
observation-theory-campaigns/experiments/DATABASE-FRESHNESS-TRACK.md
at f7b7c77.
- line 23. XPROTO-PG (analysis/pgrep); Postgres, recovery_min_apply_delay; WAL LSN; ~0.50 → ~0.06
- line 24. XPROTO-MG (analysis/mongo); MongoDB delayed secondary; oplog ts; ~0.47 → ~0.03
- line 25. XPROTO-PGX (analysis/pgx); production PG, netem lag; WAL LSN, pg_stat_statements footprint; ~0.47 → ~0.02
- line 27. XPROTO-ZK (analysis/zk); ZooKeeper 3.9 ensemble; zxid, sync(); hot 0.99 / cold 0.01, witnessed 0.0
From
observation-theory-campaigns/experiments/RADIO-FRESHNESS-TRACK.md
at f7b7c77.
- line 25. XPROTO-CSI (analysis/csi); CQI → MCS; HARQ; 0.34–0.37 → 0.10 (OLLA); ✅ 08-23
- line 26. XPROTO-BEAM (analysis/beam); mmWave beam index; HARQ; 0.31 → 0.02 (BFR); ✅ 08-23
- line 27. XPROTO-AICSI (analysis/aicsi); neural-CSI recon (turboquant bridge); precoder/HARQ; recon wins yet 0.28 → 0.13; ✅ 08-23, scope-corrected 08-25 ⚠️
- line 28. XPROTO-HO (analysis/ho); RSRP → serving cell; RLF; 0.31–0.44 → 0.09–0.12; ✅ 08-23
- line 30. XPROTO-PHY (analysis/phy); PMI / RI / TA; HARQ; 0.27–0.42 → 0.055–0.13; ✅ 08-24
Failures and corrections
none
Invariance envelope
none declared
Machine checked
lean/DataMiningAsObservation/Certificate.lean,
theorems falseClear_mul_coverage,
coverage_empty, falseClear_mem_unit,
minOverStrata_passes_iff,
minOverStrata_le_weighted_mean, at observation-data-mining
f3914f0; what the check covers is stated in the book’s appendix
C.
Used in
Data Mining as Observation chapters 0, 12, 13, 14.
Related
certificate; false-clear rate; coverage.
See also
Sources-table rows that share a record with the entry without naming it: chapter 12 section 12.6, chapter 13 section 13.3, chapter 13 section 13.4.
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.