Which Constant Is Responsible? Dominator Analysis of Classical Dependence in Mathlib
Abstract
61.2% of Mathlib's theorems depend on Classical.choice. Asking which constant is responsible for that dependence is a different question from asking which constants a proof touches, and the two answers differ by a factor of 58 on the first case examined: 116,766 theorems reach the order lemma lt_or_eq_of_le, and 2,018 would stop being classical if it were rebuilt constructively. The rest have another route.
The distinction is exactly dominance. In the dependency graph reversed and rooted at the axiom, severing a constant frees precisely the theorems it dominates, so one dominator tree answers for all 766,564 constants what a separate reachability computation answers for one. Built with the iterative algorithm of Cooper, Harvey and Kennedy, it converges in three passes and reproduces six independently computed severing counts exactly.
Two results follow. First, 60.1% of classically dependent theorems have no responsible constant at all: their immediate dominator is the axiom itself, so no single declaration gates them and no local repair can reach them. Second, the 39.9% that do have one concentrate in a way that a mathematics library is not usually described in. Outside classical logic itself, the largest sites are a functor category instance (5,271 theorems), hash-map well-formedness in the standard library (4,899), the powerset Boolean algebra (3,430) and string-to-list conversion (1,111). Classical dependence in Mathlib accumulates in its infrastructure rather than in its mathematics.
The dominator construction is standard and is used this way in memory profilers and bundle-size tooling; what appears to be new is its application to a proof-dependency graph rooted at an axiom, and the reading of the resulting subtree sizes as removability weights.
Measured on Lean 4.32.1 with Mathlib v4.32.1: 766,564 declarations, 29,469,817 dependency edges. The pipeline is validated against the author's previously published figures before any new number is reported, reproducing 324,510 theorems reaching Classical.choice against a published 324,808, and the eligibility ceiling at 13.1%.
The reproduction archive recomputes every table from bundled data with no Lean toolchain; the Lean sources that regenerate the graph are included.
Cite it
Gonzalez, V. (2026). Which Constant Is Responsible? Dominator Analysis of Classical Dependence in Mathlib. Zenodo. https://doi.org/10.5281/zenodo.21883963