Monotone Invariance Theorem result

Definition	A strictly monotone transform of a score in either direction cannot change its optimal thresholded F1, because the sweep tries thresholds both ways. A strictly increasing transform leaves the AUROC unchanged, and a strictly decreasing one sends it to one minus itself. Equation 6.2. Also Monotone Invariance, strictly monotone.
Example	Squaring a positive score keeps every ranking, so its AUROC and its optimal F1 are unchanged, and negating it sends AUROC 0.75 to 0.25.
Book	Data Mining as Observation, draft 0.2, commit `f3914f0`; entry id `monotone-invariance`, kind result.
Status	no ledger row names this entry. Corrections: none recorded.
Defining equation	Book equation 6.2.
Assumptions and scope	Two statements with different scope. A strictly monotone transform of a score in either direction cannot change its optimal thresholded F1, because the sweep tries thresholds in both directions and so reaches every partition the transform can. A strictly increasing transform leaves the AUROC unchanged, and a strictly decreasing one sends it to 1 minus A. The F1 half licenses the pruning of monotone unary nodes in the formula search. The AUROC half licenses nothing about decreasing transforms. The Lean file states the increasing case, and the AUROC file states the reversal.
Prior art	none recorded
Evidence	`theory-radar/paper/astar_paper.tex:94-170`, `theory-radar/paper/theory_radar_paper.tex:290-304`, `theory-radar/paper/astar_paper.tex:94-110`, `lean/DataMiningAsObservation/MonotoneInvariance.lean`
Reviewed	semantic review 2026-09-06; generated 2026-09-10 from records at the commits on the provenance page.

Optimal thresholded F1 survives any strictly monotone transform, AUROC only an increasing one.

Equation

Book equation 6.2.

\[\begin{gathered} \max_{\tau,\ \mathrm{dir}}F_1\!\Big(\mathbf 1\big[\mathrm{dir}\big(g(f(X)),\tau\big)\big],\,y\Big)=\max_{\tau,\ \mathrm{dir}}F_1\!\Big(\mathbf 1\big[\mathrm{dir}\big(f(X),\tau\big)\big],\,y\Big) \\ \text{for every strictly monotone } g. \end{gathered}\]

Conditions

Two statements with different scope. A strictly monotone transform of a score in either direction cannot change its optimal thresholded F1, because the sweep tries thresholds in both directions and so reaches every partition the transform can. A strictly increasing transform leaves the AUROC unchanged, and a strictly decreasing one sends it to 1 minus A.
The F1 half licenses the pruning of monotone unary nodes in the formula search. The AUROC half licenses nothing about decreasing transforms. The Lean file states the increasing case, and the AUROC file states the reversal.

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

Ledger

none

First stated

theory-radar, theory-radar/paper/theory_radar_paper.tex:290-304 and theory-radar/paper/astar_paper.tex:94-110, DOI 10.5281/zenodo.20660206, and chapter 6 section 6.3 of Data Mining as Observation.

Measurements

Where the book states it	Numbers, as the book’s sources table records them	Source
chapter 5 section 5.4	Monotone Invariance and AUROC invariance theorems, the AUROC to F1 bound via the Youden index, stated in the source for every ROC curve and corrected in the book to concave curves, with the counterexample at AUROC 0.75 and F1 0.857	`theory-radar/paper/astar_paper.tex:94-170`; `theory-radar/paper/theory_radar_paper.tex:290-304`
chapter 6 section 6.3	Monotone Invariance Theorem and its proof	`theory-radar/paper/theory_radar_paper.tex:290-304`; `theory-radar/paper/astar_paper.tex:94-110`

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/MonotoneInvariance.lean, theorems aurocNum_comp, auroc_comp, predicted_comp, predictedBelow_comp, sweptF1_comp, sweptF1Below_comp, optF1_comp, 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, 5, 6, 12.

formula search; safe pruning; Youden F1 bound.

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.

← min-over-strataMonte Carlo →