THE SUBSTITUTION LEDGER
what actually came out, checked by the kernel
Every other measure in this program ranks or bounds. This one removes. A site is only shown to be repairable when a substituted proof term is accepted by Lean's kernel, which is the same standard the library itself is held to and the only measure here that has ever discriminated.
Run against the top of the dominance ranking it returns 8 of 114 occurrences, in 3 declarations. That is the result: at the very top of the ranking, substitution almost entirely fails.
Measured with gonzalgo · Lean 4.32.1 with Mathlib v4.32.1 · substituted terms accepted by the Lean kernel, not by the elaborator
| declaration | dominates | occurrences | testable | synthesised | choice-free |
|---|---|---|---|---|---|
| Std.DHashMap.Internal.Raw₀.isHashSelf_updateBucket_alter | 4,899 | 1 | 0 | 0 | 0 |
| lt_or_eq_of_le | 2,018 | 1 | 0 | 0 | 0 |
| Classical.not_not | 792 | 1 | 1 | 0 | 0 |
| _private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.testBit_two_pow_sub_succ._proof_1_3 | 520 | 2 | 2 | 2 | 2 |
| Classical.not_forall | 497 | 2 | 1 | 0 | 0 |
| _private.Init.Data.Nat.Mod.0.Nat.mul_lt_mul_left._proof_1_1 | 440 | 4 | 4 | 4 | 4 |
| WellFounded.extrinsicFix | 398 | 1 | 1 | 0 | 0 |
| Multiset.add_right_inj | 363 | 44 | 0 | 0 | 0 |
| List.perm_insert_swap | 237 | 1 | 1 | 0 | 0 |
| Std.instMinEqOrOfLawfulOrderLeftLeaningMin | 237 | 45 | 0 | 0 | 0 |
| _private.Init.Data.Int.DivMod.Lemmas.0.Int.natCast_eq_zero._proof_1_1 | 236 | 2 | 2 | 2 | 2 |
| Classical.or_iff_not_imp_left | 230 | 1 | 1 | 0 | 0 |
| and_forall_ne | 215 | 1 | 0 | 0 | 0 |
| Classical.or_iff_not_imp_right | — | 1 | 1 | 0 | 0 |
| DerivingHelpers.deriving_lawful_beq_helper_nd | — | 1 | 1 | 0 | 0 |
| HomologicalComplex.Hom.comm | — | 1 | 1 | 0 | 0 |
| by_contradiction | — | 1 | 1 | 0 | 0 |
| not_and_or | — | 1 | 1 | 0 | 0 |
| not_iff_not | — | 2 | 2 | 0 | 0 |
| not_imp_not | — | 1 | 1 | 0 | 0 |
The four counts narrow in sequence. occurrences is uses of Classical.propDecidable in the proof term; testable is how many the harness could reach; synthesised is how many had a Decidable instance found; choice-free is how many produced a term the kernel accepted. Only the last column means a removal happened.
Get the data
substitution-ledger.json · substitution-ledger.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/Subst2.lean
ConstantInfo.value? must be passed allowOpaque := true or theorem proof terms read as empty and every occurrence count here comes back zero. Code and derived data: 10.5281/zenodo.21883963.
The bottleneck is not synthesis
Of 114 occurrences only 21 were testable at all. The rest occur under binders, where the proposition is not closed and cannot be handed to instance synthesis from outside its declaration. That is a limit of this harness rather than a fact about the proofs, so the 8 here is a floor. Re-running inside each declaration's own context is the obvious next move and has not been done.
Where an occurrence was testable, synthesis and the kernel agreed every time: 8 synthesised, 8 accepted, no term that elaborated and then failed to check.
What came out, and what it says
All three successes are private lemmas about Nat and Int — bit arithmetic, modular arithmetic, a cast — where the propositions are decidable by computation and a constructive instance already exists. That is the same population the controlled experiment identifies: on Nat and Int the free instance is there and the classical one was taken anyway.
Nothing at the head of the ranking moved. Classical.propDecidable dominates 91,858 theorems, has a choice-free type, passes the eligibility test, and cannot be made constructive. lt_or_eq_of_le dominates 2,018 and its one occurrence was not testable. The ranking is good at finding what is load-bearing and it does not follow that what is load-bearing can be moved.