The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

operating point concept

DefinitionThe row at which a consumer is read, or the threshold at which a classifier is scored. A probe pays 2d evaluations for one. Chapter 0 section 0.5 and chapter 11 section 11.7.
ExampleA probe at one row with 16 directions spends 32 calls at that one operating point.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id operating-point, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 0.8.

Assumptions and scope
  • The row at which a consumer is read, or the threshold at which a classifier is scored. A central-difference probe pays two evaluations per coordinate for one operating point, and raising a classifier’s threshold can only shrink the set it calls positive.
  • Whether many cheaper operating points can average their way back to the population operator was measured within a budget range and not proved, and the cliff at k equal to d does not soften for a probe confined to the directions it chooses.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/FiniteDifference.lean, lean/DataMiningAsObservation/Threshold.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
00.5100.51false positive ratetrue positive rateoperating pointarea under the curve, AUROCchance is the diagonal
The row at which a consumer is read, or the threshold at which a classifier is scored.

Equation

Book equation 0.8.

\[g_j\;\approx\;\frac{C(x+h\,e_j)-C(x-h\,e_j)}{2h},\qquad j=1,\dots,d.\]

Book equation 11.4.

\[\text{directions resolved}(k)=\begin{cases}1\ \text{or}\ 2,& k<d\\[2pt] \operatorname{rank}P_C,& k\ge d\end{cases}\qquad \text{cost}=2d\ \text{consumer calls per operating point}.\]

Conditions

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

Ledger

none

First stated

Chapter 0 section 0.5 and chapter 11 section 11.7 of Data Mining as Observation, with the budget law in readscope/README.md:118-141.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/FiniteDifference.lean, theorems central_quad, forward_quad, forward_error, central_cost, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

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 0, 2, 5, 6, 11, 14.

Related

finite difference; budget; budget cliff; threshold; blind probe.

See also

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

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

Sources-table rows that share a record with the entry without naming it: chapter 11 section 11.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.

← observerorthogonal →