The Dominator Table

which sites Mathlib's use of choice actually rests on

Asking which constant a theorem's classical dependence is responsible to 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 site'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

#	site	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.WF.out	theorem	Std: hash maps	4,899	yes
5	Classical.indefiniteDescription	definition	classical logic	4,711	yes
6	Set.instCompleteAtomicBooleanAlgebra	definition	sets	3,430	yes
7	lt_or_eq_of_le	theorem	order / root namespace	2,018	yes
8	Set.image_univ	theorem	sets	1,484	yes
9	GroupWithZero.toDivisionMonoid	definition	GroupWithZero	1,290	yes
10	eq_or_lt_of_le	theorem	order / root namespace	1,221	yes
11	LE.le.eq_or_lt	theorem	LE	1,179	yes
12	CategoryTheory.Functor.comp	definition	category theory	1,112	yes
13	String.toList	definition	strings	1,111	yes
14	AddAction.orbitRel	definition	AddAction	1,044	yes
15	QuotientAddGroup.leftRel	definition	QuotientAddGroup	1,009	yes
16	map_sub	theorem	order / root namespace	856	yes
17	Classical.not_not	theorem	classical logic	792	yes
18	GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra	definition	GeneralizedBooleanAlgebra	722	yes
19	String.compare	definition	strings	702	yes
20	Filter.comap	definition	filters	662	yes
21	CategoryTheory.Functor.fromPUnit	definition	category theory	616	yes
22	LE.le.lt_or_eq	theorem	LE	583	yes
23	List.nodup_range	theorem	lists	534	yes
24	Nat.testBit_two_pow_sub_succ	theorem	Nat	520	yes
25	subset_interior_iff_isOpen	theorem	order / root namespace	511	yes
26	Classical.not_forall	theorem	classical logic	497	yes
27	Classical.em	theorem	classical logic	476	yes
28	CategoryTheory.instCompleteLatticePresieve	definition	category theory	450	yes
29	Nat.mul_lt_mul_left	theorem	Nat	440	yes
30	MulAction.orbitRel	definition	MulAction	423	yes
31	Array.foldrM_congr	theorem	arrays	410	yes
32	monotone_nat_of_le_succ	theorem	order / root namespace	405	yes
33	WellFounded.extrinsicFix	definition	WellFounded	398	yes
34	IsUnit.unit	definition	IsUnit	397	yes
35	BooleanAlgebra.toBiheytingAlgebra	definition	BooleanAlgebra	381	yes
36	Std.DHashMap.Internal.Raw.foldRev_eq	theorem	Std: hash maps	374	yes
37	WellFounded.extrinsicFix₂	definition	WellFounded	366	yes
38	Multiset.add_right_inj	theorem	multisets	363	yes
39	List.eq_nil_iff_forall_not_mem	theorem	lists	363	yes
40	LinearMap.range	definition	LinearMap	358	yes
41	Set.mul_mem_center	theorem	sets	351	yes
42	Std.IterM.toArray	definition	Std: other	348	yes
43	AddSubmonoid.instCompleteLattice._proof_1	theorem	AddSubmonoid	337	yes
44	CategoryTheory.shiftFunctor	definition	category theory	335	yes
45	Lean.Name.quickCmp	definition	Lean	333	yes
46	Submodule.completeLattice	definition	Submodule	333	yes
47	Nat.mono_cast	theorem	Nat	328	yes
48	AddSubmonoid.instCompleteLattice	definition	AddSubmonoid	326	yes
49	CategoryTheory.Sieve.instCompleteLattice	definition	category theory	322	yes
50	Classical.ofNonempty	definition	classical logic	321	yes
51	em	theorem	order / root namespace	316	yes
52	QuotientGroup.leftRel	definition	QuotientGroup	308	yes
53	GroupWithZero.noZeroDivisors	theorem	GroupWithZero	288	yes
54	CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	definition	category theory	284	yes
55	Real.instLT	definition	Real	283	yes
56	LinearEquiv.ofBijective	definition	LinearEquiv	281	yes
57	IsLocallyConstant.tfae	theorem	IsLocallyConstant	279	yes
58	zpow_ne_zero	theorem	order / root namespace	279	yes
59	Set.biInter_range	theorem	sets	270	yes
60	Std.DTreeMap.Internal.Impl.WF.ordered	theorem	Std: other	266	yes
61	FreeAlgebra.lift._proof_4	theorem	FreeAlgebra	263	yes
62	DFinsupp.zipWith	definition	DFinsupp	262	yes
63	eq_or_ne	theorem	order / root namespace	260	yes
64	Equiv.ofBijective	definition	Equiv	258	yes
65	Equiv.Perm.permGroup	definition	Equiv	250	yes
66	List.nodup_finRange	theorem	lists	244	yes
67	NNReal	definition	NNReal	243	yes
68	Set.forall_mem_image2	theorem	sets	239	yes
69	Subsemigroup.center	definition	Subsemigroup	238	yes
70	List.Perm.union	theorem	lists	237	yes
71	List.min?_eq_some_iff	theorem	lists	237	yes
72	Int.natCast_eq_zero	theorem	Int	236	yes
73	Classical.choose	definition	classical logic	232	yes
74	SeminormedAddCommGroup.toIsTopologicalAddGroup	theorem	SeminormedAddCommGroup	231	yes
75	isOpen_iff_nhds	theorem	order / root namespace	230	yes
76	Classical.or_iff_not_imp_left	theorem	classical logic	230	yes
77	List.min?_eq_some_iff_subtype	theorem	lists	228	yes
78	Nat.testBit_two_pow_sub_one	theorem	Nat	224	yes
79	isOpen_iff_mem_nhds	theorem	order / root namespace	223	yes
80	and_forall_ne	theorem	order / root namespace	215	yes
81	TensorAlgebra.lift	definition	TensorAlgebra	211	yes
82	Array.getElem_extract	theorem	arrays	202	yes
83	IsStrictOrderedRing.toIsOrderedRing	theorem	IsStrictOrderedRing	202	yes
84	CategoryTheory.Iso.refl	definition	category theory	200	yes
85	InfHomClass.toOrderHomClass	theorem	InfHomClass	198	yes
86	CommGroupWithZero.toDivisionCommMonoid	definition	CommGroupWithZero	198	yes
87	MonoidHom.mrange._proof_1	theorem	MonoidHom	197	yes
88	HomologicalComplex.Hom.comm	theorem	HomologicalComplex	196	yes
89	Multiset.eq_zero_of_forall_notMem	theorem	multisets	196	yes
90	Equiv.symm_apply_eq	theorem	Equiv	196	yes
91	Equiv.apply_eq_iff_eq_symm_apply	theorem	Equiv	194	yes
92	IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT	theorem	IsLeftCancelAdd	194	yes
93	Int.natCast_eq_zero._simp_1	theorem	Int	193	yes
94	Int.natAbs_ediv	theorem	Int	191	yes
95	SimpleGraph.edgeSet	definition	SimpleGraph	190	yes
96	Nat.cast_nonneg'	theorem	Nat	188	yes
97	by_contradiction	theorem	order / root namespace	186	yes
98	MonoidHom.mrange	definition	MonoidHom	186	yes
99	Fin.fintype	definition	Fin	185	yes
100	AlgebraicGeometry.LocallyRingedSpace.instCategory	definition	AlgebraicGeometry	184	yes

Showing the first 100 of 1,500 rows. The tail is long and flat — rank 1,500 dominates 16. The full set is in the JSON and the CSV.

theorems dominated counts theorems for which this site is the sole route to the axiom. eligible is false when the site's own type is classical, so no constructive replacement for it can exist — true of only 2 of the 1,500, which is the negative result in the eligibility note: the test does not discriminate among load-bearing sites. The full data carries each site's chain, and constant_alone where the site's label constant dominates fewer theorems by itself than the chain does together.

Get the data

dominator-table.json · dominator-table.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. Cite the series as 10.5281/zenodo.21900625, which resolves to the current deposit.

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 site 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.

Why sites rather than constants

A run of constants that each dominate the next, losing no theorems between them, is one repair and not several — severing any member frees the same theorems. Counting them separately would count one repair many times. 182 of the 1,500 rows here are such chains; the rest are single constants.

The hash-map row is the clearest case. Std.DHashMap.Internal.Raw.WF.out, wfImp_alter and isHashSelf_updateBucket_alter dominate 4,892, 4,896 and 4,899 theorems taken individually, and they are one site of 4,899. Read as three constants they look like three findings; read as a site they are one piece of infrastructure.

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.