The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

sweep instrument

DefinitionRunning a measurement across a range of one parameter and reading the curve. Chapter 5 section 5.4 and chapter 9 section 9.3.
ExampleThresholds from 0.1 to 0.9 in steps of 0.1 trace nine points of the ROC curve.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id sweep, kind instrument.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equationnone
Assumptions and scope
  • Running a measurement across a range of one parameter, a threshold, a budget, or a degradation, and reading the curve. As a threshold rises the set called positive can only shrink, so true and false positives fall together and the ROC curve is traced.
  • Fourteen corpora were swept through degradation until retrieval died, the budget sweep found the cliff at k equal to d, and the threshold sweep found the optimal F1 by sort.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/Threshold.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
00.51050100thresholdpositives calleda higher threshold calls fewer rows
A measurement run across a range of one parameter.

Equation

none

Conditions

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

Ledger

none

First stated

Chapter 5 section 5.4 and chapter 9 section 9.3 of Data Mining as Observation, with the degradation sweep in openvector-bench/README.md:60-96.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/Threshold.lean, theorems predicted_anti, tp_anti, fp_anti, decision_comp, predicted_extremes, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 3, 4, 5, 6, 7, 8, 9, 10, 13.

Related

threshold; ROC curve; budget cliff; sensitivity; harness.

See also

Book equations stated beside the entry’s terms, not defining it: 6.2, 0.28, 9.3.

Ledger rows that cite the entry’s records without naming it: GO-3, GO-4.

Sources-table rows that share a record with the entry without naming it: chapter 5 section 5.4, chapter 11 section 11.4, chapter 11 section 11.7, chapter 12 section 12.2.

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.

← surrogatesymmetric matrix →