Eligibility Discriminates Among Theorems and Not Among the Constants They Rest On
Abstract
Separating a theorem's statement dependencies from its proof dependencies bounds how much classical dependence a formal library could shed. Across Mathlib, 13.1% of theorems have a choice-free statement and a choice-dependent proof; nothing outside that band can be removed under any argument. The measure is informative because most theorems fail it: 78.6% of the theorems that reach Classical.choice are bound by what they say.
This note reports that the same measure stops discriminating exactly where it would be used. Applied to the 327,981 constants that dominate those theorems in the dependency graph, 22.88% are eligible overall, but the rate is not uniform in the thing that matters. Among constants dominating a single theorem it is 16.04%. Among constants dominating two or more it is above 99%, rising monotonically with size, and among the 25 constants dominating 500 theorems or more it is 100%.
The transition is a cliff between one and two, not a gradient. A constant that is load-bearing for more than one theorem is eligible with near-certainty, so eligibility cannot be used to choose which load-bearing constant to attack.
The reason is structural. A constant many theorems route through is a general-purpose lemma or instance, general-purpose declarations are stated in general terms, and general terms are choice-free. The property that makes a constant important is the property that makes it eligible. The clearest witness sits at the top of the ranking: Classical.propDecidable, whose type Decidable a is choice-free, is therefore eligible, dominates 91,858 theorems, and cannot be made constructive, because deciding an arbitrary proposition is the classical assumption.
This is a negative result about the measure, not about the constants. It does not say the eligible sites are unfixable; it says the test does not separate the fixable from the unfixable at the level where a repair would be chosen.
Measured on Lean 4.32.1 with Mathlib v4.32.1. The reproduction archive recomputes every table from bundled data with no Lean toolchain.
Cite it
Gonzalez, V. (2026). Eligibility Discriminates Among Theorems and Not Among the Constants They Rest On. Zenodo. https://doi.org/10.5281/zenodo.21884471