THE DOMINATOR TABLE

which constants Mathlib's use of choice actually rests on

Asking which constant a theorem's classical dependence is responsible for is not the same as asking which constants its proof touches, and the answers are far apart. 116,766 theorems reach the order lemma lt_or_eq_of_le; 2,018 would stop being classical if it were rebuilt. Reachability overstates responsibility by 58x in that one case.

The column below is the second number. A constant's count is the theorems whose every route to Classical.choice passes through it, so repairing it repairs exactly them and nothing else.

Measured with gonzalgo · Lean 4.32.1 with Mathlib v4.32.1 · 790,171 declarations, 30,015,601 dependency edges, one dominator tree over all 766,564 constants

#	constant	kind	area	theorems dominated	eligible
1	Classical.propDecidable	definition	classical logic	91,858	yes
2	Classical.byContradiction	theorem	classical logic	23,550	yes
3	CategoryTheory.Functor.category	definition	category theory	5,271	yes
4	Std.DHashMap.Internal.Raw₀.isHashSelf_updateBucket_alter	theorem	—	4,899	—
5	Std.DHashMap.Internal.Raw₀.wfImp_alterₘ	theorem	—	4,896	—
6	Std.DHashMap.Internal.Raw.WF.out	theorem	Std: hash maps	4,892	yes
7	Classical.indefiniteDescription	definition	classical logic	4,711	yes
8	Set.instCompleteAtomicBooleanAlgebra	definition	sets	3,430	yes
9	lt_or_eq_of_le	theorem	order / root namespace	2,018	yes
10	_private.Mathlib.Data.Set.Image.0.Set.image_univ._proof_1_1	theorem	—	1,484	—
11	Set.image_univ	theorem	sets	1,483	yes
12	GroupWithZero.toDivisionMonoid	definition	GroupWithZero	1,290	yes
13	eq_or_lt_of_le	theorem	order / root namespace	1,221	yes
14	LE.le.eq_or_lt	theorem	LE	1,179	yes
15	CategoryTheory.Functor.comp	definition	category theory	1,112	yes
16	String.Internal.toArray	definition	—	1,111	—
17	String.toList	definition	strings	1,109	yes
18	AddAction.orbitRel._proof_3	theorem	—	1,044	—
19	AddAction.orbitRel	definition	AddAction	1,041	yes
20	QuotientAddGroup.leftRel	definition	QuotientAddGroup	1,009	yes
21	_private.Mathlib.Algebra.Group.Hom.Defs.0.map_sub'._proof_1_2	theorem	—	856	—
22	map_sub'	theorem	—	855	—
23	map_sub	theorem	order / root namespace	853	yes
24	Classical.not_not	theorem	classical logic	792	yes
25	GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra._proof_8	theorem	—	722	—
26	GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra	definition	GeneralizedBooleanAlgebra	721	yes
27	String.compare	definition	strings	702	yes
28	String.instOrd	definition	—	702	—
29	Filter.comap._proof_2	theorem	—	662	—
30	Filter.comap	definition	filters	660	yes
31	CategoryTheory.Functor.fromPUnit	definition	category theory	616	yes
32	LE.le.lt_or_eq	theorem	LE	583	yes
33	contravariant_le_iff_contravariant_lt_and_eq	theorem	—	578	—
34	_private.Init.Data.List.Nat.Range.0.List.pairwise_lt_range'._proof_1_4	theorem	—	534	—
35	List.pairwise_lt_range'	theorem	—	533	—
36	List.pairwise_lt_range'._f	definition	—	533	—
37	List.nodup_range'	theorem	—	525	—
38	_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.testBit_two_pow_sub_succ._proof_1_3	theorem	—	520	—
39	Nat.testBit_two_pow_sub_succ	theorem	Nat	519	yes
40	_private.Init.Data.List.Nat.Range.0.List.nodup_range._simp_1_1	theorem	—	515	—
41	List.nodup_range	theorem	lists	514	yes
42	subset_interior_iff_isOpen	theorem	order / root namespace	511	yes
43	Classical.not_forall	theorem	classical logic	497	yes
44	Classical.em	theorem	classical logic	476	yes
45	CategoryTheory.instCompleteLatticePresieve	definition	category theory	450	yes
46	_private.Init.Data.Nat.Mod.0.Nat.mul_lt_mul_left._proof_1_1	theorem	—	440	—
47	Nat.mul_lt_mul_left	theorem	Nat	439	yes
48	MulAction.orbitRel._proof_3	theorem	—	423	—
49	MulAction.orbitRel	definition	MulAction	420	yes
50	Array.foldrM_congr	theorem	arrays	410	yes
51	Nat.rel_of_forall_rel_succ_of_le_of_le	theorem	—	405	—
52	Nat.rel_of_forall_rel_succ_of_le	theorem	—	400	—
53	monotone_nat_of_le_succ	theorem	order / root namespace	399	yes
54	WellFounded.extrinsicFix	definition	WellFounded	398	yes
55	IsUnit.unit	definition	IsUnit	397	yes
56	BooleanAlgebra.toBiheytingAlgebra	definition	BooleanAlgebra	381	yes
57	Std.DHashMap.Internal.Raw.foldRev_eq	theorem	Std: hash maps	374	yes
58	Std.DHashMap.Internal.Raw.foldRev_cons_apply	theorem	—	373	—
59	WellFounded.extrinsicFix₂	definition	WellFounded	366	yes
60	Multiset.add_right_inj	theorem	multisets	363	yes
61	List.eq_nil_iff_forall_not_mem	theorem	lists	363	yes
62	Multiset.instAddCancelCommMonoid._proof_3	theorem	—	361	—
63	Multiset.instAddCancelCommMonoid	definition	—	360	—
64	LinearMap.range._proof_1	theorem	—	358	—
65	LinearMap.range	definition	LinearMap	357	yes
66	_private.Mathlib.Algebra.Group.Center.0.Set.mul_mem_center._proof_1_4	theorem	—	351	—
67	Set.mul_mem_center	theorem	sets	350	yes
68	Std.IterM.toArray.go	definition	—	348	—
69	Std.IterM.toArray	definition	Std: other	347	yes
70	AddSubmonoid.instCompleteLattice._proof_1	theorem	AddSubmonoid	337	yes
71	CategoryTheory.shiftFunctor	definition	category theory	335	yes
72	Lean.Name.quickCmpAux._f	definition	—	333	—
73	Lean.Name.quickCmpAux	definition	—	333	—
74	Lean.Name.quickCmp	definition	Lean	333	yes
75	Submodule.completeLattice	definition	Submodule	333	yes
76	Nat.mono_cast	theorem	Nat	328	yes
77	AddSubmonoid.instCompleteLattice	definition	AddSubmonoid	326	yes
78	CategoryTheory.Sieve.instCompleteLattice	definition	category theory	322	yes
79	Classical.ofNonempty	definition	classical logic	321	yes
80	em	theorem	order / root namespace	316	yes
81	QuotientGroup.leftRel	definition	QuotientGroup	308	yes
82	GroupWithZero.noZeroDivisors	theorem	GroupWithZero	288	yes
83	CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	definition	category theory	284	yes
84	[email protected]._hygCtx._hyg.8	definition	—	283	—
85	[email protected]._hygCtx._hyg.8	other	—	282	—
86	_private.Mathlib.Data.Real.Basic.0.Real.lt	definition	—	282	—
87	Real.instLT	definition	Real	282	yes
88	LinearEquiv.ofBijective	definition	LinearEquiv	281	yes
89	isOpen_iff_forall_mem_open	theorem	—	279	—
90	zpow_ne_zero	theorem	order / root namespace	279	yes
91	IsLocallyConstant.tfae	theorem	IsLocallyConstant	278	yes
92	IsLocallyConstant.iff_eventually_eq	theorem	—	272	—
93	Set.biInter_range	theorem	sets	270	yes
94	Std.DTreeMap.Internal.Impl.WF.ordered	theorem	Std: other	266	yes
95	FreeAlgebra.lift._proof_4	theorem	FreeAlgebra	263	yes
96	DFinsupp.zipWith._proof_4	theorem	—	262	—
97	DFinsupp.zipWith	definition	DFinsupp	261	yes
98	eq_or_ne	theorem	order / root namespace	260	yes
99	Equiv.ofBijective	definition	Equiv	258	yes
100	Equiv.Perm.permGroup	definition	Equiv	250	yes

Showing the first 100 of 3,000 rows. The tail is long and flat — rank 3,000 dominates 10 theorems. The full set is in the JSON and the CSV.

theorems dominated counts theorems for which this constant is the sole route to the axiom. eligible is false when the constant's own type is classical, so no constructive replacement for it can exist; it is false for only 2 of the 1,500 constants where it was computed, which is the negative result in the eligibility note — the test does not discriminate among load-bearing constants. area and eligible were computed for the top 1,500 only; below that they are blank rather than guessed.

Get the data

dominator-table.json · dominator-table.csv · CC-BY-4.0 · version 2026-08-11

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

Reproduce it

# regenerate the declaration graph (~3 min, ~600 MB)
lake env lean -D maxErrors=4000 lean/Dump.lean
python analysis/dominators.py

ConstantInfo.value? must be passed allowOpaque := true or theorem proofs read as empty and every statement-versus-proof figure is wrong rather than imprecise. Code and derived data: 10.5281/zenodo.21883963.

Two results worth reading off it

60.1% of classically dependent theorems have no responsible constant at all. Their immediate dominator is the axiom itself, so no local repair anywhere in the library reaches them. That is the ceiling on what this kind of work can do, and it was not previously known.

Outside classical logic proper, the largest sites are infrastructure rather than mathematics: a functor category instance at 5,271, hash-map well-formedness at 4,899, the powerset Boolean algebra at 3,430, string conversion at 1,111. The places where choice is load-bearing are not the places anyone would have pointed at.

A disagreement in the source data

The reproduction archive carries two files with a count per constant, and they disagree on 137 of the 1,500 they share — hash-map well-formedness is 4,899 in one and 4,892 in the other. The published note reports 4,899, so that file is used here for every count and the other only for the categorical columns. Where they differ, the row carries a count_in_eligibility_file field so the disagreement is visible in the data rather than resolved out of sight.

What is not here yet

A reach column. The 58x figure above is one measured pair; computing reach for every row means a second traversal of the full graph and it has not been run. It is missing rather than estimated.