The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

capacity concept

DefinitionThe number of distinctions a model class can draw, the model-side half of the budget. Chapter 6.
ExampleA formula of depth three over 18 operations can draw far fewer boundaries than a forest of 500 trees.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id capacity, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equationnone
Assumptions and scope
  • The number of distinctions a model class can draw, the budget’s model-side half. A read operator’s rank is at most the dimension, and a probe with fewer directions than the dimension cannot resolve the operator, which is the cliff.
  • A formula of depth three over eighteen operations has a capacity the ensemble exceeds, and the ensemble wins exactly when the boundary needs that excess.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/ProbeCliff.lean, lean/DataMiningAsObservation/Rank.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
directioneigenvaluekept | dropped
The distinctions a model class can draw, the model-side half of the budget.

Equation

none

Conditions

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

Ledger

none

First stated

Chapter 6 section 6.1 of Data Mining as Observation, with the budget inversion in geometric-observation/claims/LEDGER.md row GO-4.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/ProbeCliff.lean, theorems centralDiff_affine, centralDiff_basis, exists_blind_direction, indistinguishable, budget_cliff, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

lean/DataMiningAsObservation/Rank.lean, theorems rank_le_width, rank_le_height, rank_outer_le_one, rank_mul_le, rank_zero, rank_transpose, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 6, 7.

Related

budget; budget cliff; rank; ensemble.

See also

Book equations stated beside the entry’s terms, not defining it: 1.1, 6.1, 11.4.

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

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

← calibrationcentral limit theorem →