THE SPEND-POINT TABLE

where choice is spent, and where it is only inherited

Dominance says which site a theorem's classical dependence is responsible to. It does not say where the axiom is actually spent, and the two come apart hard.

15 of these 20 sites contain no direct use of a choice primitive anywhere in their subtree. Between them they dominate 25,992 theorems while spending nothing — every primitive use is above them in the graph. Rebuilding such a site does not remove a use of choice; it removes a route to one.

Measured with gonzalgo · Lean 4.32.1 with Mathlib v4.32.1 · dominator subtrees over 766,564 constants, primitives counted where cited directly

#	site	theorems dominated	subtree	spenders	primitives cited
1	Classical.propDecidable	91,858	112,158	6,775	Classical.byContradiction x5338, Classical.propDecidable x1540
2	Classical.byContradiction	23,550	30,169	1,854	Classical.byContradiction x1854
3	CategoryTheory.Functor.category	5,271	7,558	0	(none — inherits)
4	Std.DHashMap.Internal.Raw.WF.out	4,899	5,000	0	(none — inherits)
5	Classical.indefiniteDescription	4,711	5,452	44	Classical.em x30, Classical.indefiniteDescription x14
6	Set.instCompleteAtomicBooleanAlgebra	3,430	4,047	0	(none — inherits)
7	lt_or_eq_of_le	2,018	2,151	1	Classical.propDecidable x1
8	Set.image_univ	1,484	1,838	0	(none — inherits)
9	GroupWithZero.toDivisionMonoid	1,290	1,558	0	(none — inherits)
10	eq_or_lt_of_le	1,221	1,314	0	(none — inherits)
11	LE.le.eq_or_lt	1,179	1,271	0	(none — inherits)
12	CategoryTheory.Functor.comp	1,112	1,515	0	(none — inherits)
13	String.toList	1,111	4,557	0	(none — inherits)
14	AddAction.orbitRel	1,044	1,311	0	(none — inherits)
15	QuotientAddGroup.leftRel	1,009	1,271	0	(none — inherits)
16	map_sub	856	999	0	(none — inherits)
17	Classical.not_not	792	799	1	Classical.propDecidable x1
18	GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra	722	828	0	(none — inherits)
19	String.compare	702	3,427	0	(none — inherits)
20	Filter.comap	662	784	0	(none — inherits)

subtree is the constants under the site in the dominator tree. spenders is how many of them cite a choice primitive (Classical.propDecidable, byContradiction, indefiniteDescription, em) directly rather than through another constant. Zero means the site inherits the axiom entirely.

Get the data

spend-points.json · spend-points.csv · CC-BY-4.0 · version 2026-08-12

One of the gonzalgo indexes — standing measurements of what formal libraries rest on, remeasured as the libraries move.

Reproduce it

lake env lean -D maxErrors=4000 lean/Dump.lean
python analysis/spendpoints.py

Code and derived data: 10.5281/zenodo.21883963.

The two that carry almost everything

Classical.propDecidable has 6,775 spenders in its subtree and Classical.byContradiction 1,854. Between them they account for nearly all direct spending in the library, and propDecidable's own subtree spends byContradiction 5,338 times against its own 1,540 — the decidability fallback reaches the axiom mostly through excluded middle rather than directly.

Everything below them in this table is structural. A functor category instance dominates 5,271 theorems and spends nothing. Hash-map well-formedness dominates 4,899 and spends nothing. These are places classical dependence passes through, not places it originates.

Why the distinction changes what you would do

A repair aimed at a spend point removes a use of the axiom. A repair aimed at a pure dominator reroutes a large number of theorems without removing anything, and only helps if the route it removes was the only one. Both are visible as large numbers in a dominance ranking and they are not the same kind of target.

String.toList is the sharpest case here: 1,111 theorems dominated, a subtree of 4,557 constants, and no spender in any of them.