The gonzalgo Indexes: standing measurements of what formal mathematical libraries rest on

14 tables measuring what formal mathematical libraries depend on, produced by one program (gonzalgo) reading proofs that Lean 4 and Metamath have already checked. 10,859 rows, each table as JSON and CSV. module-spend (3,261 rows) — Modules containing at least one declaration whose own proof term names a choice primitive directly, with the count broken down by primitive. Spending, as opposed to reach: a module with no direct spend can still be full of theorems that depend on choice through what they import. setmm-axioms (3,004 rows) — Every $a statement in Metamath's set.mm — logical axioms, definitions and syntax constructors kept apart — with the number of the library's 47,621 theorems whose proof closure reaches it, and that count as a share of the library. choice-strength (1,528 rows) — The 1,528 theorems in Metamath's set.mm whose proofs reach a choice principle, each labelled with the strongest of the three the database declares separately — full choice, countable choice, dependent choice — together with the raw membership in all three. dominator-table (1,500 rows) — Sites of classical dependence in Mathlib ranked by how many theorems each is uniquely responsible for — the number that would stop depending on the axiom of choice if that site alone were rebuilt. Computed as a dominator tree over the reversed dependency graph rooted at the axiom, with chains of constants that free the same theorems collapsed to a single site. site-diagnosis (765 rows) — Sites of classical dependence in Lean 4 examined for constructive replacement and not removed, each with the reason: no instance could be synthesised, the occurrence was not in a position where an instance is supplied, the available instance itself depends on choice, or synthesis timed out. cleanable (280 rows) — Declarations in Lean 4 core, Std, Batteries, Mathlib and Plausible where a rewrite removing a classical dependence was attempted, with the module, the compiler-generated proof term carrying the dependence, the outcome, and the kernel's reason where it refused. controlled-tactics (270 rows) — A controlled experiment over Lean tactics. 27 arithmetic goals over Nat and Int, each put to ten tactics, with the axiom set recorded for every cell. Holding the goal fixed and varying only the tactic separates a classical dependence introduced by the proof from one required by the statement. tactic-bands (167 rows) — Rates at which Lean tactics' proofs carry an avoidable classical dependence, across four libraries under two attribution rules, each shown against the band spanned by known-negative tactics in the same library and rule. The band is what makes a rate interpretable, and it is wide. spend-points (20 rows) — The 20 largest sites of classical dependence in Mathlib, each with the number of declarations in its dominator subtree that cite a choice primitive directly. Separates sites where the axiom is spent from sites that dominate theorems while inheriting the axiom from further up. substitution-ledger (20 rows) — Kernel-verified substitution attempted against the 20 largest sites of classical dependence in Mathlib. For each declaration: occurrences of Classical.propDecidable in its proof term, how many the harness could reach, how many had a Decidable instance synthesised, and how many produced a term the kernel accepted. kernel-index (14 rows) — What formal mathematical libraries rest on: theorems depending on an unfinished proof, on the compiler rather than the kernel, and on an optional axiom. Measured by one program across two proof systems and six foundations. generated-proofs (13 rows) — What a corpus of machine-generated Lean 4 proofs rests on. 9,169 Goedel-Prover proofs of Lean Workbook problems that compile under Lean 4.32, audited for unfinished proofs, compiler-trusted reductions and axiom dependence, with choice dependence split into the part the statement forces and the part the proof adds. version-delta (12 rows) — Declaration-graph differences between two Mathlib releases, measured by the same extractor on both sides. Separates declarations added and removed from those that kept their name — and among those, separates a changed statement from a changed proof. entry-points (5 rows) — Axioms used, direct entry points into them, and entry points per theorem, for five Metamath databases spanning five foundations. Entry points per theorem normalises for library size and is the measure that can be compared across databases; amplification is carried as reported but is a property of factorization rather than of mathematics. Every figure comes from the proof system's own bookkeeping — Lean's collectAxioms and Metamath's proof structure. The tool proves nothing itself and checks no proofs. Each table carries a sha256 over its rows, and each declares the arithmetic relations its published prose depends on and will not build if one fails. Measured against Lean 4.32.1 with Mathlib v4.32.1, and Metamath set.mm, iset.mm, nf.mm, ql.mm, hol.mm. Live catalogue: f-keys.com/gonzalgo/data/