The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

null model instrument

DefinitionA version of the data with the structure under test removed and everything else kept, the right comparison for any measured statistic. Chapter 0 section 0.9.
ExampleShuffling the labels 1000 times and rescoring gives the null distribution the measured score is compared against.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id null-model, kind instrument.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 0.17.

Assumptions and scope
  • A version of the data with the structure under test removed and everything else kept. A label permutation keeps every class size and the bag of scores, so any statistic that reads only class sizes or only scores is unchanged by it, and only a statistic that reads the pairing between score and label can move.
  • That is what makes the permuted statistic the right comparison, and the excess over the null mean is the number a chapter reports. A number without its null is not yet a finding, and the drift claim that lost half its size to a paired null is the ledger’s case.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/NullModel.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
00.51statisticnullsystembar
What the statistic looks like when the claimed effect is absent.

Equation

Book equation 0.17.

\[\Pr[X\ge c]=1-\sum_{i<c}e^{-\mu}\frac{\mu^{i}}{i!},\qquad c^{\star}=\max\{c:\ n\Pr[X\ge c]\ge 1\},\qquad \mu=\frac{n_q\,k}{n}.\]

Book equation 8.3.

\[\Pr[\text{at least one of } m\text{ null tests passes}]=1-(1-\alpha)^{m},\qquad \alpha_{\mathrm{Bonferroni}}=\frac{\alpha}{m}.\]

Conditions

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

Ledger

none

First stated

Chapter 0 section 0.9 and chapter 8 section 8.4 of Data Mining as Observation, with the program’s Poisson, paired, and permutation nulls in openvector-bench, readscope, and the encoder gate.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/NullModel.lean, theorems card_pos_perm, scores_perm, stat_of_counts_const, excess_eq_zero_iff, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation primers L and S, chapters 0, 2, 3, 4, 5, 8, 9, 10, 11, 12, 14.

Related

Poisson ceiling; chance level; cross-corpus gate; p-value; harness.

See also

Ledger rows that cite the entry’s records without naming it: OT-4, NEG-15 (Bell boundary).

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.

← null hypothesisnull space →