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

Eight tables measuring what formal mathematical libraries depend on, produced byone program (gonzalgo) reading proofs that Lean 4 and Metamath have alreadychecked. 2,006 rows, each table as JSON and CSV. kernel-index (14 rows) - theorems resting on an unfinished proof, on the compilerrather than the kernel, or on an optional axiom, across nine Lean libraries andfive Metamath databases spanning six foundations. dominator-table (1,500 rows) - sites of classical dependence in Mathlib ranked byhow many theorems each is uniquely responsible for. A site is a chain of constantsthat each dominate the next, since severing any member frees the same theorems. controlled-tactics (270 rows) - a controlled experiment. 27 arithmetic goals overNat and Int, each put to ten Lean tactics, axiom set recorded per cell. Holding thegoal fixed and varying only the tactic separates a dependence the proof introducedfrom one the statement required. spend-points (20 rows) - which of the largest dominating sites contain a direct useof a choice primitive and which only inherit one. Fifteen of twenty spend nothing. substitution-ledger (20 rows) - kernel-verified substitution attempted at the top ofthe ranking. 114 occurrences, 21 reachable, 8 accepted by the kernel. entry-points (5 rows) - axioms used, direct entry points, and entry points pertheorem across five Metamath foundations. tactic-bands (167 rows) - tactic classical-dependence rates against the band spannedby tactics that cannot introduce a classical instance, which is what makes any suchrate readable. generated-proofs (10 rows) - what 9,169 machine-generated Lean proofs rest on. Every figure comes from the proof system's own bookkeeping - Lean's collectAxiomsand Metamath's proof structure. gonzalgo proves nothing itself and checks no proofs.Each table carries the library version it was taken from and a sha256 over its rows.The build scripts are included; each table declares the arithmetic relations itsaccompanying 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.